Information Technology Reference
In-Depth Information
contains a component
v
(
V
C
) which denes the value of
v
in the abstract state
-related to the concrete state represented by
V
C
.
v 2 IO
For the abstract observable variables
, premise R3 already constrains
O
v
(
v
(
V
C
)=
V
C
). It therefore remains to describe the mappings
us to choose
v
for
.
Recall that every variable
v 2 V
C
− IO
=
MRL
v 2 R
gives rise to an abstract register variable
v
,
an abstract memorization variable
m:v
introduced into the
sts
corresponding to
A
, and a corresponding concrete variable
v
c
. For example, the register flow ZN
in the
program DEC, gave rise to a similarly named variable and to the
memorization variable m.ZN in the
Signal
sts
DEC and to the concrete variable ZN
c
in function DEC iterate().
Therefore, we dene for each register flow
r
the following two instances of
the
mapping:
0
m:r
r
c
:
m:r
=
r
c
=
For example, the mapping into the abstract variable m.ZN will be given by the
equation m.ZN = ZN
c
.
It only remains to dene
v
for
v 2 RL
. Since variables in
L
do not necessarily
have counterparts in the
C
program, it may not be so easy to nd an expression
over
V
C
which will capture their values.
Here we are helped by the fact that every compilable Signal program
A
is
determinate
in the new values of
I
(the inputs) and
R
(the register flows).
I
0
Equivalently, the corresponding
sts
A
is determinate in the values of
(new
inputs) and
(old memorization values). Determinateness means that a set of
values for these variables uniquely dene the new values of all other variables
(all variables in
M
). Determinateness is the necessary condition for being
able to compile the program into a deterministic running program. Input
IORML
Signal
programs which are not determinate are rejected by all the
Signal
compilers
we worked with.
We use the fact that every abstract variable
v 2 RL
has a unique equation
v
0
=
eq
v
of the form
sts
A
. In principle, determinateness implies that we
could chase these equations applying successive substitutions until we nd for
within
v
a dening expression all in terms of the concrete variables
V
C
. However, this is
not actually necessary. Instead, we transform premises R1{R3 into the following
two verication conditions:
^
^
C
^
m:r
r
c
)
^
v
?
!
A
W1.
(
=
(
=
)
r2R
v2IORL
8
:
9
;
^
C
W2.
^
r2R
^
^
m:r
=
r
c
O
v
)
0
)
v
0
=(
v
0
=
eq
v
)
^
^
(
(
^ m:r
0
=
r
c
v2IO
v2RL
!
A
O
a
=
O
c
is automatically
Obviously, we can dispense with premise R3 since
O
v
guaranteed by taking
v
=
for each
v 2 IO
. In verication condition W1, we
simplied the mapping
having the prior information that only the
m:r 2 M
Search WWH ::
Custom Search