Question

How do labels in preconditions work?

Answer

method M0(x: int)
  requires x == 0
{
  assert x < 10; // verifies
}

method M1(x: int)
  requires Zero: x == 0
{
  // the following assertion does not verify, because labeled
  // preconditions are hidden
  assert x < 10; // error
}

method M2(x: int)
  requires Zero: x == 0
{
  // by revealing the hidden precondition, the assertion verifies
  reveal Zero;
  assert x < 10; // verifies
}

In the code example above, the precondition x == 0 is labeled with Zero. Unlabeled preconditions are assumed at the beginning of a method body, but labeled preconditions are not. Labeled preconditions are only assumed when they are explicitly revealed. So in the example, the assert in method M1 cannot be proved because the fact x < 10 is not known. In method M2, that fact is made known by the reveal statement, and so here the assert can be proved. The effect of the reveal is just as if an assumption were made at the point of the reveal statement.

Note that if the reveal statement is in a by block of an assert by statement, then the revealing is limited to the proof of the corresponding assert.

These same rules apply to labeled assert statements.

There is an expanded discussion in section 7 of Different Styles of Proofs.