Add by { ... } block to method calls

[keyboardDrummer]

Dafny has method calls. Here's an example that shows calling a method with a precondition, and how you can prove that precondition before doing the method call:

predicate P(x: int);

method Foo(x: int)
  requires P(x)

lemma ProveP(x: int) ensures P(x)

method Caller(x: int) {
  ProveP(x); // Calling the lemma here allows us to satisfy the precondition of Foo in the next line
  Foo(x); // Method call
  assert P(x); // The precondition of Foo still holds after the call
}

However, we would like our proof of the precondition of the called method, not to affect any of the surrounding proofs. For that we propose the following syntax:

predicate P(x: int);

method Foo(x: int) returns (r: int)
  requires P(x)

lemma ProveP(x: int) ensures P(x)

method Caller(x: int) {
  var r := Foo(x) by {
    ProveP(x);
  }
  assert P(x); // Error, could not prove
}

For function calls, which occur in expressions, it is not necessary to add by { ... } clauses, because there is already syntax for proving the preconditions of expression only in the scope of that expression, using statement expressions.

Example:

function Q(x: int): int requires P(x)

method Foo(x: int) {
    var r := (ProveP(x); Q(x)); // The outer parenthesis are necessary so this is resolved as an expression
    assert P(x); // Currently this passes but that's a bug. It should fail
}
lemma ProveP(x: int) ensures P(x)

[keyboardDrummer]

This is existing discussion on this topic here: #5192

[RustanLeino]

I argue that the same functionality is useful for function calls. For example, one may want to hide the proof of P(x) from the proof of R(r) in:

function F(x: int): int {
  var r := Foo(x) by {
    ProveP(x);
  }
  assert R(r); // I'm imagining that R(r) is the precondition to Roo(r)
  Roo(r)
}

[keyboardDrummer]

I argue that the same functionality is useful for function calls. For example, one may want to hide the proof of P(x) from the proof of R(r) in:

function F(x: int): int {
  var r := Foo(x) by {
    ProveP(x);
  }
  assert R(r); // I'm imagining that R(r) is the precondition to Roo(r)
  Roo(r)
}

I don't follow your example well. Did you make any typos?

However, expressions, in which function calls occur, already have a space for specifying proofs that are specific to that expression, using expression statements.

predicate P(x: int)
function Foo(x: int): int requires P(x)
lemma ProveP(x: int) ensures P(x)

method Bar(x: int) {
  var z := (ProveP(x); Foo(x));
  assert P(x); // Currently passes since the expression statement is not properly scoped
  // However, we will change that so the call to ProveP(x) is out of scope at this point
  // And then the assertion will fail
}