Skip to content

Design by contract macros

Jump to bottom
Alex Zimin edited this page Jul 11, 2011 · 3 revisions

Table of Contents

Introduction

Languages like Eiffel, Chrome, or Spec# incorporate a methodology called Design by Contract to reason about programs, libraries, methods. It allows to write more secure and correct software and specify its behavior.

Languages following this design must support writing explicit requirements about values on which a program operates, including:

  • preconditions - some fact (boolean condition) that must be satisfied in order to call a method; mostly concerning passed parameters, but can be used to enforce any condition computable at method invocation begining
  • postconditions - a fact that must be satisfied after calling a method, for example about the return value
  • invariants - a property of a program, which does not change in time (like a non-decreasing order of elements in list, etc.)
  • other restrictions in behavior of some part of a program (like, for example, the fact that a method does not change the state of a class)
We are currently on the way to add an ability to define most of those features to Nemerle. In the following subsections we present their current state, design and plans for the future.

All the examples in this section are partial. You always need to do: 

using Nemerle.Assertions;
before using this special requieres/ensures syntax.

Preconditions - Requires attribute

Preconditions of a method (conditions that need to be satisfied before the method is called) can be specified using the Requires attribute. 

class String 
{
  public Substring (startIdx : int) : string 
  requires startIdx >= 0 && startIdx <= this.Length
  { ... }
}

Using this attribute we can add an arbitrary assertion, keeping the body of the method clean and verbose. The compiler automatically adds runtime checks at the beginning of the method. If the condition is violated, then an AssertionException is being thrown with an appropriate message containing this expression.

Requires and other attributes can occur many times before a single method. They can be also defined directly on parameters. 

ConnectTrees (requires (!tree1.Cyclic ()) tree1 : Graph,
              requires (!tree2.Cyclic ()) tree2 : Graph, 
              e : Edge) : Graph 
{ ... }

What happens when contract is violated

By default when some contract is not fulfilled in runtime we throw a special Nemerle.AssertionException and signal exactly what and where failed (the precondition expression and its location in code). You can also override this behaviour by giving expression, which will be executed when contract fails. It is done using otherwise keyword: 

getfoo (i : int) : int
requires i >= 0 && i < 5 otherwise throw System.ArgumentOutOfRangeException ($"$i is not in 0-4 range")
{ ... }

Postconditions - Ensures attribute

Following the same design, we can define postconditions which the method must satisfy. This is an assertion that must be true after the execution of the method. If the method returns a value, then a symbol value is available inside the expression stating an assertion. 

class LinkedList 
{
  public Clear () : void
  ensures this.IsEmpty
  { ... }

  public Length () : int
  ensures value >= 0
  { ... }
}

Class invariants - Invariant attribute

An even more powerful feature is to give a condition, which must be true all the time during the execution of a program. We can attach invariant to any class by writing Invariant attribute before its definition. 

class Vector [T]
invariant position >= 0 && position <= arr.Length
{
  private mutable position : int = 0;
  private arr : array [T] = array [];

  public push_back (x : T) : void 
  { ... }

This way we can ensure that the state of our object is valid according to defined rule.

This naturally brings the problem with changing variables, which are dependent on each other in invariant. Suppose we have an assertion x == y + 5 and we cannot change any of the variables. Thus, we need a mechanism for making transactions, within which invariants are temporarily turned off.

We follow the design of Spec# and add a special construct to expose the object to changes. 

expose (this) {
  x += 3;
  y += 3;
}

expose takes reference to the object to be exposed and executes the given code.

In the matter of fact, invariants are not checked all the time during execution. It would be too expensive to validate them at any assignment or call to external function. We again follow design of Spec# and run assertions at the end of expose blocks and after execution of all public methods.

Using Spec# verifier on Nemerle assemblies

Wojtek Walewski put the work on contracts even further and added ability to run Spec# static verifier on Nemerle compiled assemblies. His work is described in master thesis and can be enabled by ```nemerle using Nemerle.Contracts; ```

Clone this wiki locally