Definite-assignment in specification depends on implementation

[RustanLeino]

Dafny version

4.9.1

Code to produce this issue

method M0(b: bool) {
  var x: int;
  opaque
    ensures b ==> x == 8
  {
    if b {
      x := 8;
    }
  }
}

method M1(b: bool) {
  var x: int;
  opaque
    ensures b ==> x == 8
  {
    x := 8;
  }
}

Command to run and resulting output

% dafny verify test.dfy
test.dfy(4,18): Error: variable 'x', which is subject to definite-assignment rules, might be uninitialized here
  |
4 |     ensures b ==> x == 8 // as a spec, this is odd, because it could be evaluated in a context where x is not assigned
  |                   ^

What happened?

The specification of the opaque block in both of the methods above is

  opaque
    ensures b ==> x == 8

Specifications in Dafny (e.g., ensures clauses of methods and invariant clauses of loops) are checked for well-formedness _without regard of the implementation(except for gathering the syntactic assignment targets, which applies to both loops and opaque blocks, since these two can make local variables). However, of the methods above, an error is generated for methodM0but not forM1. The only difference between M0andM1` is the implementation (i.e., the body) of the opaque block.

The right thing to do is to check the well-formedness of the opaque block's specification without looking at the body. So, both of the methods above should generate an error.

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

Mac