Information Technology Reference
In-Depth Information
variables have non-bottom values and they are mapped by
into their concrete
counterparts
r
c
.
In verication condition W2 we used the fact that the only unprimed variables
to which
A
refers are the memorization variables
m:r
. Therefore, it is sucient
to map them in the unprimed version of
V
A
=
(
V
C
). For the primed version
O
v
for all
m:r
0
=
r
c
of
,weused
v 2 IO
,
for all
r 2 R
(
m:r 2 M
). and the
original
.
Theorem 1.
With the notation introduced above, if verication conditions W1
andW2arevalid,then
sts
A
equations for each
v 2 RL
CvA
.
4.4 Illustrate on the Example
Applying these methods to the case of the
Signal
program DEC and its trans-
lated
C
-program DEC iterate(), we obtain the following two verication condi-
tions:
8
:
9
;
8
:
9
;
FB =
?
FB =
?
^
N=
?
^
m.ZN = ZN
c
^
^
N=
?
!
U1.
ZN
c
=1
^
ZN =
?
^
ZN =
?
^
m.ZN = 1
8
:
9
;
m.ZN = ZN
c
FB
0
=
if
h2
0
c
then
FB
0
c
else
^
?
N
0
=N
c
U2.
C
^
^
!
A
m.ZN
0
=ZN
c
^
ZN
0
=
if
N
0
^
=
?
then
m.ZN
else
?
variables FB
0
and N
0
, and for the
Note that the
-mapping for the
IO
M
variable
m.ZN is given directly in terms of the concrete variables, while the
-mapping
of ZN
0
is given in terms of the abstract variables N
0
and m.ZN. In principle, it
is possible to substitute the denitions of N
0
and m.ZN in the right-hand side
of the denitions for ZN
0
and obtain a mapping which expresses all the relevant
abstract variables in terms of the concrete variables. Performing the substitution
and some simplications concerning comparison to
?
, we obtain the following
version of U2:
8
:
9
;
m.ZN = ZN
c
FB
0
=
if
h2
0
c
then
FB
0
c
else
^
?
N
0
=N
c
^
C
^
!
A
U2a.
m.ZN
0
=ZN
c
^
ZN
0
=ZN
c
^
The presented approach is immune against the optimizations performed by the
industrial code generators that we considered. The proof technique exploits, in
contrast to our previous work [20], only minimal knowledge about the code gen-
eration process. We only assume that
variables are reconstructible which
is the minimal requirement for the C-code to be a correct implementation of the
Signal
IOM
source [16].
Search WWH ::
Custom Search