Information Technology Reference
In-Depth Information
5 Checking the Proof Obligations
As shown in the previous section, the generated proof obligations are quantier-
free implications referring to potentially innite data domains such as the inte-
gers. Direct submission of these implications to a theorem prover such as PVS
and invoking various proof procedures turned out to be far too slow.
In this section we explain the theoretical basis for an ecient BDD-based
evaluation of the proof obligations on the basis of
uninterpreted functions
.
Typically, the verication conditions involve various arithmetical functions
and predicates, tests for equality, boolean operations, and conditional (if-then-
else) expressions. It has been our experience that the compiler performs very
few arithmetical optimizations and leaves most of the arithmetical expressions
intact. This suggests that most of the implications will hold independently of
the special features of the operations and will be valid even if we replace the
operations by
uninterpreted functions
.
5.1
The Uninterpreted Functions Encoding Scheme
Under the uninterpreted functions abstraction, we follow the encoding procedure
of [2]. For every operation
f
occurring in a formula
'
, which is not an equality
test or a boolean operator, we perform the following:
i
f
Replace each occurrence of a term
f
(
t
1
;:::;t
k
)in
'
by a new variable
v
of a type equal to that of the value returned by
f
. Occurrences
f
(
t
1
;:::;t
k
)
and
f
(
u
1
;:::;u
k
) are replaced by the same
v
i
f
i
t
j
is identical to
u
j
for
every
j
=1
;:::;k
.
Let
^
t
denote the result of replacing all outer-most occurrences of the form
f
f
(
t
1
;:::;t
k
) by the corresponding new variable
v
in a sub-term
t
of
'
.For
j
f
,
i
f
every pair of newly added variables
v
and
v
i 6
=
j
, corresponding to the
f
t
1
;:::;t
k
)and
non-identical occurrences
(
f
(
u
1
;:::;u
k
), add the implication
j
f
as antecedent to the transformed formula.
(
^
^
i
t
1
=^
u
1
^^
t
k
=^
u
k
)
)v
f
=
v
Example 1.
Following are
a
of program DEC, after performing the unin-
terpreted functions abstraction. Note how the '-' function and the '
c
and
' predicate
i
−
i
were replaced by the new symbols
v
and
v
respectively, where
i
is a running
index:
8
:
9
;
(h1
0
c
=
T
)
(h2
0
c
=(
^
1
v
))
(h2
0
c
)
N
0
c
=FB
c
)
^
c
=
h2
0
c
)
(FB
0
c
=FB
c
^
N
c
=
^
(
:
v
1
−
))
(ZN
0
c
=N
c
)
^
Search WWH ::
Custom Search