Question on assert vs. ensure

Feb 21, 2013 at 4:48 PM
I have a method that does a very simple manipulation and proves an assertion correct, but then fails to prove the same assertion in the "ensures" clause of the method with a timeout. Any ideas on what might be going wrong?
method findLoc(n: int) returns (usedSeqLoc: int, usedLoc: int) 
    requires arrayInv();
    requires usedHd != -1;
    requires n < elementArray[usedHd] ;

    // If I comment this, it works.
    // ensures (usedLoc == usedSeq[usedSeqLoc]) ; 
{
    usedLoc := usedHd; 
    usedSeqLoc := 0;
    // this is true because of a property in arrayInv(); 
    assert(usedLoc == usedSeq[usedSeqLoc]);                 
}
Thanks!

Mike
Coordinator
Feb 22, 2013 at 10:41 PM
Hi Mike,.

Dafny insists that all expressions be well-defined in every possible usage context. For example, consider this method:
method M(x: int, y: int) returns (z: int)
{
  z := x / y;
}
Dafny will flag the expression "x / y" as possibly having a division-by-zero error, because there is a context in which y might be passed in as 0. If you wrap the assignment inside a conditional like "if (y != 0) { ... }", then the error goes away, because the context of "x / y" now guarantees that y is non-zero.

In a specification, the "context" of a precondition is any state at all, and the context of a postcondition is any state where the precondition holds. The following program, which is more similar to yours, illustrates:
method P() returns (x: int, y: int)
  ensures x / y == 100;
{
  x, y := 1200, 12;
  assert x / y == 100;
}
Looking at the body, it is clear that all executions that bring us to the assert statement have the property that y != 0, so the expression in the assertion is well-formed (furthermore, x/y==100 holds, so the assertion also holds). But, as I said above, a postcondition must be well-defined in every context where the precondition holds. That is, the postcondition needs to well-defined independently of the method implementation. This is good, because it means that clients of the methods never need to worry about cases where the postcondition would be undefined, for what would the postcondition mean in such cases?

So, the postcondition is checked for well-definedness independently of the method body, which means you get a division-by-zero error for the postcondition. To fix the problem, change the postcondition to:
  ensures y != 0 && x / y == 100;
or to:
  ensures y != 0 ==> x / y == 100;
If y had been an in-parameter, the following specification would also be well-defined:
method Q(y: int) returns (x: int)
  requires y != 0;
  ensures x / y == 100;
So, in your example, change the postcondition to be:
  ensures 0 <= usedSeqLoc < |usedSeq|;
  ensures usedLoc == usedSeq[usedSeqLoc];
and you'll be fine.

Rustan
Feb 26, 2013 at 5:14 AM
Thank you very much sir. Works like a charm.
Mar 1, 2013 at 8:59 PM
This is very good advice! I've had the same problem, i.e. asserting just what a method ensures. Great to see an explanation.

(1) Any idea, though, why Dafny loops, instead of reporting the out-of-bounds use of [usedSeqLoc]?

(2) The method's precondition is
requires arrayInv();
requires usedHd != -1;
requires n < elementArray[usedHd] ;
Does the arrayInv() guarantee that 0<=usedHd<|elementArray|?

Thanks!