C0 | Documentation
About Downloads Tutorial References Courses
C0 Tutorial C0 and other languages Other references

Contracts

One of the novel aspects of C0 is the use of contracts. We use this term to refer to annotations we make in the program to express what a program or part of a program is supposed to accomplish, as opposed to how it should compute. In various places in this tutorial we have already used contracts when introducing individual constructs. Here we summarize some general properties and advice.

Contracts have one of the two general forms

//@anno

/*@anno1
  @anno2
  ...
  @*/

where the first one extends through the remainder of the line after //@, while the latter potentially extends over multiple lines in between /*@ and @*/. The are modeled after C and C++ or Java-style Comments, emphasizing that they are executed only when coin or cc0 are invoked with the -d flag.

There are four different kinds of annotations, @requires e;, @ensures e;, @loop_invariant e;, and @assert e;. In each case, e is a boolean expression (returning true or false), where false indicates a violation of a contract. If a contract is violated, program execution will abort with an error message pinpointing the failing contract. If you execute without the -d flag, of course, annotations are ignored and the program will continue despite the contract violation making it more difficult to find the error.

It it important that contract expressions do not have effects, such as mutating the state. This ensures that the correct programs will execute identically, no matter whether contracts are checked or not.

@requires and @ensures

The @requires and @ensures contracts are associated with functions. They always must appear between the function header, which gives the types of arguments and the result, and the body of the function. @requires e; expresses that the boolean condition e must hold of the function's arguments; @ensures e; expresses that the boolean condition e must hold when the function returns. This information can range from a simple restriction on arguments and promise on the result to a complete specification of the function. We call a requires clause a precondition of the function, an ensures clause a postcondition.

The following is an integer logarithm function to base 2. The contract states only that the argument must be strictly positive (since log(0) is undefined), and promises that the result will be positive but could include 0 (since 20 = 1).

/* file log1.c0 */

int log(int x)
//@requires x >= 1;
//@ensures \result >= 0;
{ int r = 0;
  while (x > 1) {
    x = x / 2;
    r = r + 1;
  }
  return r;
}

Note the special identifier \result that can only be used in @ensures annotations and refers to the result returned by the function.

Working towards a full specification we note that if x is a power of 2, then 2r = x. However, we might round down because x = x/2; rounds down, so we only have 2r ≤ x. We cannot add this directly to the postcondition (@ensures) because x is modified in the loop, but the postcondition should speak about the original x. So we modify the function slightly, using a temporary variable y instead of x during the iteration. We use (1 << r) to implement exponentiation 2r.

/* file log2.c0 */
int log(int x)
//@requires x >= 1;
//@ensures \result >= 0;
//@ensures (1 << \result) <= x;
{ int r = 0;
  int y = x;
  while (y > 1) {
    y = y / 2;
    r = r + 1;
  }
  return r;
}

We see that the preconditions (@requires) can refer to the function's parameters, while the postcondition can refer to the parameters (as long as they are not modified) and the special variable \result.

It would be interesting to say even more, to make sure the result is really the integer logarithm, but we leave this as an exercise to the reader.

@loop_invariant

The second form of contract we discuss is a loop invariant. A loop invariant must be true every time just before the exit condition is tested. It must appear just before the loop body. Continuing the logarithm example from above, the following contains two loops invariants. The first one states that y must always be greater or equal to 1, and the second that the result variable r will be greater or equal to 0.

/* file log4.c0 */

int log(int x)
//@requires x >= 1;
//@ensures \result >= 0;
{ int r = 0;
  int y = x;
  while (y > 1)
    //@loop_invariant y >= 1 && r >= 0;
    {
      y = y / 2;
      r = r + 1;
    }
  return r;
}

You should convince yourself that this is indeed a valid loop invariant, and that it is sufficient to prove the postcondition of the function. We do not explain this reasoning process here, but refer to the lecture notes of the course on Principles of Imperative Computation. If we want the stronger postcondition, we should also have a stronger loop invariant, something that often requires considerable ingenuity. Here is a possibility for this function.

/* file log5.c0 */
int log(int x)
//@requires x >= 1;
//@ensures \result >= 0;
//@ensures (1 << \result) <= x;
{ int r = 0;
  int y = x;
  while (y > 1)
    //@loop_invariant y >= 1 && r >= 0;
    //@loop_invariant y * (1 << r) <= x;
    {
      y = y / 2;
      r = r + 1;
    }
  return r;
}

@assert

Sometimes while reasoning about our code we want to make a property we have established or conjectured explicit. The @assert annotation must always guard a statement; it cannot be at the end of a block. Continuing the logarithm example, we may be worried about overflow since C0 is defined to use modular arithmetic. Because of that, it is possible that r+1 < 0, namely if r is already the maximal integer. However, this cannot happen because r will always be smaller than x. To document that, we could add the line //@assert r < x to the code.

/* file log6.c0 */

int log(int x)
//@requires x >= 1;
//@ensures \result >= 0;
//@ensures (1 << \result) <= x;
{ int r = 0;
  int y = x;
  while (y > 1)
    //@loop_invariant y >= 1 && r >= 0;
    //@loop_invariant y * (1 << r) <= x;
    {
      y = y / 2;
      //@assert r < x;
      r = r + 1;
    }
  return r;
}

This condition, like the other contracts, should never fail and id therefore only executed when dynamic checking is enabled with the -d flag to coin or cc0.

There is also an assert statement which is always executed, not just when we check dynamically. It is appropriate for parts of function contracts that may easily be overlooked and are inexpensive to test, so the efficiency of the functions are not compromised. It is also used for testing. For example:

/* file log-test.c0 */
#use <conio>

int main() {
  assert(log(1) == 0);
  assert(log(2) == 1);
  assert(log(3) == 1);
  assert(log(4) == 2);
  for (int k = 1; k < 31; k++) {
    assert(log(1<<k) == k);
    assert(log((1<<k)-1) == k-1);
    assert(log((1<<k)+1) == k);
  }
  print("All tests passed!\n");
  return 0;
}

which can be used to test various implementation of the logarithm. For example

% cc0 -d log6.c0 log-test.c0
% ./a.out
All tests passed!
0
%