DAReing to reduce the annotation overheads of verified programs

TL;DR

This paper introduces DARe, a tool that automatically reduces annotation overhead in verified programs, significantly decreasing guidance needed for the Dafny verifier and potentially simplifying program verification workflows.

Contribution

The paper presents DARe, a novel tool that automatically removes unnecessary annotations in Dafny programs, reducing verification guidance by up to 88%.

Findings

88% of guidance can be removed from verified programs

DARe is integrated with the Dafny IDE

Applied to 252 programs from the Dafny library

Abstract

Modern program verifiers use the same uniform program text to both specify and implement programs. The program text is also used to provide the necessary guidance to ensure that the program satisfies its specification. The amount of guidance required is often called the annotation overhead. This can be high and is often seen as a hindrance for wider use of program verifiers, as development time is increased and the guidance may obfuscate the program text. In this paper we introduce the DARe tool, which automatically removes as much unnecessary guidance as possible for the Dafny program verifier. The tool is integrated with the Dafny IDE. To evaluate DARe, we apply it to 252 programs from the Dafny library and analyse the degree to which it is able to remove unnecessary guidance. Our results are very encouraging as a staggering 88% of the guidance can be removed.

Full text

0.1 Introduction

Users of modern auto-active program verifiers, such as Spec# [4], VCC [9], Verifast [22], Dafny [25], and SPARK 2014 [30], use the program text to encode: (i) the program specification, (ii) the program implementation, and (iii) the proof guidance to ensure that the program satisfies the specification.

The advantage of these techniques, compared with interactive theorem provers such as Isabelle [35] or Coq [5], is that both programs and proofs are developed in the same language, and using constructs more familiar to software engineers. Thus, a developer does not need to learn to use an additional system.

The ratio of the number of lines of specification and annotations (LoA) to the number of lines of code (LoC) is called the annotation overhead. For non-trivial programs this ratio can be high, for example [38] reported on $4.8$ LoA per LoC. Such a high degree of annotations may obfuscate the program text and act as a hindrance for mainstream uptake of the technique beyond niche markets. There are at least two reasons why stated annotation overheads may be too high:

Annotations are normally added incrementally to the program text until a proof is found. Previous increments may or may not have helped to progress the proof. Instead of attempting the (possibly time consuming and tedious) task of manually “tidying up” these annotations, a developer may be satisfied that the job is done. This scenario will be illustrated in §0.2. 2. 2.

The underlying verifier is improved such that guidance that used to be required is no longer needed. Periodic “tidying” annotations of existing libraries may be too time consuming for a developer, in particular if this has to be done manually.

In this paper we present the DARe tool (Dead Annotations Removal), which automatically removes annotations that are superfluous (or dead111Inspired by the term used for “dead code” we call them “dead annotations”.) for the Dafny program verifier. To investigate how useful this tool is, and thus the degree to which annotations are superfluous, we empirically evaluate the program using examples from the Dafny library and test suite [1]. For usability purposes, we investigate the impact DARe has on runtime, and embed it in the Dafny IDE for Visual Studio [28]. This requires instant feedback and we therefore investigate and compare algorithms that are either simple, complete or fast.

0.2 Proofs & programs in Dafny

Dafny is an imperative, object-oriented and functional programming language that has been designed for verification. Properties that have to be satisfied are commonly specified by contracts: given a precondition that a method can assume, it must guarantee that a given postcondition holds. Special proof constructs, together with standard programming constructs, are used to provide guidance to ensure that the contract holds. To verify a program, Dafny translates it into an intermediate verification language (IVL)222An IVL can be seen as a layer to ease the process of generating new program verifiers. called Boogie [3]. From Boogie a set of verification conditions (VCs) is generated and applied to the Z3 SMT solver [32]. If it fails, then the failure is translated back to the Dafny code, via Boogie.

0.2.1 Assertions & lemma calls

The simplest form of annotation is the use of assert statements in the code. An assertion must be verified, and will subsequently be used by the prover. Dafny also supports a ghost state. From a programming point of view, working in the ghost state is exactly the same the non-ghost state. The difference is that it is only used for verification and will not be compiled. To illustrate, a ghost variable v is declared as ghost var x, and then used like a normally variable.

A lemma is a ghost method, i.e. a method that is in the ghost state (including all its local variables). It is therefore only used for verification purposes. Lemmas are used for more complex assertions that require guidance in order to be verified. A lemma contract specifies the desired property, while the method body encodes the proof guidance. To illustrate, consider the following lemma and associated proof by contradiction [14]:

⬇

1 requires x in A $\land$ A * B $=$ {}

2 ensures $\lnot$(x in B)

3{

4 if x in B {

5 assert x in A * B;

6 set_eq_simple(A*B,{},x);

7 assert x in {};

8 assert false;

9 }

10}

The lemma states that if a given variable x is a member of the set A, and the sets A and B are disjoint (their intersection A*B is empty), then x cannot be in set B.

We will now illustrate how this proof was found, and use \blacktriangleright$$\ldots$$\blacktriangleleft to highlight where Dafny reports that the error is. The proof in the lemma body started by setting up the contraction using an if-statement:

⬇

$\blacktriangleright$ $\blacktriangleleft$

}

Dafny will translate the lemma with this body to Boogie, which will generate a set of VCs that are applied to the Z3 SMT solver. One of the VCs fails, and Boogie relates that to the post-condition not being satisfied for the case where x in B. The error is then highlighted inside this case within the Dafny IDE, as illustrated above. As only this case is highlighted we know that Dafny can prove the property when (x in B)!, which is unsurpricing considering that this is the same as the postcondition. For the problematic x in B case, more guidance is required in the program text.

We then continued developing the proof by asserting that x is in the intersection of A and B (x in A * B), which is trivial to prove as we know x in A fromt a precondition and that x in B from the condition of the if statement. We also add the contradiction we are deriving (line 8 of set_inter_empty_contr). Dafny then highlights the following mistake:

⬇

**assert** x **in** A * B;

$\blacktriangleright$ assert false; $\blacktriangleleft$

}

Here, Dafny report that the last assertion (assert false) cannot be proven. It does not complain about the first assertion, which means that it can be verified. Moreover, it no longer complain about the postcondition, meaning that it can be derived from the last assertion (which we still need a proof of). We then add the assertion from line 5, from which we can derive false:

⬇

**assert** x **in** A * B;

$\blacktriangleright$ assert x in {}; $\blacktriangleleft$

**assert** **false**;

}

We now see that Dafny can infer the contradiction, but needs help to show that x in {}. To bridge this line to the previous line, we add a call to lemma set_eq_simple (line 6). This lemma states that if x is in A*B then x is in {}:

⬇

requires x in A $\land$ A $=$ B

ensures x in B

{ }

This lemma is proven automatically (as the body is empty). The proof is now complete.

0.2.2 Loop invariants & variants

Loop invariants express properties that have to hold throughout the execution of a loop, and are normally required for any program that contains a loop. Dafny methods and loops must terminate (with one exception discussed in §0.3). For simple cases, Dafny can prove this automatically; for more complex cases, the developer must provide an expression, called a variant333Other names for variants include rank functions or decrease clauses., which for each step has to decrease towards a lower bound.

To illustrate, consider the following implementation of binary search over an array, which returns the index where the value is, or returns -1 when the search fails to find the value [1]:

⬇

1 requires a $\neq$ null $\land$ 0 $\leq$ a.Length $\land$ sorted(a)

2 ensures 0 $\leq$ index $\Longrightarrow$ index < a.Length $\land$ a[index] $=$ value

3 ensures index < 0 $\Longrightarrow$ $\forall$ k $\bullet$ 0 $\leq$ k < a.Length $\Longrightarrow$ a[k] $\neq$ value

4{

5 var low, high :$$= 0, a.Length;

6 while low < high

7 decreases high - low

8 invariant 0 $\leq$ low $\land$ low $\leq$ high $\land$ high $\leq$ a.Length

9 invariant $\forall$ i $\bullet$ 0 $\leq$ i < a.Length $\land$ $\lnot$(low $\leq$ i < high) $\Longrightarrow$ a[i] $\neq$ val

10 {

11 var mid :$$= (low + high) / 2;

12 if a[mid] < value {

13 low :$$= mid + 1;

14 } else if value < a[mid] {

15 high :$$= mid;

16 } else {

17 return mid;

18 }

19 }

20 return -1;

21}

The contract specifies the desired properties, and a while loop is used to implement it. Lines 8 and 9 have a loop invariant that the developer has to provide to help the prover verify that the implementation indeed satisfies the contract. In addition, a variant is provided (line 7), which states that high - low, meaning that the difference between high and low is reduced for each step of the loop.

0.2.3 Calculations

The proof of set_inter_empty_contr is a linear sequence of arguments: from x in A * B it implies that x in {}, which implies false. The first implication is justified by a call to set_eq_simple(A*B,{},x).

Dafny supports such calculational proofs via the calc statement [27], which is inspired by Dijkstra’s way of writing calculuations [11]. Using calculations, the body of set_inter_empty_contr can instead be written as:

⬇

1 calc {

2 x in A * B;

3 $\Longrightarrow$ { set_eq_simple(A*B,{},x);}

4 x in {};

5 $\Longrightarrow$

6 false;

7 }

8 }

On line 1 a calculation is started, while line 2 gives the starting statement that x in A * B. This implies (line 3) that x in {} (line 4), justified by the lemma call set_eq_simple(A*B,{},x) (line 3). Then, x in {} (line 4) implies (line 5) false (line 6). This last step can be proven automatically, so Dafny does not require any further justification/hints.

Note that there are multiple ways of writing such calculations. For example, we can state that by default, arguments are chained by an implication, and thus omit it for each step:

⬇

1 calc $\Longrightarrow${

2 x in A * B;

3 { set_eq_simple(A*B,{},x);}

4 x in {};

5 false;

6 }

7 }

We return to calculations in §0.3.

0.3 The DARe approach to dead annotation removal

0.3.1 A motivating example

Let us return to the proof of the set_inter_empty_contr lemma, and recall how we worked with the system by incrementally adding annotations until a proof was found. At the end of the proof, we do not know which steps were required, with the exception of the last step that was added. One way to find the steps that were required is to remove the added annotations one-by-one and see if the proof still holds. If we do this we will see that none of the annotations except the last lemma call were needed (i.e. lines 4,6 and 7). The body of the lemma can therefore be simplified to:

⬇

set_eq_simple(A*B,{},x);

}

In the rest of the paper we describe and evaluate the DARe tool to automate this process. First we will describe what constitutes an annotation.

0.3.2 Specification vs program vs proof guidance

When removing annotations manually, as we did above, it is normally straightforward for the developer to separate annotations that are only used to guide the prover (which can be removed) from specification elements (which should be kept). However, it is not that easy to formalise this relationship so that it can be understood by a computer. For example, Dafny uses many of the same constructs for both proof and programming; e.g. the proof of the set_inter_empty_contr lemma is really just a program. Moreover, annotations are sometimes used to help explain a correctness argument, which is desirable to keep. In order to develop a tool that automatically removes dead annotations, we have to decide upon what constitutes an annotation that can be removed. We detail our choices next. Some may disagree with them, and in the future we plan to empirically evaluate these choices (§0.8). Note that the DARe tool (§0.4) is modular and can easily be updated to incorporate such changes.

We consider all assertions, lemma calls, invariants and variants to be annotations that can be removed. From our experience, this is normally the case. We keep the lemmas, even if all calls to them are removed. We do not consider common programming constructs, such as variable declarations, assignments, loops and conditionals, to be proof guidance, even if they are in the ghost state. These are therefore kept. This is something we will revisit in the future. We consider contracts to be specification. This is not always the case: for example, one can implement iteration using recursive functions. Here, a “loop invariant” is encoded using preconditions and postconditions. In this case, contracts become proof guidance, but we cannot (syntactically) separate them from the actual contracts that specify the program. In the future we may extend our work to weaken preconditions444Dual to weakening a precondition is to strengthen a postcondition. However, this does not fit our ethos of simplifying the program text by removing elements., which will require global analysis. Finally, calculations are considered to be annotations used for proof guidance.

We can now define what constitutes annotations (for proof guidance) and dead annotations in our context:

Definition 1** (Annotation).**

An annotation is a lemma call, a variant, an invariant, an assertion, a calculation, a calculation step or a calculation hint.

Definition 2** (Dead annotation).**

A dead annotation is an annotation, or a conjunct of an annotation, that can be removed from a verified Dafny method as long as the method still verifies after the annotation has been removed.

0.3.3 Overall approach

In the next sections we will provide details of the algorithms, architecture and implementation of the DARe tool. DARe essentially works by removing annotations from the program text and checks if the program still verifies. Here, we will describe how the various elements are handled and illustrate it with examples from [1]555See §0.6.1 for details about the examples used.. This will give an indication of the type of simplifications that can be done by DARe and those that are not handled. Note that all simplification has been done by the tool described in §0.4.

0.3.4 Lemma calls

The simplest cases are lemma calls. They are simply removed from the program text. To illustrate, consider the implementation of Fibonacci from [1]:

⬇

{

if n < 2 then n

else Fib(n - 2) + Fib(n - 1)

}

The property that n is divisible by 3 is equivalent to that its Fibonacci number is divisible by 2, is then expressed and proven as follows:

⬇

ensures Fib(n) % 2 $=$ 0 $\Longleftrightarrow$ n % 3 $=$ 0

decreases n

{

if n < 2 {

} else {

FibLemma(n - 2);

FibLemma(n - 1);

}

}

The proof follows the same structure as the definition of Fib with two recursive calls. However, this is something Dafny will do automatically, so DARe is able to simplify this to666 In this case, Dafny is actually able to prove the lemma fully automatically, so the body could be removed. We have taken a conservative approach to our definition of annotations (see Definition 1), meaning we do not attempt to remove such programming constructs. This is however something we may reconsider in the future (see §0.8). :

⬇

ensures Fib(n) % 2 $=$ 0 $\Longleftrightarrow$ n % 3 $=$ 0

{

if n < 2 {

} else {

}

}

0.3.5 Assertions

As with lemma calls, DARe first try to remove assertions. This was illustrated for set_inter_empty_contr above, where three assertions were removed.

If it is not possible to remove an assertion, then we we do not want to separate the equivalent cases illustrated by

⬇

assert A $\land$ B;

and

⬇

assert B;

For the first case, conjunctions are handled by first breaking the expressions up, then removing them one at a time, and re-combining them at the end.

0.3.6 Variants

DARe attempts to remove variants. This is illustrated above for FibLemma, with further examples below.

‘Wild-card’ variants (decreases *)

There is a special case for what we call wild-card variants (decreases *). These are used for programs that may not terminate. For example, when working with infinite sequence (using co-inductive datatypes) or control systems with a top-level non-terminating loop. There may also cases where a developer may decide to delay, or even ignore, a proof of termination.

To support such cases, a wild-card (*) can be used in the decrease clause to tell Dafny to ignore proving termination. For example, the following non-terminating methods is valid:

⬇

decreases *

{

while true

decreases *

{ }

}

Note that the wild-card has to be used consistently – if a method has a potentially non-terminating loop then the method needs to be declared to be potentially non-terminating, as illustrated above.

One could potentially use DARe to remove unnecessary wild-cards. However, in our data sets there were very few examples of this, and those that were there could not be further simplified. We will therefore not give this type of annotation much attention.

0.3.7 Invariants

Invariants are handled the same way as assertions. To illustrate, consider again the BinarySearch example. Firstly, the variant can be removed. The first two conjuncts of

⬇

invariant 0 $\leq$ low $\land$ low $\leq$ high $\land$ high $\leq$ a.Length

can also be removed. This is achieved by DARe by treating it as:

⬇

invariant low $\leq$ high

invariant high $\leq$ a.Length

and then remove the first two invariants. As a result we are left with:

⬇

invariant high $\leq$ a.Length

invariant $\forall$ i $\bullet$ 0 $\leq$ i < a.Length $\land$ $\lnot$(low $\leq$ i < high) $\Longrightarrow$ a[i] $\neq$ value

Another example is the following implementation of a method Max, then returns the index of the largest element in a given array:

⬇

requires a $\neq$ null

requires a.Length > 0

ensures $\forall$ i $\bullet$ 0 $\leq$ i < a.Length $\Longrightarrow$ a[i] $\leq$ t

{

var i$\colon$ int :$$= 1;

var max$\colon$ int :$$= 0;

while(i < a.Length)

invariant i $\leq$ a.Length

invariant max < a.Length

invariant i > 0 $\land$ max $\geq$ 0

invariant $\forall$ j $\bullet$ 0 $\leq$ j < i $\Longrightarrow$ a[j] $\leq$ a[max]

decreases a.Length-i

{

**if**(a[i] > a[max]) { max $:$$=$ i; }

i $:$$=$ i + 1;

}

return a[max];

}

Here, the variant

⬇

decreases a.Length-i

and the invariant

⬇

invariant i > 0 $\land$ max $\geq$ 0

can be removed, giving the following while-loop header:

⬇

invariant i $\leq$ a.Length

invariant max < a.Length

invariant $\forall$ j $\bullet$ 0 $\leq$ j < i $\Longrightarrow$ a[j] $\leq$ a[max]

0.3.8 Calculations

We have seen an example of a calculation that was used to chain together implications. Such proofs consists of chain together a sequence of facts, possibly combined with an operator and/or a justification/hint.

The simplest case for DARe is to remove complete calculations, but this may not be possible. For those cases, we try to simplify them. Calculations are used to write out the chain of reasoning in order to connect the first element of the calculation with the last element. For example, in the calculation of §0.2 it is shown how to derive false (last element) from x in A * B (first element). We therefore keep the first and last element, and try to remove all steps and hints between. This is achieved by splitting them up into individual elements, remove as many as possible, and then combine the remaining elements. For the calculation example in §0.2, we can remove one element (x in {}), creating the simplified calculation:

⬇

calc $\Longrightarrow${

x in A * B;

{ set_eq_simple(A*B,{},x);}

false;

}

}

For a more involved example, consider the following representation of Peano arithmetic, with a recursive definition of addition777The example is taken by a course on ‘’Verified programming in Dafny’ by Will Sonnex and Sophia Drossopoulou.:

⬇

function add(x$\colon$ natr, y$\colon$natr)$\colon$ natr

{

match x

case Zero $\Rightarrow$ y

case Succ(x’) $\Rightarrow$ Succ(add(x’, y))

}

The following lemma proves that addition commutes:

⬇

    **ensures** add(x,y) $=$ add(y,x)

{

match x {

case Zero $\Rightarrow$

**calc** {

  add(Zero, y);

 $=$

  y;

 $=$ { prop_add_Zero(y); }

  add(y, Zero);

}

case Succ(x’) $\Rightarrow$

**calc** {

  add(x, y);

 $=$ {**assert** x $=$ Succ(x’);}

  add(Succ(x’), y);

 $=$

  Succ(add(x’, y));

 $=$ {prop_add_comm(x’, y);}

  Succ(add(y, x’));

 $=$ {prop_add_Succ(y, x’);}

  add(y, Succ(x’));

}

}

}

As the add function is defined recursively over the first argument, the proof follows the same structure by a case analysis (match statement) of the first arguments. As we will see, this is the first step of a proof by structural induction [6].

For each case, the proof is achieved by a calculation. For the Zero case, the proof has two steps: first that we can remove adding Zero and the second that it can be added to the second argument, which completes the proof. The second step is justified by a separate lemma, which is proven automatically:

⬇

    **ensures** add(x, Zero) $=$ x

{}

The other case (Succ) follows a similar strategy by first moving Succ outside add, apply the induction hypothesis prop_add_comm(x’, y) to commute the arguments and the move Succ into the second argument. The last step justified by the following lemma, that does not require any proof guidance:

⬇

    **ensures** Succ(add(x,y)) $=$ add(x, Succ(y))

{}

This proof is unnecessary detailed, and DARe can simplify it to the following:

⬇

ensures add(x, y) $=$ add(y, x)

{

match x {

case Zero $\Rightarrow$

case Succ(x’) $\Rightarrow$

**calc** {

  add(x, y);

 $=$

  Succ(add(y, x’));

 $=$

  add(y, Succ(x’));

}

}

}

The first observation is that the first calculations is not needed so DARe has removed it. For the second calculation, the second step can be removed together with all justifications888This example also illustrates another potential simplification that we do not apply due to our more conservative definitions of annotations. Here, calls to two auxiliary lemmas are removed. If there are no other calls to them, they can be safely removed. However, as some lemmas may show a useful property and are not used just to help a proof we have decided to keep all of them. We may revisit this choice in the future. .

Combining operators in calculations

A calculation can also have combinations of operators. In some cases, the operator is also omitted, in which the given default operators is used (e.g calc $\Longrightarrow$ { $\ldots$}). If no such operator is given, equality is used. When removing a line of a calculation, DARe will also remove its preceding operator. This simple solution may result in that we do not find the shortest solution. To illustrate, consider the following dummy sequence:

⬇

 A;

$\Longrightarrow$

 B;

$=$

 C;

}

DARe may try to remove ‘$\Longrightarrow$ B;’. This will result in

⬇

 A;

$=$

 C;

}

which may not hold while the weaker

⬇

 A;

$\Longrightarrow$

 C;

}

may hold. This means that with our current design, this simpler solution will not be found. We plan to revisit this in the future, which will most likely involve using a lattice of the supported operators when selecting which operator should be kept.

0.4 The DARe tool999The source code is available from [2].

We have implemented a tool called DARe that removes dead annotations as specified in the previous section. The overall architecture of the tool is shown in Figure 1. DARe takes as input a Dafny program and returns a new Dafny program where the dead annotations have been removed. It uses Dafny to parse, resolve and translate the program to Boogie. Resolving a program involves some pre-processing and type checking. Dafny stores a program in an AST. DARe will remove (and add back) annotations from the AST. Dafny returns an updated Dafny program, or a translated Boogie program (if the translate command is given). The Boogie program is sent to Boogie for verification, which may return errors. Such errors are analysed and acted upon by DARe as explained next.

We have developed several different algorithms to remove the dead annotations. We give a theoretical comparison of them below, with an empirical evaluation in §0.6. The first version, called SimpleDARe, is as follows:

procedure SimpleDARe($prog$)

     for all $m\in\textsc{Methods}(prog)$ do

         $pos\leftarrow\textsc{Start}(m,prog)$

         while $\textsc{hasAnnot}(m,pos)$ do

              $pre\leftarrow\textsc{MethodBody}(m)$

              $pos\leftarrow\textsc{RemoveNextAnnot}(m,pos,prog)$

              $err\leftarrow\textsc{Verify}(prog)$

              if $\textsc{HasError}(err,m)$ then

                  $\textsc{ReplaceMethodBody}(prog,m,pre)$

              end if

         end while

     end for

end procedure

SimpleDARe steps through the program, method by method. For each method, it finds the initial position. As long as there are more annotations left from a given position in the method, it will remove the next annotation (RemoveNextAnnot) from the given position in the given method of the program. This will return the position just after that annotation. Note that there will be a side-effect on the program $prog$, where the next annotation has been removed (within method $m$). It then calls Verify to see if Boogie complains. If it reports any errors, then the removal is undone by replacing the body of method $m$ with the body before the annotation was removed ($pre$). This is achieved by ReplaceMethodBody.

Consider a program with the following assertions:

⬇

assert P; assert Q; assert R;

Assume that the verifier needs either P, or Q and R (e.g. P $\Longleftrightarrow$ (Q $\land$ R)). SimpleDARe will remove assert P and keep

⬇

        **assert** Q;   **assert** R;

The simplest, or shortest, solution would instead have been to keep ‘assert P’, as we could then have removed both ‘assert Q’ and ‘assert R’.

To overcome such issues, we developed a more complete version, called CompleteDARe. For simplicity, we describe this algorithm recursively:

procedure CompleteDARe($prog$)

     for all $m\in\textsc{Methods}(prog)$ do

         $pos\leftarrow\textsc{Start}(m)$

         $\textsc{MethodDARe}(m,pos)$

     end for

end procedure

procedure MethodDARe($m,pos$)

     if $\textsc{hasAnnot}(m,pos)$ then

         $pre\leftarrow\textsc{MethodBody}(m)$

         $pos\leftarrow\textsc{RemoveNextAnnot}(m,pos,prog)$

         $err\leftarrow\textsc{Verify}(prog)$

         if $\textsc{HasError}(err,m)$ then

              $\textsc{ReplaceMethodBody}(prog,m,pre)$

              $\textsc{MethodDARe}(m,pos)$

         else

              $\textsc{MethodDARe}(m,pos)$

              $s_{1}\leftarrow\textsc{Size}(m,prog)$

              $m_{1}\leftarrow\textsc{MethodBody}(m)$

              $\textsc{ReplaceMethodBody}(prog,m,pre)$

              $\textsc{MethodDARe}(m,pos)$

              $s_{2}\leftarrow\textsc{Size}(m,prog)$

              if $s_{1}<s_{2}$ then

                  $\textsc{ReplaceMethodBody}(prog,m,m_{1})$

              end if

         end if

     end if

end procedure

The main difference with SimpleDare is that when there are no errors, CompleteDARe will try both cases of keeping and removing the guidance, and keep the version that is shortest. In the above case it would have kept the first assertion and deleted the other two assertions.

The improved completeness achieved by CompleteDARe, results in a drastic increase in (worst case) runtime. We can see that SimpleDARe steps through each guidance one by one, and thus has a $O(N)$ runtime, where $N$ is the number of annotations. For CompleteDARe, on the other hand, this is increased to $O(2^{N})$ as all combinations are checked.

The increased runtime is undesirable, in particular for our interactive extension, discussed in §0.5, where rapid feedback is essential. For example, in a recent empirical study on the use of program analysis [8], the majority of developers ($375$ software engineers at Microsoft) said they would sacrifice intricate issues for fast feedback, when the analysis is run in real-time (as is the case in §0.5).

We therefore did an experiment by running both SimpleDare and CompleteDARe on $117$ examples from the Dafny library (see §0.6) for assertions and invariants. There was only one example where different results were returned, which had the same number of annotations but different ones had been deleted. Based on this observation, and the study in [8], we decided to sacrifice completeness for speed, and therefore discarded the CompleteDARe version.

The main bottleneck for runtime is the time that the verifier uses; this is studied in detail in [16, 41]. In fact, the time DARe (or Dafny) uses to parse, change, resolve and translate the AST is so insignificant compared with Boogie that it can be ignored. Whilst Boogie itself has some built in parallelisation [28], it is not (currently) possible to apply Boogie in parallel. Still, one optimisation is to reduce the number of calls to Boogie, which is achieved by CombinedDare:

procedure CombinedDare($prog$)

     for all $m\in\textsc{Methods}(prog)$ do

         $pos_{m}\leftarrow\textsc{Start}(m)$

     end for

     while $\exists m\;\cdot\;\textsc{hasAnnot}(m,pos_{m})$ do

         for all $m\in\textsc{Methods}(prog)$ do

              $pre_{m}\leftarrow\textsc{MethodBody}(m)$

              $pos_{m}\leftarrow\textsc{RemoveNextAnnot}(m,pos_{m},prog)$

         end for

         $err\leftarrow\textsc{Verify}(prog)$

         for all $m\in\textsc{Methods}(prog)$ do

              if $\textsc{HasError}(err,m)$ then

                  $\textsc{ReplaceMethodBody}(prog,m,pre_{m})$

              end if

         end for

     end while

end procedure

The difference from SimpleDare is that each method will in parallel remove a single annotation. It then applies Verify (Boogie) to all methods, and keeps the changed methods that do not have any related verification errors. Note that RemoveNextAnnot will do nothing, and just return the same program and position, when the end of the method is reached.

0.4.1 Properties of DARe

CombinedDare has no theoretical improvements in worst case runtime from SimpleDARe. However, it may in practice as the main bottleneck is the number of calls to the verifier. Let $\textsc{NumAnnots}(m)$ compute the number of annotations for method $m$. We can then summarise the number of calls to the verifier for each algorithm as follows:

[TABLE]

For SimpleDARe this is the same as the total number of annotations in the program text. As CompleteDare is run method-by-method, the number of calls is not quadratic on the number of annotations in the program. It is exponential for each method, which is then summed up. The interesting case is CombineDare. As each methods is run in parallel, the number of calls is the number of annotations of the method with the maximum number of annotations.

Below we outline a few simple yet important properties of DARe and the various implementations of the approach. We assume that RemoveNextAnnot is correct with respect to Definition 1, and that all annotation are tried101010We discuss implementation issues of RemoveNextAnnot in §0.4.2.. We use DARe to cover all algorithms.

Proposition 1**.**

DARe does not change the behaviour or contract of a program.

Proof.

The only changes to a program is done by RemoveNextAnnot, which we have assumed will remove annotations. Thus, both the program and its contract is left unchanged. ∎

DARe will only be applied to verified methods, meaning all stated properties hold. Thus, it cannot make any false properties true (as there are not any). This is also the case for the dual:

Proposition 2**.**

Ignoring runtime environments, DARe will not make any true properties false.

Proof.

The only changes DARe makes is to remove an annotation. If a method reports a verification error after removing an annotation then this is added back again to the program. As a method is assumed to be initially verified, it follows by induction that it will remain verified for each step. The only exception is that DARe may result in a longer proof. As the verifier may time-out that means that it may introduce new time-outs on other runtime environments. However, this case is ignored in the assumption. ∎

Next we compare the functional properties of the three algorithms.

Proposition 3**.**

CombineDare* and SimpleDARe will remove the same annotations.*

Proof.

For a given method, both algorithms sequentially steps through the methods and tries to remove the next annotation using RemoveNextAnnot. The only difference is that CombineDare will do this for all methods at the same time to reduce the number of calls to the verifier. The only case where they deviate is when there are no more annotations left in a method. CombineDare may then still make calls to RemoveNextAnnot, if there are other methods that have further annotation. However, in this case RemoveNextAnnot is assumed to behave as an identity, thus the method will be left unchanged. ∎

One may think that CompleteDARe somehow generalises SimpleDARe and CombineDare. However, this is not the case as it may remove completely different annotations than the other algorithms. The goal with CompleteDARe is to remove as many as possible, thus we have the property:

Proposition 4**.**

CompleteDARe* will remove at least as many annotations as SimpleDARe and CombineDare.*

Proof.

As CompleteDARe will try all possibly combinations, including those of SimpleDARe and CombineDare, and always pick the result that removes the most annotation, it will always remove at least as many as the others. ∎

0.4.2 Design choices & implementation issues

There are variations of how the next annotation is found (by RemoveNextAnnot); e.g. we could first remove all assertions, then all invariants, etc, or just remove the next annotation in a sequential manner. We have implemented the latter, although wild-cards in variants and calculations require special care which we will not go into here.

0.4.3 Running the DARe tool

There are two ways to run DARe:

In the Dafny Visual Studio IDE, which is explained in §0.5. 2. 2.

As a standalone tool in the command line.

The advantage of the command line execution is that it can provide various metrics that may be helpful for the user. The command line version has the following syntax:

It can also be used as a command line tool, which can also provide various metrics that may be helpful. Through the command line using the following style for command line parameters:

DareTools.exe <Z3 location> <output directory> <list of programs>

The user must provide the location of the Z3 executable (<Z3 location>), the directory where the simplified programs should be stored (<output directory>), and a list of programs that should be simplified (<list of programs>). The following example illustrates execution:

DareTools.exe C:\Programs\z3\z3.exe C:\Dafny

C:\Dafny\Prog.dfy C:\Dafny\Progs*

When the tool is launched it will tell you what programs were detected so that a user can make sure you entered them correctly. It will then give the following options:

Simplify and print program: This will remove all the dead annotations from the program and print a new one. 2. 2.

Log: This will remove all the dead annotations from the program and log the details as CVS files. The log will include counting the instances and how many of the different types of annotation is removed. 3. 3.

Completeness testing: This will run both CompleteDare and CombineDare and check if CombineDare find the smallest solution. 4. 4.

Runtime comparison: This will executes the tree algorithms discussed above, and log the times each takes to run.

In most cases the first option will be used, and the last third are mainly for evaluation purposes and used for the results discussed in §0.6.

0.5 A semi-automated DARe integrated in the Dafny IDE111111A screencast of the DARe IDE is available at [2].

There are cases where a developer may want to keep some of the dead annotations as they serve to explain the code: e.g. a variant to show why a loop terminates, or some key steps in a calculation which explains the correctness argument. Still, it is likely that many dead annotations should be removed.

To achieve both of these aims, we have developed a semi-automatic version of DARe that is integrated into Dafny’s Visual Studio plug-in [28]. Dafny’s IDE adapts the interaction model commonly used by IDE for compilers: the verifier is applied seamlessly in the background and verification errors are highlighted in the program text, by underlying the affected areas by red “squiggly” lines, as illustrated on line 31 of Figure 2 This approach is also recommended in [8], where most developers want results from static analysis shown in the editor.

We have followed the same approach, where DARe is seamlessly applied in the background. When it successfully finishes, all dead annotations will be highlighted (underlined and greyed out) as shown on line 31 of Figure 2. The user can select which one to remove, and to help automate this she can press the light-bulb to get the options of removing the given annotation or all annotations of the method or file, as shown in Figure 3.

As DARe will apply the verifier multiple times and is therefore slow compared with Dafny itself, it has been designed to be as unintrusive as possible. It is disabled by default, and the user can enable it in the Dafny menu121212The main “pain point” for static analysis reported in [8], is that wrong checks are on by default, which to some degree justifies our decision to have it disabled by default.. Figure 4 illustrates how to enable it.

Once enabled, DARe will initially be applied to all verified methods after the IDE has remained idle for at least 10 seconds. Once a user starts interacting with the IDE, DARe will terminate (with failure) so that the system does not become unresponsive. It will reapply DARe when it has been idle for at least 10 seconds. The plug-in will keep track of any methods that have changed since last time DARe was applied successfully and will reapply DARe to a method only when it has been changed. Again, this will only happen if the method does not have any verification errors and the system remains idle for 10 seconds.

0.5.1 Implementation details

The easiest way to achieve the seamless DARe application, is to apply it in a separate thread which is killed when interaction happens. However, this is not possible due to the issues of applying Boogie in parallel, as elucidated in §0.4. Instead, we implemented the architecture shown in Figure 5. We still apply DARe in a separate thread, but do not kill it and instead use a shared variable mode to control the execution.

Dafny applies the verifier and waits for the results – typically with a timeout of 10 seconds. If the program is changed while the verifier runs, it still waits for the previous verification task to complete before a new one is started [28]. Our extension has to fit with this model, and works as follows. The plug-in keeps track of which methods have changed, and when it is decided that DARe should be run, then: either DAReAll is called to apply DARe to all methods (initially); or DAReGiven is applied, provided with the names of the methods that have changed since last time. It will then set the mode to running. DARe will then execute, and on termination return the positions in the AST of the annotations that can be removed and set mode to success. If the user starts interacting while DARe is running, then the IDE will set mode to cancel. The CombinedDare algorithm of §0.4 is updated so that for each step, it will check the value of mode before running Boogie: if it is set to cancel, then it will terminate with failure and set the mode to failure. When the plug-in receives the results (either failed or successful), it will set mode back to idle. To avoid conflicts, we have restricted Dafny to only apply the verifier when the mode is idle.

The plug-in consists of two components:

• •

The tagger handles the communication with DARe and highlights annotations that can be removed in the program text.

• •

The action deals with the actual removal of annotations from the program text when the developer chooses to do so.

0.6 Evaluation

Several examples of the kinds of annotations that can be removed by the DARe tool is shown in §0.3. Note that all the removals discussed there has been created by the DARe tool. In this section we give the results of applying the different algorithms to a larger set of examples. The evaluation focuses on the amount of annotations that can be removed, the tool’s recall, and runtime issues. The experiments were conducted using Windows 10 with an Intel CORE i5 processor and 16GB RAM. A complete set of results, including all the programs (before and after DARe was applied) can be found on a dedicated webpage [2]. We first discuss the evaluation data used.

0.6.1 Evaluation data & approach

In order to evaluate the DARe tool we applied it to examples from the Dafny library and test suite [1]. The suite combines programs used purely for testing with actual developments. The full set is used for regression testing. Developments include solutions to verification challenges and competitions, such as VerifyThis and VSComp.

We removed all the programs we knew where only used for testing; they are predominantly found in a separate folder in the suite (called dafny0). After this $259$ programs were left. We then applied DARe to all methods that did not initially report a verification error, which was $7$ methods, leaving $252$ programs. Note that DARe was applied method-by-method: there were several cases within the $252$ where some methods did not intitially verify. These methods were ignored.

Note that to compare the algorithm in §0.6.4 a smaller evaluation set was used as only CombineDare supports the full functionality.

0.6.2 Annotations removed

In total there were $2869$ annotation over the programs131313This only includes methods that initially verified., meaning on average each program had $11.4$ annotations. DARe managed to remove $88\%$ of the annotations: a total of $345$ annotations were left, with an average of $1.4$ annotations per program.

Figure 6 shows the relationship between annotations removed and the LoC. Note that the relationship between the total number of annotations and annotations removed is almost identical. As the figure illustrates there is no clear pattern, although it is worth noting that there is a high degree of programs where no annotations were required.

Below we discuss each type of annotations separately.

Assertions

In our test set there were $113$ programs with a total of $657$ assertions (average of $5.8$ for each program). DARe was able to remove $91\%$ of these, meaning only $58$ annotations were left (average of $0.5$ for each program). Of the remaining $58$ we tried to remove any conjuncts if present, which could not be done for any of them.

It is not clear why this number is so high. One of the reasons are that annotations are often used to find a proof or to debug in order to discover where the prover fails. These may then have been left. Another reason is improved automation by Dafny. A third reason is that some of them are probably left to explain the proof and should therefore not be removed.

Lemma calls

There were a total of $491$ lemmas calls over $55$ programs in our test-data. Out of these, $85\%$ could be removed leaving only $75$. In many cases all lemma calls could be removed.

As with assertions, the number of lemma calls that can be removed is surprisingly high. Some of the reasons are the same as for assertions, as one can see lemma calls as ways of asserting richer properties that require proofs. Another direct reasons may be the introduction of an “induction tactic” [26], which means that many recursive function calls are no longer required. Any development pre-dating this feature would have had such calls which can now be removed.

Invariants

$57$ programs had a total of $393$ invariants. DARe was able to remove $102$ of these invariants, meaning $26\%$ could be removed. As with assertions, invariants may be made of a conjunction. For the remaining $291$ invariants we could split some of them, resulting in $125$ conjuncts141414We only consider the invariants that could be split up. Of these $6$ conjuncts could be removed.

Variants

$51$ programs had a total of $168$ variants, where $40$ ($24\%$) could be removed.

As we have already mention, no wild-card variants could not be removed: $6$ programs used a total of $16$ of these clauses and none of them could be removed.

Calculations

$29$ programs had a total of $114$ calculations. $89\%$ ($101$) could be removed fully. $8$ of the remaining calculations where in one program (Calculations.dfy). When splitting them up as described above we ended up with $47$ parts where $38\%$ of them could be removed. The remaining calculations where unchanged.

Again, this is a surprisingly high number that can be removed. One reason may be that calculations are predominantly used ‘explain’ proofs and not to automate them.

0.6.3 Runtime

The most important feature was if removing annotations had any impact on runtime. There are reasons that it may increase of decrease:

• •

By removing unnecessary clutter, the prover can find a proof faster, thus reducing the verification time;

• •

By removing annotations, we could remove a shorter proofs, thus increasing the search required and thus increasing verification time.

To evaluate runtime we ran each program $3$ times and used the average from this. On average for all $252$ programs, each program took $1027$ ms to verify before annotations were removed, and $566$ ms afterwards, i.e. the runtime was almost halved. The average reduction for all programs was $461$ ms, while the median was only $4.5$ ms. From that one may conclude that many programs were either very small or there were a few programs with a drastic improvement in runtime while very few had a massive improvement.

0.6.4 Comparing algorithms

In §0.4 three different algorithms: CombineDare is the one the tool supports by default (and used by the GUI), while CompleteDare tries all possible combinations and will find the solution with fewest annotations. For technical reason we were only able to compare the algorithms for a version of DARe that does not have all the features presented above. This version was only applicable to $117$ programs, and is the same data as used in [7].

Our first experiment was to test the recall of CombineDare by comparing it with an implementation of CompleteDare. As this was only for comparison we only support assertions and invariant removal.

It was only case where the results from the two algorithms different, and in that case the size was actually the same. Although this may suggest a recall of $100\%$, the size of the data and the fact we only support assertions and invariants makes such conclusion premature. However, it was sufficient for us to conclude that in practice the recall of CombineDare is sufficient to justify using it.

To compare runtime we only compared SimpleDARe and CombinedDare and CompleteDARe only supports assertions and invariants so a comparison will neither be fair nor informative. The difference in runtime between SimpleDARe and CombinedDare was not as large as expected. The average difference is about $5$ seconds, with a median of only $0.26$ seconds. Figure 7 shows the difference in runtime (Y-axis) with respect to the overall runtime of SimpleDARe. The figure shows that while the difference increases with the runtime, there is no indication that the factor is related to runtime. The smaller than expected difference may be due to: an uneven distribution of annotations between the methods151515Recall that CombinedDare performs better the more distributed annotations are. and optimisations within Boogie where verification results are cached at the method level so that only changed methods are re-verified [29].

0.7 Related work161616An abstract of this work appears in [7], and a tool demo is given in [15]. [7] only gives a high-level view of the tool and results, while [15] only illustrates tool usage. This is a special issue dedicated to the work presented in [15].

This work is an example of search based software engineering [18], where search techniques are used to support and automate the work by software engineers. The problem of discovering which annotations are unnecessary, which is the key challenge of our work, is comparable to the credit-assignment problem in reinforcement learning [31]. This is the problem of determining which components contribute to the overall success of a system or game.

We are not familiar with any similar work for program verifiers, where the focus tends to be on the discovery of auxiliary annotations (e.g [17, 20, 39, 12]). Our work is inspired by dead code removal (or dead code elimination), which is the problem of discovering and removing code that is never reached. This is a common compiler optimization, and is typically achieved by data-flow analysis.

Within automated theorem proving there is a large line of work concerned with selecting only necessary lemmas and axioms provided to the prover in order to reduce the search space (e.g. [40, 24]). An alternative approach to DARe would be to see if any of these heuristics can be explored to automatise our search, which currently remove annotations one by one. Another approach is to derive the required annotations from the proof terms generated by Z3 [10], and remove any annotation not used. This will not require any additional Boogie calls, and should thus be considerably faster and scale better. This approach is however complicated by the way in which translation from Dafny into Z3 is handled via Boogie. As our work was mainly motivated by discovering the amount of dead annotation, we decided for the simpler search-based approach. In the future, it would be interesting to see how feasible it is to analyse the result from Z3 (which may also be beneficial for general caching of verification attempts [29]). Note that this is similar to how the Sledgehammer tool for Isabelle uses tools like Z3 in order to reconstruct the proofs within Isabelle [36].

Dual to our work of trying to a find a minimal solution to a success criteria (i.e. provability), is finding the minimal causes of failures. This is particularly relevant for debugging regressions. Two approaches that are reminiscent of our work are: regression containment [33], which automates the process of isolating regressions; and the more general delta debugging [45]. Here, the smallest configuration that introduces a regression is (automatically) sought, which is similar to the manner in which we are seeking the smallest set of annotations. “The method” of the ACL2 community [23] involves deriving a “toy problem” from a problem such that the solution of the toy problem can be ported to solve the main problem. One would like this toy problem to be as small as possible. Note that this is a (manual) development method, and has not been automated.

The topic of automated repair has recently received a great deal of attention, with a large number of tools addressing this problem171717See automated-program-repair.org.. The SemFix repair tool [34] steps through each statement, ranked by their suspiciousness of being the bug, and attempts to repair them one-by-one in the same way as DARe steps through annotations one-by-one (albeit without any ranking). The AutoFix tool [37] repairs programs in presence of contracts, and uses program synthesis techniques to add statements. This is again analogous to how DARe works, with the difference that DARe removes annotations as opposed to generating statements. Within model-driven engineering there has been work on discovering redundant constraints, i.e. constraints that can be derived from other constraints [42]. This work uses the Alloy system [21] to derive these, and is similar to DARe in that redundant constructs are removed using a verification system.

The main advantage of our approach relates to readability, as there is little effect on runtime once redundant annotations are removed. There are many tools to support developers in achieve “better code” in that respect. The most well-known is probably ReSharper from JetBrains181818See www.jetbrains.com/resharper/.. As with DARe, it has a Visual Studio plug-in, and can highlight issues related to quality (e.g. redundant casts) as well as use of coding standards.

There are also several code refactorings that relate to improved readability [13], and an additional, or even alternative, way to improve readability and structure is to apply more general refactorings to the annotations in the program text. Refactorings have previously been studied for proof scripts [43, 44], and we have started to address this for program verifiers. However, it is not clear how this can be fully automated. Recent work on tactics for Dafny aims to provide more high-level guidance, and attempts to generate a minimum number of annotations from given verification patterns [16, 14].

0.8 Conclusion & future work

We have presented the DARe tool, which automatically removes annotations that are not required by the verifier. We have extended the Dafny IDE with a semi-automatic version of the tool, and shown that in our evaluation set, $88\%$ of annotations can be removed. It was particularly successful for assertions, lemma calls and calculations.

Next, we would like to apply DARe to larger programs. In particular, the large Ironfleet development, which in total has $40K$ lines of “proofs”191919This number is likely to contain elements which we have not classified as annotations. [19], would be a very interesting case study. This will stress-test DARe, but is likely to require some special-purpose configurations to DARe (e.g. change of time-out values), due to the sheer size of the development. It is also worth noting that most of the programs in the Dafny library have been developed by the main Dafny developer (Rustan Leino), who is considered to be the main expert on Dafny. He is therefore likely to write more “minimal” annotations than “normal” users. It will therefore be interesting to see if the number of dead annotations increase when developed by others.

There are several ways to extend the work further. We could address further simplification techniques, possibly normalising formulas to CNF form and then split the conjuncts. We could also extend the tool to other constructs. For example, programming constructs for the ghost state can also be removed. Another example is to remove/simplify contracts for (auxiliary) recursive methods which are analogous to loop invariants; in this case a user may need to indicate whether or not a lemma is auxiliary. Similarly, certain auxiliary lemmas that are no longer called can be removed. Another possibility, is to extend the work to more meta-level analysis such as subsumption and equivalence relations between annotations, as well as exploring the Z3 proof terms as discussed in §0.7.

We would like to empirically investigate if the classification of annotations makes sense for Dafny developers. This could be achieved by interviews, user experiments, and (to some degree) by instrumenting DARe with a logging mechanism to capture which dead annotations a developer selects to remove. We may also make the classification user configurable. Such studies will help inform the development of future releases of DARe. Finally, we could implement similar tools for other program verifiers and re-do the same experiments for them.