Experience on Dafny Programming

Because of Professor Dillig’s class, I finally got the chance to try out Dafny, a language made by Microsoft Research, with built-in support for formal specification through preconditions, postconditions, loop invariants and loop variants. I often think, what if we write programs in a verification language, would there be much less bugs and will it make our lives much easier than sitting in front a screen for hours grinding at bugs. Here are some thoughts I want to put down before they are gone in my head.

Here is a simple example illustrating some basic concepts in Dafny. Suppose we are given a function that reverses a sequence. For example, we want to return [c, b, a] when given [a, b, c], the recursive implementation would look like:

function reverse<T>(in : seq<T>) : seq<T>
{
    if (|s| == 0) then s
    else reverse(s[1..]) + [s[0]]
}

This looks correct, right? We have termination condition set for recursion, the implementation is fairly straightforward. Nothing seems wrong. If the function is correct, it would suggest that the lemma

lemma reverseLemma<T>(in : seq<T>)
ensures in == reverse(reverse(in));
{}

must hold. If we simply reverse a sequence twice, it would be the same compared to the original input. However, compiling the program would complain that a postcondition might not hold. This is really strange. If we simply eye-ball through the implementation of reverse, it’s hard to imagine what could possibly go wrong.

One thing you should constantly keep in mind is that the Dafny compiler doesn’t really understand the implementation of the code. It instead uses specification to reason about the correctness of the program.

Imagine we are given a function called func1, we know its function signature and its return type. Then we are told that calling this function twice with a given input \(s\) is going to produce an output \(k\) matching \(s\) exactly. How should we trust that this claim is valid if the function func1 is a black box. How do we know if calling func1 with input \(s\) might never terminate?

The solution is to annotate the function with certain properties so that the compiler knows what condition might hold before and after a function is executed.

For example, the reverse might take a sequence with length greater or equal to 0. Otherwise, it wouldn’t make sense to reverse a sequence with negative length. We could write this requirement as requires |in| >= 0.

We also need to claim that the output of function reverse must be equal to the input, denoted as ensures |s| == |reverse(s)|.

Finally, and most importantly, what property must the output of reverse have? It’s the order of the output must be the reverse of the input. How do we express such property? We should say something like: every element in the output sequence must match the element in the original input sequence at the reversed location. It will look like: ensures forall i :: 0 <= i < |in| ==> reverse(in)[i] == in[i_reversed].

After spending some good hours writing Dafny, my feeling towards Dafny is mixed. The plus side is writing down how a program behaves exactly and precisely forces programmers to be more careful when writing code. This would remove a lot of problems after deployment. Reuse verified API also removes concerns over much of the safety issue.

The tricky part is coming up with annotations that meets specification requirements. On one side, this forces people to break down big tasks into smaller functions so that it’s much easier to come up with correct annotations. On the other side, debugging complex functions would require some magic. The debugging messages aren’t really helpful in terms of narrowing down possible problems. It would require some guesses and luck to find what annotations are wrong or lacking. The example reverse function only has few post and pre conditions. However, more sophisticated functions involving multiple conditions as well as invariants are much harder to get right. Often, it requires the programmer to explore in the dark without much guidance before uncovering the solution.