Cautionary Tales

This page collects some "cautionary tales" where users thought they had proven something, but actually they did not prove anything, because they misunderstood how Dafny works.

Understand Dafny's command line interface

If I have a file A.dfy and a file TopLevel.dfy which includes A.dfy, and I want to verify both of them, I used to just call dafny TopLevel.dfy, and let Dafny find A.dfy by reading the path given in the include in TopLevel.dfy. This looked like a very handy way of not having to list all dafny files explicitly on the command line. However, it turns out that dafny only verifies the files you explicitly mention in the command line arguments, and for the included files, it just assumes that all proofs in them hold, without verifying them. So if I modify A.dfy in a way which makes some lemma in it not hold any more, and I just run dafny TopLevel.dfy, it will look like everything is still fine, even though it isn't.

So one has to make sure that every file to be verified is given as a command line argument to dafny.

Specifying external classes

When interfacing with libraries written in C#, we have to write specs for them, but we don't implement them in Dafny. If we don't pay close attention to getting the reads clauses and modifies clauses right, it's easy to make contradictory assumptions, and Dafny will exploit such contradictions whenever a method with a contradictory specification is used, so it's easy to believe to have proved something without actually having proved it. There is a separate wiki page on understanding and preventing this.

Know your operator precedence and don't trust indentation

Here's simplified example from an actual project which caused some confusion. Consider the following file:

datatype Option<T> = None | Some(get: T)

predicate FirstPredicate(n: nat)

predicate SecondPredicate(n: nat)

predicate ThirdPredicate(n: nat)

predicate FourthPredicate(n: nat)

method test(n: nat) returns (res: Option<nat>)
    requires SecondPredicate(n)
    requires FourthPredicate(n)
    ensures FirstPredicate(n) ==>
                SecondPredicate(n) &&
                res.Some? &&
            ThirdPredicate(n) ==>
                res.Some? && FourthPredicate(res.get)

{
    return Some(n);
}

By quickly looking at it, we might believe that we proved that if FirstPredicate holds for n, then test will always return Some. A good way to "smoke test" proofs is to change some postcondition to its negation and see if the proof still works. For instance, in the above file, if we replace the first res.Some? by res.None? -- surprise -- the proof still goes through!

So what's wrong with this specification?

It turns out that && binds stronger than ==>, and moreover, ==> is right-associative (i.e. P ==> Q ==> R is the same as P ==> (Q ==> R)). So if we add parentheses and change indentation to clarify, we see that what we wrote above is equivalent to the following:

method test(n: nat) returns (res: Option<nat>)
    requires SecondPredicate(n)
    requires FourthPredicate(n)
    ensures FirstPredicate(n) ==> 
                ((SecondPredicate(n) && res.Some? && ThirdPredicate(n)) ==>
                    (res.Some? && FourthPredicate(res.get)))
{
    return Some(n);
}

And if we further clarify it by using that P1 ==> P2 ==> P3 is equivalent to P1 && P2 ==> P3, we get

method test(n: nat) returns (res: Option<nat>)
    requires SecondPredicate(n)
    requires FourthPredicate(n)
    ensures (FirstPredicate(n) && SecondPredicate(n) && res.Some? && ThirdPredicate(n))
             ==> (res.Some? && FourthPredicate(res.get))
{
    return Some(n);
}

So we see that the first res.Some? is actually on the left-hand side of an implication, so we're not proving it, but we're assuming it.

The correct way to write what we meant puts parentheses around the implications, as follows:

method test(n: nat) returns (res: Option<nat>)
    requires SecondPredicate(n)
    requires FourthPredicate(n)
    ensures (FirstPredicate(n) ==>
                SecondPredicate(n) &&
                res.Some?) &&
            (ThirdPredicate(n) ==>
                res.Some? && FourthPredicate(res.get))

{
    return Some(n);
}

And now if we repeat the smoke test of replacing the first res.Some? by res.None?, the proof doesn't work any more, as expected.

Know your grammar and again, don't trust indentation

Suppose we have some complex machinery in a method, and this machinery only works for even numbers:

datatype Option<T> = None | Some(get: T)

method Machinery(arg: int) 
    requires arg % 2 == 0
{
    // some complex code
}

method UseMachinery(o: Option<int>) {
    var a: int;
    match o
        case Some(v) => a := v;
        case None => a := 0;
    Machinery(a);
}

The above snippet is verified, so we might think that each call to UseMachinery calls Machinery exactly once, and that it always passes an even argument to it. However, that's not true, because parsing of case None greedily adds as many statements to the None branch as possible, so Machinery(a) is only invoked in the None case. To fix this, we have to use curly braces:

method UseMachineryCorrectly(o: Option<int>) {
    var a: int;
    match o {
        case Some(v) => a := v;
        case None => a := 0;
    }
    Machinery(a); // as expected, precondition failure
}