Contracts on blocks

Complex functions can overwhelm the theorem prover. For such cases, the function can be broken into separate blocks with their individual contracts. Syntactically, these blocks are specified using the block keyword as such:

#include <vcc.h>

int foo(int i)
  requires(i < 10)
  ensures(result == i + 2)
{
  i++;
  block
    requires(i < 11)
    ensures(i == old(i) + 1)
  {
    i++;
  }
  assert(i < 12);
  return i;
}


Internally, the block is transformed extracted into a function and replaced by a call to that function. As you can see in the example above, old can be used in the ensures clause to refer to the value of locals at the beginning of the block.

Similar to the requires and ensures clauses, a block may also specify reads and writes clauses.

A block extracted in this fashion must not contain a return statement or a goto, break, or continue that jumps outside of the block.

Last edited Nov 13, 2009 at 1:06 PM by stobies, version 3

Comments

No comments yet.