Information Technology Reference
In-Depth Information
more complex than
Max
, we need to express abstract properties potentially involving
infinitely many elements, such as for framing and for reasoning about unbounded se-
quences of pointers to heap-allocated data. Even in an example as simple as sorting,
if a sorting procedure takes a function pointer as argument to denote the comparison
function, we need to express that it encodes a total order—something involving quan-
tification over a potentially unbounded domain. More generally, we designed Boogaloo
to work with the same proof-oriented annotated programs used by static verifiers, which
involve features difficult to execute and normally not found in high-level programming
languages.
Another option to debug
Max
is using the Boogie Verification Debugger (BVD [14]),
which extracts concrete counterexamples from failed verification attempts. The rele-
vance of such counterexamples is, however, limited in the presence of loops and proce-
dure calls with incomplete specifications. On
Max
as in Fig. 1, BVD returns the assign-
ment “
N = 1, a = [], max = -900
”; after adding
N>0
as precondition, it returns “
N
= 797, a = [], max = -900
”; after fixing the implementation, it returns “
N = 797,
a = [0 -> -901], max = -901
”. These examples fail to point out the two errors in
Max
, because according to modular reasoning [17] and in the absence of an invariant,
any loop is equivalent to assigning arbitrary values to program variables. While BVD's
modular semantics helps debug incompleteness in specifications, it also enforces an
“all-or-nothing” development style, where developers first have to get right the most
complicated part (the invariants), before they can proceed with debugging the rest of
the program. This lack of incrementality is what makes modular verification so hard in
the first place.
It is possible to make Boogie use loop and procedure bodies instead of their specifi-
cation by
unrolling
loops and
inlining
procedures
U
times, for a given
U
≥
0. With un-
U
, and in particular the
same counterexamples constructed by Boogaloo. The approach, however, has its limi-
tations. First, unrolling and inlining require users to guess a suitable
U
; since all longer
executions are ignored, verification vacuously succeeds when the shortest counterexam-
ple requires
>U
iterations or nested calls, without providing any concrete feedback.
Second, unrolling of complex loops and inlining of recursive procedures scale poorly,
as they consist of literally rewriting the code
U
times; Boogaloo, in contrast, uses sym-
bolic execution techniques, which are less likely to incur blow up. Building a debugger
on top of the Boogie verifier also means that it cannot generate passing executions
(Boogie does not produce a model in case verification succeeds) and cannot help when
the theorem prover gets bogged down. In contrast, Boogaloo uses simpler verification
conditions, designed for predictable generation and readability of counter examples as
opposed to sound proofs.
≤
rolling, BVD finds counterexamples for executions where
N
3
A Runtime Semantics of Boogie Programs
This section describes the syntax of Boogaloo programs (Sec. 3.1) and their opera-
tional semantics (Sec. 3.2). We use the following notation:
Z
is the set of mathe-
matical integers; and
of Boolean values. A
map
m
is a math-
ematical function from a domain
D
1
×···×
B
is the set
{
,
⊥}
D
n
,for
n
≥
0, to a codomain
D
0
;
