Information Technology Reference
In-Depth Information
4.2 State Changes
The initial state has no variables:
value
init: State = [ ]
A state is subsequently build and modified through a series of basic operations
to declare, undeclare and modify variables, as well as operations obtained from
them by sequencing, concurrency, choice, etc. The type
StateX
represents such
state-changing expressions and the function
exec
checks if a pair of states -
initial and final state - are a possible effect of executing a given expression.
type
StateX ==
decl(StructX)
|
undecl(Id)
|
change(Id, StructX)
|
seq(StateX, StateX)
|
con(StateX, StateX)
|
test(BoolX, StateX, StateX)
value
exec: StateX
×
State
×
State
→
Bool
exec(sx, s, s
)
≡
case
sx
of
decl(tx)
→
decl(eval(tx, s), s, s
),
undecl(id)
→
undecl(id, s, s
),
change(id,tx)
→
change(id, eval(tx, s), s, s
),
seq(sx1, sx2)
→
(
∃
s
: State
•
exec(sx1, s, s
)
∧
exec(sx2, s
,s
)),
con(sx1, sx2)
→
exec(sx1, s, s
)
∧
exec(sx2, s, s
),
test(px, sx1, sx2)
→
if
eval(px, s)
then
exec(sx1, s, s
)
else
exec(sx2, s, s
)
end
end pre
iswf(sx, s)
For instance, here is a function
decl
to declare a variable. Its pre-condition
canDecl
checks if a given structure is a variable and its identifier is new.
value
decl: Struct
×
State
×
State
→
Bool
decl(v,s,s
)
≡
s
=s
∪
[ val2id(val(v(idCat)(1)))
→
v]
pre
eval(canDecl(v), s),
canDecl: Struct
→
BoolX
canDecl(v)
≡
and(hasType(v, vType), not(hasVar(v)))
StateX
depends on external expressions like
StructX
or
BoolX
.Hereisthe
definition of
StructX
with operations to get, make and modify structures by
adding or deleting their parts (all parts with a given category and value).
type
StructX ==
get(Id)
|
make(Struct)
value
eval: StructX
×
State
→
Struct
eval(sx, s)
≡
case
sx
of
get(id)
→
s(id),
make(st)
→
make(st),
add(px, sx)
→
add(eval(px, s), eval(sx, s), s),
del(c, vx, sx)
→
del(c, eval(vx, s), eval(sx, s), s)
end pre
iswf(sx, s)
|
add(PartX, StructX)
|
del(Cat, ValueX, StructX)
Search WWH ::
Custom Search