Information Technology Reference
In-Depth Information
O
prov
of
provided
operations (for inputs),
O
req
consists of pairwise disjoint sets
O
int
of
internal
operations. Provided
operations are offered by a component and can be invoked by the environment;
required operations are required from the environment and can be called by the
component. To indicate that
op
of
required
operations (for outputs), and
∈O
prov
we often write ?
op
and to indicate that
∈O
req
we often write !
op
.
State variables.
In order to equip operations with pre- and postconditions con-
cerning the operations' formal parameters
and
the data states of a component,
we must first provide a formal notation for data states. For this purpose we use
state variables of different kinds which all belong to a global set SV of state
variables.
Provided
state variables describe the externally visible data states,
while
internal
state variables describe the hidden data states of a component.
Provided and internal state variables together model the possible data states a
component can adopt. There is, however, still a third kind of state variable which
we call
required
state variable. Required state variables are used to refer to the
data states a component expects to be visible in its environment. Formally, an
I/O-state signature
op
V
prov
V
req
V
int
consists of pairwise disjoint sets
V
prov
,
V
=
V
req
,and
V
int
of provided, required and internal state variables, respectively.
Definition 1 (I/O-Signature).
An
I/O-signature
is a pair
Σ
=(
V
,
O
)
con-
sisting of an I/O-state signature
V
and an I/O-operation signature
O
.
Predicates on states.
We assume given a global set LV of logical variables, disjoint
from the state variables SV such that, for each operation
op
,
par
(
op
)
⊆
LV .
Moreover, we assume a set
S
(SV
,
LV ) o f
state predicates
ϕ
and a set
T
(SV
,
LV )
of
transition predicates
π
with associated sets
var
state
(
ϕ
)
⊆
SV of state variables
and
var
log
(
ϕ
)
LV of logical variables; analogously for
π
. State predicates refer
to single states and transition predicates to pairs of states (pre- and poststates).
For each
⊆
W⊆
SV and
X
⊆
LV we define
S
(
W
,X
)=
{
ϕ
∈S
(SV
,
LV )
|
var
state
(
ϕ
)
⊆W
,
var
log
(
ϕ
)
⊆
X
}
,
T
(
W
,X
)=
{
π
∈T
(SV
,
LV )
|
var
state
(
π
)
⊆W
,
var
log
(
π
)
⊆
X
}
.
We require that both sets,
S
(
W,X
)and
T
(
W,X
), are closed under the usual
logical connectives, like
∧
,
⇒
, etc. We assume that state predicates
ϕ
∈S
(
W
,X
)
and transition predicates
π
∈T
(
W
,X
) are both equipped with a
satisfaction
relation
π
, resp., expressing universal validity of predicates w.r.t.
some semantic domain of states and w.r.t. a domain of valuations for the logical
variables. We will not go into further details here, but the reader may assume a
predefined data universe
ϕ
and
U
such that concrete data states are functions mapping
state variables to values in
U
and, similarly, valuations are mappings from logical
variables to values in
. Then state predicates should be interpreted w.r.t. a sin-
gle data state and a valuation of the logical variables, while transition predicates
should be interpreted w.r.t. two data states (pre- and poststates) and a valuation
of the logical variables. Universal validity
U
ϕ
of a state predicate
ϕ
∈S
(
W
,X
)
then means that
ϕ
is valid for all data states, modeled by functions
σ
:
W→U
,
Search WWH ::
Custom Search