Information Technology Reference
In-Depth Information
procedure
Max(N
:
int
,a
:
[
int
]
int
)
returns
(max
:
int
)
1
∀
j
:
int
•
≤
j
∧
j<N
=
⇒
a[j]
≤
max);
ensures
(
0
2
∃
j
:
int
•
≤
j
∧
j<N
∧
a[j]
=
max);
ensures
(
0
3
{
4
var
i
:
int
;
5
i
:=
0;
6
max
:=
0;
7
while
(i<N){
8
if
(a[i] > max) { max
:=
a[i]; }
9
i
:=
i+1;
10
}
11
}
12
Fig. 1.
Boogie procedure
Max
that finds the maximum element in an array. Both the specification
and the implementation contain errors, and no loop invariant is provided.
or specification that require further attention. We also identify a subset of the annotation
language for which no infeasible executions are generated.
We implemented our technique for the Boogie intermediate verification language,
used as back-end of numerous program verifiers [18,4,26]. Working atop an inter-
mediate language opens up the possibility of reusing the tool with multiple high-
level languages and verifiers that already translate to Boogie. It also ensures that
our technique is sufficiently general: Boogie is a small yet very expressive lan-
guage (including both specification and imperative constructs), designed to support
translations of disparate notations with their own supporting methodologies. Our im-
plementation is available as a tool called Boogaloo, distributed as free software:
https://bitbucket.org/nadiapolikarpova/boogaloo/
and accessible through the
we will use “Boogaloo” to denote the execution generation technique as well as its
implementation, and will employ the self-explanatory Boogie syntax in the examples.
2
Illustrative Example
We give a concise overview of the capabilities of Boogaloo using a simple verification
example: finding the maximum element in an integer array.
1
Fig. 1 shows a straight-
forward Boogie implementation as procedure
Max
, which inputs an integer
N
, denoting
the array size, and a map
2
a
that represents the array elements
a[0]
,
...
,
a[N-1]
;it
returns an integer
max
for
a
's maximum. The Boogie procedure includes specification
in the form of two postconditions (
ensures
), formalizing the definition of maximum:
max
should be no smaller than any element of
a
(line 2); and it should be an element of
a
(line 3).
What happens if we try to verify procedure
Max
, as shown in Fig. 1, using Boogie?
Verification fails with a vague error message (“
Postconditions on lines 2 and
3
1
The tool output messages in this section are abridged without sacrificing the gist of the original.
2
In general, maps have an infinite domain in Boogie.
