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