Requires/ensures encapsulation

May 27, 2014 at 11:59 AM
Edited May 27, 2014 at 12:00 PM
I have two questions related to restricting inference.

(1) Is it possible to write a method body "inline", within another and having access to variables in the usual way, but such that the only information that the enclosing "outer" method uses is that given by the requires/ensures of the inner? (This would be analogous to the way a forall expirts only its ensures; but a forall has no executable code.)

(2) My experiments show that a loop does -not- behave this way: a loop can preserve an (outer) invariant without declaring it to be an invariant of its own. What are the rules for this?

Both these questions are to do with a recent troublesome example that mostly times out because irrelevant facts from one section are searched during proofs related to the other. In brief, I'm looking for some way of enforcing "local reasoning" only without having to declare a method, called only once, with lots of parameters.

Thanks!
Coordinator
Jun 11, 2014 at 3:55 AM
(1)

There is no direct such inlining feature at this time, but I like the idea. As you noted, there are such features for proofs, like the forall statement and the calc statement. You can perhaps hack it with a loop like this:
method M(x: int) returns (y: int)
  ensures x == y;
{
  var done := false;
  while !done
    invariant done ==> x == y;
    decreases !done;
  {
    y := x;
    done := true;
  }
}
(Btw, a forall statement can have executable code, but it's currently limited to one assignment state (see, e.g., this example). Such a forall statement does not have an ensures clause. More to the point, such a forall statement will not achieve your goals.)

(2)

I'm guessing that your point of confusion resolves around what the loop is considered to modify. Dafny (or, more precisely, Boogie) does a syntactic scan of the loop body to see which local variables are assigned to. The only thing that the verifier knows about the values of these variables at the head of loop is whatever the loop invariant says about them (plus a smidgeon of inferred properties that Boogie obtains by intervals-with-thresholds abstract interpretation; plus, also, whatever information is known from the type system, like perhaps that a particular variable is a nat). (By "head of the loop", I mean immediately before the loop guard is evaluated.) The values of other local variables are known to be preserved by the loop.

If the loop body also modifies anything in the heap, then "the heap" also becomes a syntactic loop target in the way I just described. However, for the heap, the verifier gets to use the fact that every heap update is checked against the governing "modifies" clause. The governing modifies clause is typically the modifies clause of the enclosing method, but a loop can constrain this further by declaring its own modifies clause. So, the general rule is: If the loop body does not update the heap in any way, then the verifier knows the entire heap is preserved; if the loop body causes any modification of the heap (including allocating an object), then what is known to be preserved is whatever the most closely enclosing modifies clause says (well, plus whatever user-supplied loop invariants there are).

Here is an example:
class Cell { var data: int; }

method M(c: Cell, d: Cell, n: nat)
  requires c != null && d != null && c != d;
  modifies c, d;
{
  d.data := 18;
  var i := 0;
  while i < n
    // To get the assertion below to verify, include either of the following two lines:
    // invariant d.data == 18;
    // modifies c;
  {
    c.data := c.data + 1;
    i := i + 1;
  }
  assert d.data == 18;  // error about possible assertion violation
}
Here is another example:
class Cell { var data: int; }

method M(a: array<int>, c: Cell)
  requires a != null && 100 <= a.Length && c != null;
  modifies a, c;
  ensures forall k :: 0 <= k < 100 ==> a[k] == old(a[k]) + 1;
  ensures c.data == old(c.data) + 10000;
{
  var i := 0;
  while i < 100
    invariant forall k :: 0 <= k < 100 ==> a[k] == old(a[k]) + if k < i then 1 else 0;
    invariant c.data == old(c.data) + 100*i;
  {
    a[i] := a[i] + 1;
    ghost var previousA := a[..];
    var j := 0;
    while j < 100
      invariant c.data == old(c.data) + 100*i + j;
      invariant a[..] == previousA;
    {
      c.data := c.data + 1;
      j := j + 1;
    }
    i := i + 1;
  }
}
As an alternative to the previousA trick, a simple modifies c; on the inner loop would also have let this method verify.

Rustan