Dafny: Violation of precondition in must-be-true constant case

Question

Dafny cannot validate the m method for the following code:

predicate p(k: int)
requires k >= 0
{    
    true
}

method m() returns (k: int)
    ensures p(k) //<-
{
    k := 0;
}

It reports possible violation of function precondition for the ensure line, which is k>=0. This certainly cannot be a violation as the parameter is literally a constant 0 (0=0), why does dafny think this is not in compliance? And how do I fix it?

Answer 1

Good question! In Dafny, all expressions have what is called a "well-formedness condition", which checks things like function preconditions, sequence indices in bounds, etc. All expressions are required to be well formed, and this is checked by Dafny conceptually before verifying the program.

For expressions used as part of a method specification, they have to be well formed in isolation, independently of the method body. So in your example, Dafny tries to check the expression p(k) is well formed without looking at the body of the method, which is why it fails.

The typical way to fix this error is to change the postcondition to guarantee well formedness in isolation. In your example, you can do this by changing your postcondition to

ensures k >= 0 && p(k)