Hi Mike,.
Dafny insists that all expressions be welldefined 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 divisionbyzero 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 nonzero.
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 wellformed (furthermore, x/y==100 holds, so the assertion also holds). But, as I said above, a postcondition
must be welldefined in every context where the precondition holds. That is, the postcondition needs to welldefined 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 welldefinedness independently of the method body, which means you get a divisionbyzero 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 inparameter, the following specification would also be welldefined:
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
