Information Technology Reference
In-Depth Information
as logical implications, and all the above operations on designs are monotonic
with regard to refinements (i.e. the order of implication). These fundamental
mathematical properties ensure that the domain of designs is a proper seman-
tic domain for sequential programming languages. There is a nice link from the
theory of designs to the theory of predicate transformers with the following
definition:
R, q
)
de
=
p
wp
(
p
∧¬
(
R
;
¬
q
)
that defines the
weakest precondition
of a design for a post condition
q
.
Concurrent and reactive programs, such as those specified by Back's action
systems [4] or Lamport's Temporal Logic of Actions (TLA) [19], can be defined
by the notion of
guarded designs
, written as
g
&
D
and defined by
wait
∧
v
=
v
))
(
α,
if
g
then
P
else
(
true
The domain of guarded designs enjoys the same closure properties as that do-
main. And refinement is defined as logical implication, too.
The basic UTP has no notions of objects, classes, inheritance, polymorphism,
and dynamic binding. For a combination of OO and component-based modelling,
we have extended UTP to object-oriented programming [14].
Contracts of Interfaces.
In the current version of rCOS, we only consider
components in the application of concurrent and distributed systems, and a
contract
Ctr
=(
I, Init, MSpec, Prot
)
specifies
-
the allowable initial states by the initial condition
Init
,
-
the synchronization condition
g
on each declared method and the function-
ality of the method by the specification function
MSpec
that assigns each
method to a guarded design
g
&
D
.
-
Prot
is called the
protocol
and is a set of sequences of call events; each is
of the form
?
op
1
(
x
1
)
,...,
?
op
k
(
x
k
)
. Notice a protocol can be specified by a
temporal logic or a trace logic.
For example, the component interface in Fig. 1 does not say the buffer is a one-
place buffer. A specification of a one-place buffer can be given by a contract
B
for which
-
The interface:
B
1
.I
=
q
:
Seq
(
int
)
, put
(
item
:
int
;)
, get
(;
res : int
)
-
The initial condition:
B
1
.Init
=
q
=
<>
-
The specification:
B
1
.MSpec
(
put
)=
q
=
<>
&
true q
=
<item>
B
1
.MSpec
(
get
)=
q
=
<>
&
true res
=
head
(
q
)
∧ q
=
<>
-
The protocol:
B
1
.Prot
is a set of traces that is a subset of
{e
1
,...,e
k
| e
i
is ?
put
() if
i
is odd and ?
get
() otherwise
}.
Search WWH ::
Custom Search