Information Technology Reference
In-Depth Information
,
where
{⨀←
}
is the substitution of
for
⨀
in
.
The hole
⨀
plays an important role in our context model. In fact a context
containing a
single hole represents the environment of a process
in the process
()
. A process
modelling Bob using a smart phone in the conference room with Alice can be specified as:
(ℎ[])≙ℎ[][],
where
is the context specified in Example 5.2 and
is the specification of the smart phone.
A process modelling Bob using a PDA in the conference room can be specified as:
(
0
)
≙
|
[
]
,
where
is the context specified in Example 5.2. The syntax of CEs is given in Table 3 where
ranges over CEs,
ranges over names and
is a variable symbol which also ranges over
names.
∷=
Context Expressions
True
true
=
name match
•
hole
¬
negation
|
parallel composition
∧
conjunction
[]
location
new
(,)
relevation
⨁
spatial next modality
⟡
somewhere modality
∃.
existential quantification
Table 3. Syntax context expressions
5.3 A simple example
This example illustrates the use of process abstraction and process call as a mechanism for
context provision and context acquisition, respectively. A process abstraction can be thought
of as the declaration of a procedure in procedural programming languages and a process
call as the invocation of a procedure.
A process abstraction links a name
to a process
using the following syntax:
⊳().
