Body-less opaque blocks

[RustanLeino]

Summary

The body of an opaque block should be optional.

Background and Motivation

Dafny supports body-less loops and body-less forall statements. These allow the programmer to temporarily omit the body of the loop/forall statement and only rely on its specification. Once the rest of the program has been written, the programmer can return to fill in the body. Opaque blocks are a similar statement, for it hides a body of code behind a specification. Thus, opaque blocks ought to support leaving off the body as well.

Proposed Feature

method M(s: int) returns (r: int) {
r := s;
opaque
ensures s < r
}

Alternatives

There are two tricky issues involved in implementing body-less loops. I expect body-less opaque blocks to encounter the same two issues, and I expect that these issues can have the same solutions as for loops.

One issue regards parsing. In a code snippet like

opaque
  ensures s < r
{
  // some code here
}

there is an ambiguity: is the {...} the body of the opaque block or is it a separate block that happens to follow a body-less opaque block? For loops and forall statements, this ambiguity is solved by eagerly parsing the {...} as the expected body. That makes sense also for opaque blocks.

The other issue regards figuring out a frame, since both loops and opaque blocks want to compute the syntactic targets from their given body. For a body-less loop, this issue is resolved by instead using all mutable variables that are mentioned in the loop guard or loop specification. Note that this does not include in-parameters, since in-parameters are not mutable variables. Note also that this includes the heap only if the heap is used in the loop guard or loop specification. A body-less opaque block can do the same, using the mutable variables that are mentioned in the opaque-block specification.