0

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?

wusatosi
  • 617
  • 5
  • 13

1 Answers1

2

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)
James Wilcox
  • 5,307
  • 16
  • 25
  • Does this mean to `ensure` a predicate's result dafny does not implicit add the precondition of the predicate to the `ensure` line automatically? Also, where can I find more information on such subjects? – wusatosi Feb 26 '22 at 03:25
  • 1
    Correct. Dafny does not automatically add such preconditions. Lots of resources in [this answer](https://stackoverflow.com/a/49746198/438267) and on the [Dafny homepage](https://dafny-lang.github.io/dafny/) – James Wilcox Feb 26 '22 at 19:54