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.

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.