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