Information Technology Reference
In-Depth Information
Definition 5.
A
θ
-interpretation structure
for a signature
θ
=(V,
Γ
, tv, ta, D) is a triple
(
T
,
A
,
G
) where:
•
T
is a transition system (
W
, w
0
,
E
,
→
)
s
U
).
•
A
is an S-indexed family of maps
A
s
: V
s
→
(
W
→
2
E
.
That is to say,
A
interprets attribute symbols as functions that return the value that
each attribute takes in each state, and
G
interprets the action symbols as sets of events
-- the set of the events during which the action occurs.
It is possible that no action will take place during an event. Such events correspond
to environment steps, which means steps performed by the other components in the
system. Interpretation structures are intended to capture the behavior of a design in
the context of a system of which it is a component. Because environment steps are
taken into account, state encapsulation techniques can be formalized through particu-
lar classes of interpretation structures.
•
G
:
Γ
→
Definition 6.
A
θ
-interpretation structure
(
T
,
A
,
G
) for a signature
θ
=(V,
Γ
, tv, ta, D)
∈
W
, if (w, e, w') is in →, and
is called a
locus
iff, for every a
∈
loc(V) and w, w'
G
(g), then
A
(a)(w') =
A
(a)(w).
This means a
locus
is an interpretation structure in which the values of the program
variables remain unchanged during events in which no action occurs that contains
them in their write frame.
Having defined the interpretation structures for designs and the model for the ab-
stract data type specification (S), we are able to give the semantics of the terms and
propositions in the language given by the design signature.
for any g
∈
D(a), e
∉
Definition 7.
Given a signature
-interpretation structure
S=
(
T
,
A
,
G
), the semantics of terms (for every sort s, term t
of sort s
and w
θ
= (V,
Γ
, tv, ta, D) and a
θ
∈
W
,
[t]
s
(w)
s
U
,
the value taken by t in the world w, is defined as follows:
∈
A
s
, [a]
s
(w) =
A
(a)(w)
•
if t
is a
∈
if t
is a constant c, [c]
s
(w) = c
U
•
if t
is f
U
:
s
1
U
×
s
n
U
→
s
U
, [f(t
1
,t
2
,…,t
n
)]
s
(w) = f
U
([t
1
]
s
(w), [t
2
]
s
(w), …,
•
…
×
[t
n
]
s
(w))
The semantics of propositions is defined as:
•
(
S
,w)
t
(t
1
=
s
t
2
) iff [t
1
]
s
(w) = [t
2
]
s
(w)
(
S
,w)
t
(t
1
p
s
t
2
) iff [t
1
]
s
(w) p
s
U
[t
2
]
s
(w)
•
•
(
S
,w)
t
φ
1
⇒
φ
2
, iff (
S
,w)
t
φ
1
implies (
S
,w)
t
φ
2
)
Now on the semantic level, we can represent whether a proposition (in a signature)
is true or valid in the interpretation structure of the signature:
•
(
S
,w)
t
(
¬φ
) iff
¬
((
S
,w)
t
φ
Definition 8.
A
θ
-
proposition
φ
is
true
in an
θ
-interpretation structure
S
, written
S
t
φ
, iff (
S
,w)
t
φ
at every state w. A proposition
φ
is
valid
, written
t
φ
, iff it is true in
every interpretation structure.
Having introduced the above concepts, we can now define when an interpretation
structure is a model of a design.
Search WWH ::
Custom Search