Information Technology Reference
In-Depth Information
All these sets of symbols are assumed to be finite and mutually disjoint. Channels are
used as atoms in the definition of terms:
Definition 2.
Given a design signature
θ
=(V,
Γ
, tv, ta, D), the language of
terms
is
defined as follows: for every sort s
∈
S,
•
t
s
::= a , where a
∈
V and of type s
•
t
s
::= c, where c is a constant with sort s
•
t
s
::= f(t
1
,…,t
n
), where t
1
: s
1
,…, t
n
: s
n
and f:s
1
×
…
×
s
n
→
s
The language of
propositions
is defined as follows:
•
where p
s
is a binary predicate defined on sort s. The set of predicates defined on sort s
must contain =
s
.
Having defined the signature of designs and given the language of terms and
propositions, we can formalize the notion of designs as follows:
φ
:: = (t
1s
p
s
t
2s
) |
φ
1
⇒
φ
2
|
φ
1
∧
φ
2
|
¬φ
Definition 3.
A
design
is a pair (
θ
,
Λ)
, where
θ
= (V,
Γ
, tv, ta, D) and
Λ
is (I, R, L, U)
where:
•
I is a proposition defined on
, which constrains the values of the channels
when the program is initialized.
θ
•
R assigns to every action g
∈
Γ
an expression R(g).
•
For every action g
, L(g) assigns the enabling guard to it and U(g) as-
signs the progress guard.
∈
Γ
{prv, out}.
Recall that R(g) specifies the effect of action g on its write frame. For any channel a
•
For every action g
∈
Γ
, for any a
∈
D(g), tv(a)
∈
D(g), we will use R(g,a) to denote the expression that represents the effect of action g
on channel a.
Before we define the semantic structures for a design, a model for the abstract data
type specification (S) needs to be introduced. The model is given by a
∈
Σ
-algebra
U
,
i.e., a set s
U
is assigned to each sort symbol s
∈
S, a value in s
U
(c
U
) is assigned to
each constant symbol c of sort s, a (total) function f
U
:
s
1
U
×
s
n
U
→
s
U
is assigned to
…
×
each function symbol f in S, and a relation p
s
U
⊆
s
×
s is assigned to each binary
predicate p
s
defined on sort s.
The semantic interpretation of designs is given in terms of transition systems:
Definition 4.
A
transition system
(
W
, w
0
,
E
,
→
) consists of:
•
a non-empty set
W
of states or possible worlds
•
w
0
∈
W,
the initial state
•
a non-empty set
E
of events
•
an
E
-indexed set of partial functions
→
on
W
,
W
→
(
E
→
W
), defines the
state transition performed by each event.
Having transition systems to represent the state transitions of a design, we can inter-
pret the signature of a design with the following structure:
Search WWH ::
Custom Search