Code contracts

Spec# ( is an example of a static program verifier that uses API contracts to prove program properties. API method contracts usually come in the form of pre- and postconditions:

void p()
  requires Pre;
  ensures Post;
  while (e)
    invariant I;

where $Pre, Post$ and $I$ are boolean expressions that are usually written in the same syntax as the code and are pure (have no side-effects). Additionally, they can use

  • logical connectives !, &&, ||, =⇒, ⇐⇒
  • quantifiers: forall, exists
  • additional special keywords e.g. sum, min, max, count, …

Other constructs that may appear:

  • result
    • method’s return value (used in postcondition)
  • old(x)
    • value of x before entry to method (used in postcondition)
  • modifies x
    • frame condition: variable x may be modified in method (usually implicitly no other)
    • defaults: modify all or modify none, depending on convention
  • assert
    • anywhere in code
    • run-time checks
    • redundant, but useful for code understanding
  • assume
    • hints for the prover
    • “escape” solution (what happens when you use assume(false) in wrong code?)
  • object invariants (more complex)
    • conditions on object variables that have to hold everywhere

There is also a readable Spec# tutorial and a set of tutorial slides that contain many examples clarifying the use and syntax of many of Spec#’s features.

  • Jahob: another verification system for Java