Specification Syntax Method Contracts

Method contracts specify the behaviour of the method that is visible to the calling environment, by means of pre-conditions and post-conditions. Pre-conditions use the keyword requires and restrict the situations in which the method can be invoked, e.g. restricting parameters to be non-null. Post-conditions use the keyword ensures and describe the behaviour of the method by defining the program state after the call finishes. The method contract is placed above the method header, and these keywords can only be used in combination with a method header.

Two useful keywords to define the post-state (i.e. the state after the method finishes) are \result to refer to the return value of the (non-void) method, and \old(expr) to refer to the value of expr before the method's execution.

class Test {
  /*@
  requires x >= 0;
  requires y >= 0;
  ensures \result == x+y;
  ensures \result >= 0;
  @*/
  public int add(int x, int y) {
    return x+y;
  }

  /*@
  requires xs != null;
  ensures \result != null;
  ensures \result.length == \old(xs.length)+1;
  ensures \result.length > 0;
  @*/
  public int[] append(int[] xs, int y) {
    int[] xsCopy = new int[xs.length + 1];
    /* ... */
    return xsCopy;
  }
}

Recall that VerCors analyses methods in isolation, purely based on their contract and independent from any actual calling contexts. It tries to prove that if the pre-condition is satisfied before the method body is executed, then the post-condition holds afterwards. In the example of the add method above, if the input parameters are non-negative, then the result is, too. Note that the pre-condition x>=0 is not actually required for executing the method body, but it is necessary to prove the post-condition. In contrast, in the example of append, the pre-condition xs!=null is actually needed for \old(xs.length) to be well-defined, and potentially to prove absence of null-pointer dereferences in the method body. Note that, to fully specify the correct behaviour of append, one would have to compare the values inside of xs and \result. Since these values are stored on the heap (and not on the stack like the reference xs itself), this would require access permissions, which will be introduced in the next section Permissions.

[!Note] Method contracts must not have side effects, so for example calls to (non-pure) methods are forbidden inside contracts.

[!Important] Pre- and post-conditions are processed in-order, so for example swapping the order of two pre-conditions could result in a failed verification (e.g. you need to specify that an integer variable is within range before you can use it as an array index in another pre-condition).

[!Caution] Unsatisfiable pre-conditions (e.g. contradictory conditions, or simply false) can lead to unexpected results, because the implication "if pre-condition before, then post-condition after" becomes trivially true for any post-condition, and VerCors is able to prove any arbitrary statement.

Context: Sometimes, the same expression is needed as a pre- and as a post-condition, for example the fact that a global variable is not null. In that case, the keyword context can be used as a short-hand notation: context xs != null; stands for requires xs!=null; ensures xs!=null;. An even further reaching short-hand is context_everywhere expr;, which adds expr as a pre- and as a post-condition, as well as a loop invariant for all loops inside the method body (see the section on Auxiliary Annotations).

Contracts for C declarations

When verifying C programs, function contracts can also be placed on function declarations:

// c-example.h
##ifndef _C_EXAMPLE_H
##define _C_EXAMPLE_H

extern int x;

/*@
  requires Perm(x,1);
  ensures Perm(x,1) ** x==\old(x)+1;
@*/
extern void test();

##endif

Implementing a declaration: If an implementation for the annotated function-declaration is provided to VerCors, the implementation is checked against the specification. E.g. the following implementation of test() is verified against the specification above:

// c-example-impl.c
#include "c-example.h"

int x;

void test(){
  x=x+1;
}

Using a declaration: When an annotated function declaration is included and used in a C-file and no implementation for the included function is provided, the specification is assumed to be true. E.g. in the following case, the contract of test() is assumed to be true and not checked because no implementation of test() is provided:

// c-example-use.c
#include "c-example.h"

/*@
  requires Perm(x,1);
  ensures Perm(x,1) ** x==4;
@*/
void use(){
  x=3;
  test();
}

[!Caution] When using contracts without providing an implementation, one has to be careful to make sure that the contract does not contain inconsistencies. Otherwise, its use can lead to unsoundness.