dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.83k stars 254 forks source link

function refinement broken #5366

Open erniecohen opened 1 month ago

erniecohen commented 1 month ago

Dafny version

4.5.0, 4.6.0, nightly

Code to produce this issue

abstract module A {
  function F(x: int): (r: int)
    ensures r > x
}

module B refines A {
  function F ... 
  // the result type of function 'F' (bool) differs from the result type of the corresponding function in the module it refines (int)
  // function 'F' is declared with a different number of parameter (0 instead of 1) than the corresponding function in the module it refines
  { x + 1 }
}

Command to run and resulting output

vscode

What happened?

The example above from the manual fails in the resolver. It worked through 4.4.0.

What type of operating system are you experiencing the problem on?

Mac

keyboardDrummer commented 1 month ago

The documentation seems to indicate this should work, although I'm not used to this syntax either:

image

We could check with @RustanLeino to see whether he intends to keep the semantics as the documentation currently defines it.

erniecohen commented 1 month ago

A workaround is to skip the refinement notation, e.g.

module B refines A {
  function F(x: int): (r: int)
  { x + 1 }
}

Note that if the refined module defines a precondition, you cannot repeat this precondition in the refining module.