CODEWITHSUNDEEP
dafny
Kevin S
Kevin S

Reputation: 531

Dafny recursion hits every element in sequence, can't verify

The following function, seqToSet, takes a sequence of elements and returns a set containing all (and only) the elements in the given sequence. It does this by calling a recursive helper function, addSeqToSet, with the same sequence and the empty set. The helper function adds each element in the sequence to the set it is given and returns the result. It does this via recursion on the head/tail structure of the sequence. It is done when the sequence is empty, and otherwise calls itself recursively with the tail of the sequence and the union of the set with the singleton set containing the head of the sequence.

Dafny can't verify on its own the postcondition stating that the resulting set contains all of the elements in the original sequence.

What's the right strategy for helping it to see that this is the case?

function method seqToSet(q: seq<int>): set<int>
{
    addSeqToSet(q, {})
}

function method addSeqToSet(q: seq<int>, t: set<int>): (r: set<int>)
    ensures forall i :: i in q ==> i in r
{
    if | q | == 0 then t
    else addSeqToSet (q[1..], t + { q[0] })
}

Upvotes: 1

Views: 568

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

When Dafny tries to verify postconditions of recursive functions, it reasons by induction: assume the postcondition holds on any recursive calls, and show that it also holds for the current call.

Imagine how Dafny reasons about addSeqToSet.

In the first branch, | q | == 0 implies q is empty, so the postcondition holds trivially, since there are no elements i in q.

In the second branch, Dafny assumes the postcondition of the recursive call:

forall i :: i in q[1..] ==> i in r

and then tries to prove the postcondition for the current call:

forall i :: i in q ==> i in r

Notice that since addSeqToSet directly returns the answer from the recursive call, r is the same in both of the above formulas.

If you think about it for a minute, you can see that the postcondition of the outer call does not follow from the postcondition of the recursive call, because the recursive call says nothing about q[0].

You need to strengthen the postcondition in some way so that you know that q[0] in r as well.

One such strengthening is to add the additional postcontition about t

ensures forall i :: i in t ==> i in r

Dafny then verifies both postconditions.

Upvotes: 2

Related Questions