CSC/ECE 517 Fall 2007/wiki3 2 dp

Topic

Find some concise examples that illustrate the principle of programming by contract, and are accessible to a general audience of programmers.

Definition

Programming by contract [1] is a software development approach that enforces the developers to define concrete and verifiable interface specifications for the software code. It is based on the theory of a business contract.

Norms of the contract

Programming by contract is a way of designing programs. Each program component has a contract which specifies how it should cooperate with the rest of the program.

This documentation is usually only written in human understandable form rather than something syntactical. eg- When given a positive real number, this function calculates its square root. This contract contains two parts, the input spesification (postive real number) and the output specification (calculates the square root).

The idea behind programming by contract is that one should make as much of this information available to the computer as possible. This means that the system itself can catch a lot of the simple errors programmers make.

The core idea of programming by contract is how components of a software system collaborate with each other on the basis of mutual obligations and benefits. The concept is drawn from the business domain where clients and suppliers agree on a contract that defines certain norms. The corresponding norms that one can associate with a software system are –

• Preconditions - [2] Certain obligations need to be fulfilled by any module which calls the software component are called as pre-conditions. The module making the call is called the client. The preconditions are the obligations that the client needs to fulfill and are benefits for the software component, called the supplier, as it frees the supplier from having to handle cases outside of the precondition.

• Postconditions - [3] The supplier in turn, needs to guarantee certain outputs or certain properties on exit. These set of properties are called the supplier's postconditions. These postconditions are obligations for the supplier, and benefits for the client obtained from calling the supplier module.

• Class invariant - [4] The supplier needs to maintain a certain property that is assumed to exist on entry and is guaranteed on exit, called the class invariant.


	   Precondition	  Postcondition
Supplier     Benefit	    Obligation
Client	    Obligation	     Benefit

Examples

A simple interface


interface Person {

/** age always positive
 * @post return > 0
 */

int getAge();

/** age always positive
  * @pre years > 0
 */

void setAge (int years);

}

class Employee implements Person {

private int age;

public int getAge() {
  return age;
}

public void setAge (int years) {
  age = years;
}

}

In the above example, the precondition for the setter method setAge is that the value of the input parameter being passed (the age of the person) should always be positive. Also, the getter method getAge has to satisfy the postcondition (obligation) that the age of the person on whom the method has been invoked is always positive. This will always be satisfied, since, the getage() method returns the value of the same variable that is set using the setage() method, and the setage() method will never allow that value to be negative.

Calculating the square root


public class SqrtExample {

    public final static double eps = 0.0001;

    //@ requires x >= 0.0;
    //@ ensures JMLDouble.approximatelyEqualTo(x, \result * \result, eps);
    
    public static double sqrt (double x) {
        return Math.sqrt(x);
    }

}

In the above example, the caller of the sqrt method (the client) needs to make sure that it is trying to find the square root of a positive number. This is the precondition. The post condition is that the method sqrt will calculate the square root of x to a precision of eps (0.0001).

Stack of integers


public class Stack {

/* @ public invariant
   @ \forall (isValidstack() == true)
     \forall (s.isEmpty == true <==> s.pop() == -1)
   @ */

public Stack() { ... }

/*@ normal behavior //non-exceptional specification
  @  // precondition
  @  requires i > 0
  @  requires i % 1 == 0
  @  //postcondition
  @  ensures \this.toString != \old.toString
  @  ensures \this.size() == \old.size + 1
  @  ensures \this.top() == i
  @  ensures \this.contains(i) == true
  @  ensures \this.pop() == \old
  @ */

//push adds a given element to the top of the stack leaving previous elements below
public void push(int i){ ... }

// pop removes the current top element of the stack
public int top() { ... }

// isEmpty checks whether the stack is empty or not
public boolean isEmpty() { ... }

//contains checks whether the stack contains the given element or not
public boolean contains(int i) { ... }

//size queries the number of elements stored in the stack
public int size() { ... }

/* toString returns a string to represent the stack content. For example, it returns 
" " for an empty stack; "8;" for a stack containing only one element 8, "8;9;" for a 
stack containing 2 elements 8 and 9 */
public String toString() { ... }

//isValidStack checks whether the stack has valid state; 
public boolean isValidStack();
}

The above implementation shows a stack of positive integers. The stack has no limit on the number of elements in it. The fact that the stack is a valid one is always true. Also, whenever a pop operation is done on an empty stack, a value of -1 is returned. Since these two things never change, they are the class invariants.

Whenever any element is to be added to the stack, the client needs to make sure that the element is positive and that it is an integer. These two requirements are the preconditions.

Also, the stack needs to ensure that whenever a push operation is performed on it, the old stack and the new resulting stack are never the same and the size of the new stack is one more than that of the old one. It also needs to ensure, that the top method always returns the latest inserted element i and if that element i is popped out, the resulting stack is the same as the old one.