Dafny: issue with sets

Oct 9, 2012 at 1:08 PM

Why Dafny can't prove this property about sets ?

ghost method Lemma(d1 : set<int>, d2 : set<int>)
	requires forall x :: x in d2 ==> x in d1;
	ensures d2 <= d1;
{
}

Oct 16, 2012 at 2:39 PM

This issue is the same as in the following discussions thread: http://boogie.codeplex.com/discussions/399581

http://rise4fun.com/Dafny/27P

Coordinator
Oct 17, 2012 at 10:28 PM

I have fixed this problem.  However, the solution lies in a tricky region that intersects soundness, usefulness, and acceptable performance, so I made some compromises.  In particular, Dafny now knows some additional properties of sets if the sets are in-parameters of methods.

More details:

The problem had to do with the underlying encoding.  Dafny sets are represented in Boogie as sets of "boxes".  That is, a set<T> in Dafny is essentially represented as a set<Box> in Boogie (I'm taking liberties with syntax).  So, the Dafny statement "S := S + {x};" is encoded in Boogie as:

S := S + { Box(x) };

and the Dafny expression "y in S" is encoded in Boogie as:

Box(y) in S

The postcondition in your example above uses Dafny's built-in subset operator, which gives rise to the encoding:

forall bx: Box :: bx in d2 ==> bx in d1                      // (*)

In contrast, the quantifier you wrote yourself above is encoded as:

forall x: int :: Box(x) in d2 ==> Box(x) in d1               // (**)

When the prover tries to prove the postcondition (*) from the precondition (**), it assumes (**) and negates (*) and looks for a counterexample.  The negation gives:

bx in d2 && !(bx in d1)

but this is not of the form that would make the verifier think of using (**).  More precisely, this does not trigger any instantiation of (**).  In my fix, I encoded things to get a property like:

bx in S ==> Box(Unbox(bx)) == bx

This causes the "x" in (**) to be instantiated with x := Unbox(bx), which then completes the argument.

The fix also addresses the issues in the related discussion thread you mention above (where you correctly had suspected that boxing was an issue).

  Rustan

Oct 19, 2012 at 3:15 PM

Ok, thanks, Rustan!

 

  Eugene