ar
X
iv
:1
01
1.
34
07
v1
[
cs
.PL
]
15
N
ov
20
10
Reducing the Number of Annotations
in a Verification-oriented Imperative Language
Guido de Caso, Diego Garbervetsky, and Daniel Gorín
Departamento de Computación, FCEyN, Universidad de Buenos Aires
{gdecaso,diegog,dgorin}@dc.uba.ar
Abstract. Automated software verification is a very active field of re-
search which has made enormous progress both in theoretical and prac-
tical aspects. Recently, an important amount of research effort has been
put into applying these techniques on top of mainstream programming
languages. These languages typically provide powerful features such as
reflection, aliasing and polymorphism which are handy for practition-
ers but, in contrast, make verification a real challenge. In this work we
present Pest, a simple experimental, while-style, multiprocedural, im-
perative programming language which was conceived with verifiability
as one of its main goals. This language forces developers to concurrently
think about both the statements needed to implement an algorithm and
the assertions required to prove its correctness. In order to aid program-
mers, we propose several techniques to reduce the number and complexity
of annotations required to successfully verify their programs. In partic-
ular, we show that high-level iteration constructs may alleviate the need
for providing complex loop annotations.
Key words: Annotations, language design, verifiability, high-level iter-
ation constructs.
1 Introduction
Formal automated software verification regained in recent years the attention of
the community. There are at least two reasons behind this resurgent success: on
the one hand, there were crucial developments in automated theorem proving
in the last fifteen years, with SAT-solvers finally reaching industrial strength;
on the other, the focus was shifted to partial specifications which somehow over-
comes many of the objections raised in [20]. Verification of partial specifications
must be regarded as an error-detection procedure and, as such, akin to tradi-
tional forms of testing.
We will center on the particular form of verification where the source code
is annotated with special assertions. These normally take the form of method
pre and postconditions, loop and class invariants, etc. Special tools then read
these annotated sources, generate verification conditions from them and feed
these into automated provers [15]. Spec# [4] and ESC/Java [14] are two of the
best-known examples. The former is based on a dialect of C# while the latter
takes Java code with JML [17] annotations.

2 de Caso, Garbervetsky, Gorín
Apart from the abovementioned, there are ongoing research efforts in auto-
mated verification for almost every major programming language in use [6,24,23].
The rationale is to lower the adoption barrier by giving practitioners tools for
verifying the code they are writing today. Now, while this is an undeniably sen-
sible plan, we perceive that, in almost every case, the resulting “programming-
language-with-annotations” regarded as a whole ends-up being not entirely sat-
isfying. We consider next some of the reasons for this.
Lack of cohesion. Annotations are usually introduced as a “patch” to the lan-
guage. Most of the time, this is done in a way such that regular compilers and
IDE-tools regard them as mere comments. Moreover, most programming lan-
guages provide a way to perform optional run-time assertion checks. These are
usually used to validate pre and postconditions or invariants and are, thus, the
run-time counterparts of the verification annotations. But despite their dual
nature, both mechanisms have normally no syntactical relation whatsoever.
Redundancy. In statically typed languages, the type of the input and output
variables of a function are clearly part of its contract. But this means one ends-
up with two completely unrelated ways of specifying contracts: one enforced by
compilers (types) and the other by static checkers (the additional annotations).
Missed optimization opportunities. Optimizing compilers cannot leverage on pro-
gram annotations in the same way they currently do on type information.
Inadequate semantics. We can most certainly exclude “to ease automated ver-
ifiability” from the list of goals that have driven the design of most modern-
day programming languages. We cannot know for sure if today’s mainstream
languages would have been as popular without features such as complex in-
heritance mechanisms, uncontrolled method reentrancy or unrestricted aliasing.
Nevertheless, the fact that the designers of Spec# already had to diverge in
slight ways from C#’s semantics [4] is indicating, in our opinion, a new driver
for the programming languages to come.
In this paper we report on an ongoing experiment in language design. Our
language forces programmers to introduce annotations specifying their intention
when writing code. We will show that by coupling tightly the annotations with
the language semantics we can rely on a verifying compiler to infer many of the
annotations. Moreover, we find that high level iteration constructs can effectively
be used as means of reducing the annotation burden of invariants.
2 A walk-through of the Pest language
In this section we will briefly present the Pest1 programming language by way
of examples. For a formal description the reader is referred to [8].
1 After the eastern side of the Danube river in Budapest, pronounced ["pESt].

Reducing Annotations in a Verification-oriented Language 3
Pest is an multi-procedural, non-recursive, structured, while-style, imper-
ative programming language whose syntax natively incorporates various kinds
of annotations. Its main objective is to provide a test-bed for exploring new
concepts and ideas.
max(a,b,c)
:? true
:! (a ≥ b ⇒ c = a) ∧ (a < b ⇒ c = b)
:! a = a@pre ∧ b = b@pre
{
if a ≥ b then
c ← a
else
c ← b
fi
}
Fig. 1. Simple Pest procedure definition.
Figure 1 shows the definition of a simple procedure in Pest. Keywords :?
and :! introduce pre and postconditions respectively. In the postcondition a@pre
and b@pre denote the value of a and b at the beginning of the procedure exe-
cution. Therefore, this clause states that the value of a and b does not change;
this is necessary since in Pest all values are copied-in and then copied-out.
There are currently only three data types in Pest: booleans, integers and
arrays of integers. Variables are monomorphic and their type is inferred from
use. For example, in Figure 1, all variables are integers, since the ≥ operator
takes integers as arguments. Apart from classical boolean operators, boolean
expressions may include bounded first-order quantification.
Figure 2 lists a Pest procedure containing a while-loop iterating over an
array and a procedure call. Loop invariants are introduced using the :?! keyword
and exactly one loop variant must be provided, using the :# keyword. Only
variables are allowed as arguments on procedure calls and they are syntactically
enforced to be distinct. Observe that since, additionally, values are copied in
variable assignments, we impose a strict control over aliasing.
Operationally, annotations in Pest are interpreted as assertions. Roughly
speaking, preconditions are evaluated prior to procedure calls and postconditions
on return; invariants are checked before evaluating the loop guard. Since most
of the semantic rules include the evaluation of annotations, a program execution
gets stuck when the interpretation of one of them fails.
To enforce this semantics, annotations can be checked at run-time, but this
can be very expensive. Alternatively, a Pest compiler can simply remove an
assertion if it can be statically verified. In a way, this is reminiscent of type

4 de Caso, Garbervetsky, Gorín
arrayMax(A, m)
:? |A| > 0
:! ∀k / 0 ≤ k < |A| : m ≥ A[k]
:! ∃k / 0 ≤ k < |A| : m = A[k]
:! A = A@pre
{
m ← A[0]
local i ← 1
while i < |A|
:?! 1 ≤ i ≤ |A|
:?! ∀k / 0 ≤ k < i : m ≥ A[k]
:?! ∃k / 0 ≤ k < i : m = A[k]
:?! A = A@pre
:# |A| − i
do
local t ← 0
local e ← A[i ]
call max(e, m, t)
m ← t
i ← i + 1
od
}
Fig. 2. A Pest procedure containing a loop.
erasure. Of course, the programmer will normally want to be aware of which
assertions failed to be statically verified.
A Pest compiler can also infer pre and postconditions of a procedure. If only
the precondition is given a postcondition can be obtained by way of a symbolic
computation; on the other hand, starting from a postcondition, a precondition
can be obtained using a variation of the notion of weakest precondition. In simple
cases, like the procedure in Figure 1, one can remove the annotation altogether
and rely solely on inference. Details are given in §4.
Eliminating the need for explicitly given loop invariants is, of course, highly
desirable. A lot of research has been done in loop invariant inference (for in-
stance, [13,18]). In §5 we will show that higher-level iteration constructs can be
alternatively regarded as encapsulating “directives” on how to build a proper
invariant from the loop body.
Using the ideas sketched above, arrayMax can be rewritten in Pest as shown
in Figure 3 which requires no annotations for the loop and still enforces its
contract. Notice that, in addition to the invariant, in this case we are also able
to remove the precondition and part of the postcondition since they can be
inferred by the Pest compiler using the rules presented in §4.

Reducing Annotations in a Verification-oriented Language 5
easyArrayMax(A,m)
:! ∀k / 0 ≤ k < |A| : m ≥ A[k]
:! ∃k / 0 ≤ k < |A| : m = A[k]
{
m ← A[0]
for i from 1 to |A| do
local t ← 0
local e ← A[i ]
call max(e, m, t)
m ← t
od
}
Fig. 3. Using a for construct to remove annotations.
3 Formal semantics of Pest
In this section we introduce Pest semantics. In §3.1 we briefly comment on
Pest (big-step) operational semantics. As we already mentioned in the preceding
section, annotations are interpreted as assertions and a computation gets stuck
whenever one of these fails. In §3.2, we present a static formulation based on
Hoare-style clauses. This characterizes those programs that cannot get stuck
according to the operational semantics. In this sense, it is reminiscent of a type
system; but, observe that it relies on a semantic entailment relation over formulas
(|=) that is undecidable in the general case.
In this setting, automatic verification of a Pest program can be performed by
checking conformance to its static semantics using a computable approximation
(⊢) of the |=-relation. Later, in §4 we will derive some calculi from the static
semantics to cope with several inference tasks.
3.1 Operational semantics
Pest operational semantics is based on the standard notion of while-style pro-
gramming languages semantics. Annotations are handled by incorporating con-
ditions (i.e. assertions) into the semantic rules that disallow the execution of a
program that violates them.
The semantic rules are given in terms of state transformations. A state σ is
a function that maps program variables to concrete values of the proper type.
With σ{v 7→ n} we denote a state that coincides with σ except, possibly, in the
value for v which, in the former, is n; σ⊖V is the restriction of σ to a domain
that does not contain any variable in V . We use JeKσ to denote the value of an
expression e under σ.
We write σ ⊲ s ⊲ σ′ to express that a Pest sentence s, when run from state
σ, finishes correctly and arrives in state σ′. Some rules are depicted in Figure 4;
for the complete set of rules refer to [8].

6 de Caso, Garbervetsky, Gorín
JgKσ = false JinvKσ = true
σ ⊲ while g :?! inv :# var do s od ⊲ σ (O-WHILE-F)
JgKσ = true JinvKσ = true
JvarKσ > 0 σ ⊲ s ⊲ σ′
JvarKσ′ < JvarKσ
σ′⊖ locals(s) ⊲ while g :?! inv :# var do s od ⊲ σ′′
σ ⊲ while g :?! inv :# var do s od ⊲ σ′′ (O-WHILE-T)
Jpre(proc)Kρ = true
ρ ⊲ body(proc) ⊲ ρ′
Jpost(proc)Kρ′ = true
σ ⊲ call proc(cp1, . . . , cpk) ⊲ σ{cp1 7→ ρ′(p1), . . .}
(O-CALL)
where ρ(pi) def= σ(cpi) and ρ(pi@pre) def= σ(cpi)
Fig. 4. Pest operational semantics (fragment)
Consider the rules for the while statement. Observe first that if JinvKσ 6= true
then no rule applies and, thus, a computation will stick in that case. When the
guard is false, the state is not affected (the language syntax guarantees that
guards are free of side-effects). Alternatively, when the guard is true, the variant
must be above zero in order to continue. Observe that σ′ is the state after an
execution of the loop body, including locally-defined variables; if the variant
didn’t decrease the computation will stuck.
For procedure calls, state ρ binds formal and actual parameters; the precon-
dition of the called procedure must hold for this state. The state ρ′, if defined, is
the result of executing the procedure body from ρ; the postcondition must hold
in ρ′. At the end, actual parameters are updated with the final values assigned
to the formal parameters (recall that all parameters are in/out in Pest).
3.2 Hoare-style static semantics
We first need to introduce some preliminary definitions. For σ a state and b a
Pest boolean expression2, we write σ |= b if JbKσ = true. We will write b1 |= b2
to indicate that, for all σ, whenever σ |= b1 holds, then σ |= b2 must hold too
(i.e. b1 is stronger than b2).
We also require a notion of “safeness” for the evaluation of expressions. Given
an expression e, we want safe(e) to be a boolean expression such that σ |= safe(e)
implies that JeKσ is defined. For example, we expect safe(a[ i ] / y) to be the
expression “0 ≤ i ∧ i < |a| ∧ y 6= 0”. A formal definition of these conditions
is straightforward. Finally, e1⌊e2 7→ e3⌋ denotes the expression that results from
replacing every occurrence of e2 by e3 in e1. Observe that e2 and e3 must be of
the same type.
2 Throughout this section, boolean expressions are augmented with unbounded exis-
tential quantification.

Reducing Annotations in a Verification-oriented Language 7
Instead of using states like in the operational case, for the static semantics we
will use predicates (i.e. boolean expressions) that describe a (possibly infinite)
set of states. For boolean expressions p and q and s a Pest sentence, {p} s {q}
must be read “after executing s from a σ such that σ |= p, we obtain a σ′ such
that σ′ |= q”.
Figure 5 lists some of the static rules (for the complete list, refer to [8]).
Consider the rule for assignments: the first premise guarantees that the program
won’t get stuck when evaluating e; the second one states that q is a consequence
of what was known prior to the assignment (p⌊v 7→ v′⌋) and its effect (v = e⌊v 7→
v′⌋). The existentially quantified variable v′ stands for the value of v before the
assignment (this requires unbounded quantification).
p |= safe(e)
∃ v′ (p⌊v 7→ v′⌋ ∧ v = e⌊v 7→ v′⌋) |= q
{p} v ← e {q} (S-ASSIGN)
p |= safe(g)
p ∧ g |= p1 {p1} s1 {q1} q1 |= q
p ∧ ¬g |= p2 {p2} s2 {q2} q2 |= q
{p} if g then s1 else s2 fi {q}
(S-IF)
true |= safe(inv) inv |= safe(var)
inv |= safe(g) p |= inv inv ∧ g |= p′
p′ |= var > 0 {p′} var0 ← var s {q′}
q′ |= inv q′ |= var < var0 inv ∧ ¬g |= q
{p} while g :?! inv :# var do s od {q} (S-WHILE)
Fig. 5. Pest static semantics (fragment)
The premises of the rule for while can be seen as both a proof of the Funda-
mental Invariance Theorem for Loops [11] and a proof of termination using the
loop variant. The predicate p′ represents any state where the invariant and the
condition of the while hold; the loop body is augmented with an initial assign-
ment to a fresh variable var0 that is used to prove that the variant decreases.
There is a clear correlation between Pest’s operational and static semantics.
Using the latter, we can give a notion of safe program. In what follows, if π is a
program and p a procedure, then π, p is the program obtained by appending p
to π.
Definition 1 (Safe programs) The set Safe of programs is inductively de-
fined as follows:
∅ ∈ Safe (SAFE-EMPTY)
π ∈ Safe {pre(p)} body(p) {post(p)}
π, p ∈ Safe (SAFE-EXTEND)

8 de Caso, Garbervetsky, Gorín
Theorem 1 (Safe programs execute normally) Let π ∈ Safe and let p be
a procedure in π. For each σ such that σ |= pre(p), there exists a state σ′ such
that σ ⊲ body(p) ⊲ σ′ and σ′ |= post(p).
Proof. It is a longish yet straightforward induction on the length of a derivation
of {pre(p)} body(p) {post(p)}. See [8].
4 Reducing the annotation burden
In the previous section we presented the Pest programming language, including
a soundness result showing that programs conforming to Pest static semantics
do not go wrong. Still, providing Pest annotations is a heavy and complex task.
In this section we discuss two techniques that assist the programmer by inferring
and completing annotations.
4.1 Inference of procedure contracts
We will describe a technique for synthesizing procedure pre and postconditions.
To do that we will specialize the static semantic rules and turn them into infer-
ence rules. This will somehow resemble the process of developing type inference
rules from a type system.
Figure 6 shows some of the rules to compute a postcondition post(s, p) from
given p and s. The complete calculus is given in [8].
p |= safe(e)
post(v ← e, p) = ∃ v′ (p⌊v 7→ v′⌋ ∧ v = e⌊v 7→ v′⌋) (Q-ASSIGN)
p |= safe(g)
post(if g then s else t fi, p) =
Cl∃ locals(s)(post(s, p ∧ g)) ∨ Cl∃ locals(t)(post(t, p ∧ ¬g))
(Q-IF)
true |= safe(inv) inv |= safe(var)
inv |= safe(g) p |= inv inv ∧ g |= var > 0
post(var0 ← var s, inv ∧ g) = q′
q′ |= inv q′ |= var < var0
post(while g :?! inv :# var do s od, p) = inv ∧ ¬g (Q-WHILE)
Fig. 6. Pest postcondition calculus (fragment)
Observe the way in which these rules specialize those in Figure 5. For exam-
ple, in the specialized rule for assignments, post(v ← e, p) is simply the strongest

Reducing Annotations in a Verification-oriented Language 9
q satisfying the original assignment rule. The rule for if eliminates (using an ex-
istential closure3) the local variables defined in each of the branches from their
respective inferred postcondition.
It is worth noticing that the inferred postcondition may contain unbounded
existential quantifications. The main drawback of this is that, in that case, it
is not valid to literally include it in the code. Observe also that an assertion
with unbounded quantification cannot be checked at runtime; nevertheless, the
inferred postconditions are correct by construction and the compiler can omit
its associated runtime checks.
A similar approach can be used to infer procedure preconditions (denoted
pre(s, q)). In this case, we use weakest-preconditions to find a suitable predicate
p, except for while sentences where we simply use the provided invariant. The
rules for computing pre(s, q) can be found in [8].
Interestingly, we can infer non-trivial pre and postconditions even if the pro-
grammer provides no procedure annotations (other than loop annotations). First,
we infer a predicate that guarantees the normal execution of a procedure body
s:
P def= pre(s, true)
This gives us a proper precondition for the procedure. Next, we strengthen P
by giving a symbolic initial value to each parameter (pi = pi@pre) and use it
to infer a postcondition Q:
Q def= post(s, P ∧ p1 = p1@pre ∧ . . . ∧ pk = pk@pre)
The reader should verify that if the pre and postconditions of the procedures
in Figures 1 and 2 are omitted, this procedure will infer logically equivalent ones.
4.2 Strengthening annotations
We will now show how we can take advantage of Pest’s restrictions on variable
aliasing to incorporate inexpensive enhancements of invariants and postcondi-
tions. In a nutshell, we can propagate known facts about variables in certain
scopes if we know that their contents are not altered. For example, let us say we
know that before entering a loop it is always the case that variable j has value
e; then if we can determine that the loop body does not update j, we can add
j = e to the invariant.
In the absence of aliasing, a simple, sound approximation of the set of unmod-
ified variables is to compute first the set of variables potentially modified and
then take its complement. We call modVars(s) the set of (potentially) modified
variables; its definition is straightforward and can be found in [8].
What follows is a definition of our annotation strengthening function which
takes a sentence s and an entry point p and produces a sentence s′ with possibly
3 The existential closure of a boolean expression b with respect to a set of variables
{v1, . . . , vn} is ∃v1, . . . , vn(b)

10 de Caso, Garbervetsky, Gorín
1 ≤ i ≤ |A| ∧ ∀k / 0 ≤ k < i : m ≥ A[k] ∧ ∃k / 0 ≤ k < i : m = A[k] ∧ A = A@pre
∀k / 0 ≤ k < |A| : m ≥ A[k] ∧ ∃k / 0 ≤ k < |A| : m = A[k] ∧ A = A@pre
Fig. 7. Invariant and postcondition of the main loop in the arrayMax procedure.
Differences are highlighted.
strengthened annotations. The translation does not alter assignments, local vari-
able definitions or procedure calls. In the case of sentence sequence, we define it
as:
trS(s1 s2, p) def= s′1 trS
(
s2, post(s′1, p)
)
where s′1 = trS(s1, p). That is, we first translate s1 and use its postcondition to
translate s2.
When dealing with conditional statements we proceed by translating each
branch using the conjunction of p with the guard g:
trS(if g then s1 else s2 fi, p)
def
=
if g then trS(s1, p ∧ g)
else trS(s2, p ∧ ¬g) fi
Finally, in the presence of a loop we strengthen its invariant. We existentially
close p over the variables that are potentially modified by the loop body:
trS(while g :?! inv :# var do s od, p) def= while g :?! I :# var
do trS(s, I ∧ g) od
where I = inv ∧ Cl∃modVars(s)(p).
Using this technique we can strengthen both invariants and postconditions.
For the latter case we simply take the postcondition of the last instruction of
the procedure and existentially eliminate the local variables, in order to leave
the postcondition only in terms of procedure parameters.
5 High-level iteration constructs as annotations
In this section we focus on what we call “high-level iteration constructs”. These
capture recurrent iteration patterns and are frequently included in programming
languages to reduce error-prone boilerplate code. Examples of such constructs
are Pascal-style for -loop and C#’s foreach. We will see next that this kind
of constructs can be seen as implicitly carrying their own proof obligations,
reducing the need for explicit annotations.
5.1 The for construct
We first consider the Pascal-style for loop and take as motivating example the
arrayMax procedure in §2. In Figure 7 we compare the postcondition of the loop
with its invariant. Clearly, they are syntactically very close. In fact, if we are given

Reducing Annotations in a Verification-oriented Language 11
arrayInc(A)
{
local i ← 0
while i < |A|
:?! 0 ≤ i ≤ |A|
:?! ∀k / 0 ≤ k < i : A[k] = A@pre[k] + 1
:?! ∀k / i ≤ k < |A| : A[k] = A@pre[k]
:# |A| − i
do
A ← update A on i with A[i] + 1
i ← i + 1
od
}
Fig. 8. Pest procedure that increases each element in an array.
a postcondition and a for -loop, we can simply try to guess a candidate invariant
for the loop without even considering the loop body. Of course, the correctness
of the invariant will have to be statically verified. On the other hand, a correct
variant can be trivially obtained.
Formally, given a sentence of the form for i from l to h do s od (without
annotations) and its postcondition in the form of a predicate Qf , we can macro-
expand the sentence into the following lower-level code:
local i← l
while i < h
:?! l ≤ i ≤ h ∧ Qf⌊h 7→ i⌋
:# h− i
do
s
i ← i+ 1
od
In order to apply this expansion we are required to provide a loop postcondi-
tion Qf . Nevertheless, this can be accomplished using the precondition calculus
of §4.1 from the procedure postcondition up to the for -sentence we need to ex-
pand. If s contains a nested for -construct, a postcondition for it can be derived
from the inferred invariant and the expansion can be recursively applied.
Observe that in the easyArrayMax procedure of Figure 3, Qf is simply the
postcondition of the procedure, since the for construct is located at the very end
of the procedure body.
5.2 Declarative iteration constructs
In §4.1 we saw that if the loop-invariants are provided, then postconditions can
be omitted; conversely, in the previous section we showed that in the case of for -
loops invariants can be traded for postconditions. In this section we will show

12 de Caso, Garbervetsky, Gorín
that when more specific iteration constructs are used, both can be dispensed
with. We will only consider here the map-construct (reminiscent of the map
function over lists in functional languages) but the idea is easily extensible to
other constructs.
Consider the procedure of Figure 8 (notice that the procedure contract was
omitted and left for automatic inference). The loop iterates over an array A using
an indexing variable i. On each iteration, only the element of A at position i is
updated. Furthermore, this is done taking into account only the value of i and
A[i]. The loop condition is not affected by changes to A. We call this iteration
pattern, in which array elements are updated independently of the others, a map.
The invariant for this iteration pattern states that the already visited array
elements were updated whereas the remaining elements are unchanged. The
variant reflects the fact that the array is traversed in a forward direction.
Using our proposed map construct, the procedure in Figure 8 can be written
like this:
arrayInc(A)
{
map
A[i ] ← A[i ] + 1
in A[.. i ..]
}
Formally, this works as follows. Let A be an array, i a fresh variable and s a
sentence such that modVars(s)r locals(s) = {A} and A is accessed only indexed
by i. In that case, map s in A[.. i ..] is well-formed and gets expanded as follows:
local i ← 0
while i < |A|
:?! 0 ≤ i < |A|
:?! ∀k / 0 ≤ k < i : posts⌊i 7→ k⌋
:?! ∀k / i ≤ k < |A| : A[k] = A@pre[k]
:# |A| − i
do
s
i ← i + 1
od
where posts = post(s, 0 ≤ i < |A|). It can easily be seen that the inferred
invariant is always correct. Thus, not only can the compiler erase the assertion
checks, it doesn’t even need to statically verify them.
Notice that the invariant inferred for the map high-level construct can be
further strengthened using the technique presented in §4.2.

Reducing Annotations in a Verification-oriented Language 13
6 Experience
In order to test these ideas we developed a tool called BudaPest which is
available online4 as an Eclipse plug-in.
The tool takes Pest programs, statically verifies them and compiles them to
Java code. For the verification step the code is translated into an intermediate
assume/assert style language similar to BoogiePL [9]. Unlike the Boogie verifier,
our tool leverages the structure of the original program to discharge verification
conditions one by one to SMT-solvers, such as CVC3 [5], Yices [12] and Z3 [2].
We split verification conditions in several pieces in order to allow the provers to
work in parallel, so we can leverage each of the provers’ power and combine their
results. Splitting verification conditions also has the advantage of enabling early
detection (during the verification process) of unsatisfiable conditions since once
a subformula fails there is no need to continue with the rest of the subformulas.
We tested the usability of this tool in a first-year Computer Science course.
The curriculum of the course includes proving correctness and termination of
simple imperative programs specified using contracts written in a fragment of
first-order logic and proven by way of Hoare axiomatic semantics [16]. With the
aid of the tool they were able to automatically verify the correctness of their
implementations of algorithms such as bubble and insertion sorting, linear and
binary search, etc., which they previously had to do by hand.
The experience was very encouraging for the students since they found that
concepts they had learnt during the course (preconditions, postconditions, in-
variants, variant functions) could be applied in “real” applications and produced
code with guarantees of (partial) correctness and termination.
Finally, it is worth mentioning that the integrated nature of the Pest lan-
guage forced the students to concurrently think about both the statements
needed to implement an algorithm and the assertions required to prove its cor-
rection.
7 Related Work
There is a plenty of research on the automatic verification of programs. Due to
lack of space we will just mention some of those we consider closer to our work.
There are several languages and tools that incorporate Hoare-style specifica-
tions to automatically prove partial correctness in imperative languages. Some
well known examples are ESC/Java [14], JML [17], ESC/Modula-3 [10],
Spec# [4] and SPARK/Ada [3]. These systems enrich the language with user
provided annotations which can be checked on runtime or statically analyzed by
generating verification conditions that are discharged to a theorem prover.
The approach followed by SPARK/Ada is closer to ours in the sense that
they impose limitations to the language in order to make verification possible. We
believe they go too far since they limit syntactically to programs where assertions
4 http://lafhis.dc.uba.ar/budapest

14 de Caso, Garbervetsky, Gorín
are decidable, making them too restrictive. On the contrary, the problem with
the other tools is that they deal with complex languages that provide many
features such as polymorphism, concurrency, aliasing or reflection, which are
comfortable for program development but complicate verification.
Our work follows the philosophy that a compiler (or interpreter) should try
to reject misbehaving programs. This is similar the approach followed by sev-
eral languages that provide expressive type systems such as Deputy [7], which
uses dependent types [19] to type-check low level imperative programs. For func-
tional languages there are many proposals; just to name one, Cayenne [1] ex-
tends Haskell with dependent types. Recently, [21] presented a type theory for
higher order functional programs which incorporates Hoare style specifications
into types, making it possible to enforce correct use of side effects.
8 Final thoughts
In this paper we presented Pest, a simple imperative programming language,
which was designed with verifiability in mind. We proposed a series of tech-
niques that aim at mitigating the annotation burden required to verify programs.
Firstly, we showed an inference mechanism for procedure pre and postconditions
and then a simple method to strengthen loop invariants and postconditions.
As a distinguishing contribution we extended Pest with high-level iteration
constructs that allow programmers to dramatically reduce annotations and yet
maintain the ability to prove correctness of relatively complex pieces of soft-
ware. Our first experiences showed that an integrated approach such as ours
was gracefully adopted by young students with no pre-concepts with respect to
programming languages or tools.
We would like to explore, in the near future, the possibility of extending
Pest incorporating features that would increase its expressiveness without sac-
rificing verifiability. We plan to allow the programmer to define and use her own
data types and provide means to reason about representation invariants. Adding
dynamic memory support is another priority but, in order to keep a verifiable
language, we believe we must enforce an alias control mechanism such as [22].
Finally, we are interested in providing the means for programmers to define their
own language constructs by feeding the BudaPest tool with syntax and macro
expansion definitions, and relying on the base tools (i.e. pre and postcondition
calculi) that we provided in this paper to ensure correctness.
References
1. L. Augustsson. Cayenne-a language with dependent types. ACM SIGPLAN No-
tices, 34(1):239–250, 1999.
2. T. Ball, S. K. Lahiri, and M. Musuvathi. Zap: Automated theorem proving for
software analysis. In LPAR, 2005.
3. J.G.P. Barnes and Praxis Critical Systems Limited. High Integrity Ada: The
SPARK Approach. Addison-Wesley, 1997.

Reducing Annotations in a Verification-oriented Language 15
4. M. Barnett, K.R.M. Leino, and W. Schulte. The Spec# Programming System: An
Overview. In CASSIS. Springer, 2005.
5. C. Barrett and S. Berezin. CVC Lite: A new implementation of the cooperating
validity checker. In Proceedings of the 16th CAV, 2004.
6. S. Chatterjee, S.K. Lahiri, S. Qadeer, and Z. Rakamaric. A reachability predicate
for analyzing low-level software. 2007.
7. J. Condit, M. Harren, Z. Anderson, D. Gay, and G.C. Necula. Dependent Types
for Low-Level Programming. Lecture Notes in Computer Science, 4421:520, 2007.
8. G. de Caso, D. Garbervetsky, and D. Gorín. Pest formal specification. Tech-
nical report, Universidad de Buenos Aires, http://lafhis.dc.uba.ar/budapest/
Theory section, 2008.
9. R. DeLine and K.R.M. Leino. BoogiePL: A typed procedural language for checking
object-oriented programs. Technical report, Technical Report MSR-TR-2005-70,
Microsoft Research, 2005.
10. D. L. Detlefs, K.R.M. Leino, G. Nelson, and J.B. Saxe. Extended static checking.
Technical Report #159, Palo Alto, USA, 1998.
11. E.W. Dijkstra. A Discipline of Programming. Prentice Hall PTR Upper Saddle
River, NJ, USA, 1997.
12. B. Dutertre and L. de Moura. The Yices SMT solver. Available at
http://yices.csl.sri.com/, August, 2006.
13. M.D. Ernst, J.H. Perkins, P.J. Guo, S. McCamant, C. Pacheco, M.S. Tschantz, and
C. Xiao. The Daikon system for dynamic detection of likely invariants. Science of
Computer Programming, 2007.
14. C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata.
Extended static checking for Java. In PLDI ’02, 2002.
15. D.I. Good, R.L. London, and WW Bledsoe. An interactive program verification
system. In Proceedings of the international conference on Reliable software table
of contents, pages 482–492. ACM New York, NY, USA, 1975.
16. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM,
12(10):576–580, 1969.
17. G.T. Leavens, A.L. Baker, and C. Ruby. JML: A notation for detailed design.
In Behavioral Specifications of Businesses and Systems, pages 175–188. Kluwer
Academic Publishers, 1999.
18. K. Rustan M. Leino and Francesco Logozzo. Loop invariants on demand. In
APLAS, pages 119–134, 2005.
19. J. McKinna. Why dependent types matter. Proc. ACM Symp. on Principles of
Programming Languages (POPL 2006), 2006.
20. R.A. De Millo, R.J. Lipton, and A.J. Perlis. Social processes and proofs of theorems
and programs. Commun. ACM, 22(5):271–280, 1979.
21. A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and separation in hoare
type theory. In ICFP ’06, 2006.
22. J. Noble, J. Vitek, and J. Potter. Flexible alias protection. In ECOOP ’98: Pro-
ceedings of the 12th European Conference on Object-Oriented Programming, pages
158–185, London, UK, 1998. Springer-Verlag.
23. N. Norwitz. PyChecker. SourceForge project http://pychecker. sourceforge. net.
24. D.N. Xu. Extended static checking for Haskell. In Proceedings of the 2006 ACM
SIGPLAN workshop on Haskell, pages 48–59. ACM New York, NY, USA, 2006.