Information Technology Reference
In-Depth Information
4.6
State ADT
The ADT
STATE
models the
state
with three queries to retrieve the different parts of
the ADT.
regions
:
STATE
→
REG
heap
:
STATE
→
HEAP
store
:
STATE
→
STORE
The command
set
sets the regions, the heap, and the store at the same time. A precondi-
tion specifies consistency criteria between the parts of the state. The first precondition
clause states that a processor can handle an object if and only if the object is on the heap.
The second precondition clause states that if the heap declares a feature as non-fresh
on a processor
p
, then the regions must know about this processor. The third precon-
dition clause requires that all processors stored in attribute values are known by the
regions. Note that
HEAP
already requires that the references stored in attribute values
are known. The forth precondition clause states that each non-empty environment in the
store must belong to a processor that is known by the regions. The fifth precondition
clause states that each value in the store must either be a known reference or a known
processor.
set
:
STATE
→
REG
HEAP
STORE
STATE
σ
.
require
∃
p
∈
k
.
procs
,∃
o
∈
OBJ
:
k
.
handled objs
(
p
)
.
has
(
o
)
↔
h
.
objs
.
has
(
o
)
∃
p
∈
PROC
,
f
∈
FEATURE
:
¬
h
.
is fresh
(
p
,
f
)
→
k
.
procs
.
has
(
p
)
∀
o
∈
h
.
objs
,
a
∈
o
.
class type
.
attributes
:
o
.
att val
(
a
)
∈
PROC
→
k
.
procs
.
has
(
o
.
att val
(
a
))
∀
p
∈
PROC
,
e
∈
s
.
envs
(
p
)
:
¬
e
.
names
.
is empty
→
k
.
procs
.
has
(
p
)
∀
p
∈
k
.
procs
,
e
∈
s
.
envs
(
p
)
,
x
∈
e
.
names
:
(
e
.
val
(
x
)
∈
REF
→
e
.
val
(
x
)=
void
∨
h
.
refs
.
has
(
e
.
val
(
x
)))
∧
(
e
.
val
(
x
)
∈
PROC
→
k
.
procs
.
has
(
e
.
val
(
x
)))
axioms
σ
.
set
(
k
,
h
,
s
)
.
regions
=
k
σ
.
set
(
k
,
h
,
s
)
.
heap
=
h
σ
.
set
(
k
,
h
,
s
)
.
store
=
s
set
(
k
,
h
,
s
)
Creation.
To create a state, one has to create the three parts of the state. This is done
with the constructor
make
.
make
:
STATE
axioms
make
.
regions
=
new
REG
.
make
make
.
heap
=
new
HEAP
.
make
make
.
store
=
new
STORE
.
make
Facade.
It is too cumbersome to work with
STATE
as it is. For example, the following
expression defines a new state
σ
in which a new processor has been added to the state
de f
=
σ
.
σ
σ
. This expres-
sion is too long for this simple task, especially if the expression is used multiple times.
:
set
(
σ
.
regions
.
add proc
(
new
PROC
.
make
)
,
σ
.
heap
,
σ
.
store
)
Search WWH ::
Custom Search