Information Technology Reference
In-Depth Information
sp(
p, φ
)
de
=
Post
sy
(
p,
{
(id
,φ
)
}
)
.
Intuitively, sp(
p, φ
) is the strongest predicate satisfied by the post-states of the
extension of
φ
—i.e., the predicate whose extension is precisely the set of such
post-states. Its dual is the
weakest liberal precondition predicate transformer
wlp(
p, φ
) that yields the weakest predicate satisfied by the states whose post-
states satisfy
φ
.
PostPredicateAbstraction(
p
,
H
,
Σ
):
result :=
∅
for all
σ ∈ Σ
:
for all
σ
∈P
(
H
)
:
if a theorem prover is able to prove that
sp(
p,
σ
)=
⇒¬
σ
is valid (or, equivalently,
=
⇒
wlp(
p, ¬
σ
)
is valid):
σ
that
skip
else:
result := result
∪{σ
}
return result
Fig. 9.
Computing the abstract post-state transformer for predicate abstraction
The properties summarized above allow us to devise an algorithm to compute
the abstract post-state transformer (see a draft in Figure 9). Soundness is ensured
by considering all abstract states feasible unless the theorem prover proves the
contrary. The precision of the resulting abstract post-state transformer depends
on the precision of the theorem prover. The hard step of the procedure is deciding
the validity of a formula with shape sp(
p, φ
0
)=
φ
1
, a problem that can be
proved equivalent to the (typically easier) problem of deciding the validity of the
formula
φ
0
=
⇒
⇒
wlp(
p, φ
1
).
3.4 Classification of Basic Techniques
The categories introduced in this section allow us to classify practical state
space exploration techniques usually indicated by terms like “model checking”,
“testing”, etc. Table 1 summarizes the taxonomy that we briefly comment below.
Testing.
As discussed above, testing is a non-monotonic and width-bounded
state space exploration, but there exist variants where the exploration is also
depth-bounded. The ideal “exhaustive testing” that consists of executing the
program for all the possible inputs is still a non-monotonic and width-bounded
state space exploration, with no width bound on
S
at iteration 0 (i.e., initially
S
:=
I
). A fully exhaustive exploration is still more precise than exhaustive test-
ing, coinciding with the latter when the program is deterministic and
I
is finite
(when
I
is not finite, exhaustive testing is infeasible).
Search WWH ::
Custom Search