On the Integration of Software Testing and Formal Analysis - Empirical Software Engineering and Verification - page 167

share common features with sentences in a formal language, or equivalent for-
malisms like ordered binary decision diagrams [4]. As an example, the formula
x> 0 describes intensionally the infinite set of all and only the states which
assign a positive value to the variable x . Intensional representations have com-
plementary properties with respect to extensional ones, stemming from the fact
that the size of a symbolic formula is loosely correlated with the size of the set
it represents. Symbolic-state techniques can represent very large, and even infi-
nite, sets of states with a short formula, but sometimes may use large formulas to
represent small, or even empty, sets of states. Moreover, the same set of states
may have many, even infinite, different symbolic representations that may be
hard to compare. Indeed, the most relevant decision problems (equivalence and
inclusion) become computationally hard, or even undecidable, for most symbolic
languages.

Abstraction. Abstraction limits the fully exhaustive exploration of the state
space of a program by partitioning the space of the possibly infinite program
states into a (possibly finite) number of subsets, and by analyzing only a finite
number of representative behaviours for each set. As an example, let us consider
the program from Figure 1, which for the reader's comfort has been reported on
the left side of Figure 5. If we relax all the statements' guards by dropping all
the clauses on x ,andatthesametimeweremovealltheassignmentsto x ,we
obtain the finite-state program reported on the right side of Figure 5. There is a
precise relationship between the possible behaviours of the two programs, which
allows e.g. to conclude that the program on the left side of Figure 5 will never
set l to 9 because the program on the right, its control abstraction ,doesnot.
In a sense which will be made explicit later in this section, each behaviour of
the abstract program provides information on an infinite subset of the possible
behaviours of the original program (the abstract program overapproximates the
concrete one).
Abstraction techniques trade convergence against completeness, and this trade-
off typically is on the incorrect side. This reflects the original aim of abstraction-
based exploration techniques, i.e., proving programs correct. Classic abstract
exploration always converges, and is void w.r.t. incorrect programs, while testing
may not converge and is void w.r.t. correct programs. The degree of complete-
ness of abstract exploration w.r.t. correct programs strongly depends on how the

l =1 ∧ x =0 → l := 2 l =1 → l := 2

[] l =1 ∧ x =0 → l := 8 [] l =1 → l := 8

[] l =2 ∧ x mod 2 = 0 → l := 3 [] l =2 → l := 3

[] l =2 ∧ x mod 2 =0 → l := 5 [] l =2 → l := 5

[] l =3 → x := x − 2 ,l := 7 [] l =3 → l := 7

[] l =5 → x := 3 x +1 ,l := 7 [] l =5 → l := 7

[] l =7 → l := 1 [] l =7 → l := 1

Fig. 5. The guarded command program from Figure 1 (left) and its control abstraction
(right)