Information Technology Reference
In-Depth Information
Ta b l e 1 .
Programs tested with Boogaloo: name, main features, lines of code, number of specifica-
tion functions, annotations (
axiom
s
A
,
assert
s
S
,
assume
s
U
,
requires
R
,
ensures
E
,
loop
invariant
s
I
), time to generate passing executions, time to generate failing executions
for the buggy version. Times in seconds, rounded to the nearest integer: for a given input size
N
,
time
t
Σ
with fully symbolic execution and
t
C
with concretization.
∞
denotes a timeout of 180
seconds.
PROGRAM
FEATURES
LOC
FUN
ANNOTATIONS
TIME
BUG
AS UREIN
Σ
t
C
N
Σ
t
C
ArrayMax
see Sec. 2
33
0
0
0
1
1
2
1
26
4
0
000
ArraySum
recursive definition
34
1
0
0
1
1
1
2
26
75
2
100
BinarySearch
complex precondition
49
1
0
0
2
2
3
2
26
2
0
000
BubbleSort
complex postcond. and inv.
74
1
0
0
2
1
4
5
6 0 1200
DutchFlag
user-defined types [6]
96
3
0
0
2
2
8
6
7
132
43
100
Fibonacci
recursive procedure
40
1
3
1
0
2
0
0
11
88
0
000
Invert
complex pre- and postcond.
37
0
0
0
3
3
2
1
9
19
118
202
LinkedListTraversal
heap model
49
3
2
0
0
1
1
1
8 0 4200
ListInsert
see [14]
52
1
0
0
2
1
1
0
6 8 5100
QuickSort
helper and recursive proc.
89
3
0
0
2
1
6
0
3412
∞
0
∞
QuickSort PI
partial implementation
79
3
0
0
2
2
9
0
4
64
210
TuringFactorial
unstructured control flow
37
1
2
5
0
1
1
0
11
1
0
300
Split
linear arithmetic [13]
22
0
0
0
0
1
3
0
-00
SendMoreMoney
fixed-size array constr. [12]
36
1
0
0
15
0
0
0
-22
Primes
recursive definition [12]
31
2
0
0
0
0
2
0
874
NQueens
variable-size array constraints
37
2
1
0
3
0
0
0
11
45
1
variant of QuickSort whose partitioning procedure has a complete pre- and postcondi-
tion but no implementation. This may represent an intermediate development step where
we want to validate the overall logic of QuickSort before proceeding with implement-
ing the partitioning procedure. Boogaloo simulates array partitioning based only on its
specification—something unachievable with traditional testing techniques. The injected
bugs are mostly off-by-one errors and missing preconditions, both of which frequently
occur in practice; the bugs in BinarySearch are among those found in textbooks [22].
Declarative Programming.
The other four examples come from previous work on con-
straint programming and code synthesis [13,12], and involve linear arithmetic, recur-
sively defined functions, and quantification over variable-sized arrays. Constraints are
declared using
assume
statements or procedures without implementation; Boogaloo
generates program outputs satisfying the constraints.
Experimental Results.
All problems in Tab. 1 but two include a parameter
N
that de-
fines the input size (the input array or list for most problems). Column
TIME
displays
the value of
N
used in the experiments; and the time required to generate a passing
execution with different concretization strategies:
t
Σ
corresponds to fully symbolic ex-
ecutions where the state is concretized only once after terminating;
t
C
, instead, corre-
sponds to executions where the state is concretized before every jump statement. Col-
umn
BUGGY
displays the same time measures for the buggy programs; for these, the
value of
N
corresponds to the input size exposing the bug found by Boogaloo (which
is the smallest possible for all programs). In all experiments we imposed a timeout of
180 seconds, to reflect the expectation to use Boogaloo with good responsiveness.
Concretizing before jumping generally leads to faster executions, even with an
order-of-magnitude difference. This strategy may lead to heavy backtracking when the
constraints on a given logical variable are imposed incrementally, with one or more con-
cretization points in between, producing potentially lengthy combinatorial enumerations.
