CSC/ECE 517 Fall 2007/wiki3 2 c4

Introduction

Problem

In class, we had some difficulty coming up with good examples of programming by contract. Find some concise ones that illustrate the principle well, and are accessible to a general audience of programmers.

Programming By Contract

Programming by contract (PBC) is also called design by contract. It is a form of progamming that deals with pre conditions, post conditions, and invariants. These are used in a client/supplier model. Pre conditions, post conditons, and invariants are specified first. After that, the code is written based on the specified conditions and invariants. It can be seen as a contract because the code needs to abide by the specifications. These contracts are enforced by assertions.[1] Programming by contract uses assertions to enforce the contract between requirements and code. PBC puts the responsibilities on the client to specify the conditions of the functions and other code to meet while and the supplier to honor these requirements that form a contract. [9]

Implementation and Reasons For

Why Use Programming By Contract?

PBC helps to define and show the responsibilities of the client and the server. [9]
Works very well with Inheritance. Any inherited methods need to conform to the contract. [9]
Able to use assertions to uphold the contract. [9]
Tests for pre-conditions as well as post-conditions. [9]
Handles abmormal cases which goes great with exception handling. [10]

How it works

The client has the responsibility of specifying the post conditions for the supplier.
The post conditions are used by the supplier to develop code.
The developed code is then given back to the client with pre-conditions.
These pre-conditions have to be honored in order for the post conditions to be honored
This in turn becomes a contract between both sides

Previous information came from reference [9].

Example 1

This example shows design by contract using a sort function in the Python Progamming language. It defines pre and post conditions for the function and also tests the function to make sure that these conditions are upheld. If any of the pre or post conditions are not upheld, an exception is thrown.

The "pre:" section defines a precondition. This precondition checks to make sure that the parameter a is an instance of a list. It also checks to see if each element within the list can be compared to all of the other elements within the list. Both of these preconditions need to be met in order for the sort function to work properly.

The "post:" section defines a postcondition. There are three conditions that are required to be met at the end of the function. First the length of the list must never change during the sorting of the list. Second, no elements should be lost or gained from sorting the list. Lastly the list has to actually be sorted. These three conditions assures the integrity of the list.

The "pre:" and "post:" together make up the contract of the function.

The function is then sorted.

The code after "# enable contract checking" is used to test the function and verify that the contract is upheld. The function is simply imported and ran with an arbitrary list.

The example below is from link 3.

def sort(a):
    """Sort a list *IN PLACE*.

    >>> a = [1, 1, 1, 1, 1, 2, 2, 1]
    >>> sort(a)
    >>> a
    [1, 1, 1, 1, 1, 1, 2, 2]
    >>> a = 'the quick brown fox jumped over the lazy dog'.split()
    >>> sort(a)
    >>> a
    ['brown', 'dog', 'fox', 'jumped', 'lazy', 'over', 'quick', 'the', 'the']

    pre:
        # must be a list
        isinstance(a, list)

        # all elements must be comparable with all other items
        forall(range(len(a)),
               lambda i: forall(range(len(a)),
                                lambda j: (a[i] < a[j]) ^ (a[i] >= a[j])))

    post[a]:
        # length of array is unchanged
        len(a) == len(__old__.a)

        # all elements given are still in the array
        forall(__old__.a, lambda e: __old__.a.count(e) == a.count(e))

        # the array is sorted
        forall([a[i] >= a[i-1] for i in range(1, len(a))])
    """
    a.sort()

# enable contract checking
import contract
contract.checkmod(__name__)

def _test():
    import doctest, sort
    return doctest.testmod(sort)

if __name__ == "__main__":
    _test()

Example 2

This example is an API example that adds a number to a list. The number has to be between 0 and 100. This example shows different ways of designing by contract. There are three functions and each one defines ever a invariant, pre-condition, or a post-condition. Notice that the assert keyword is used for upholding the contract of each condition.

"def _initparms" is the initialization for the class while "def addNumber(self, number)" adds the number to the list.

"def _invariant(self):" is an invariant that uses an assertion to verify that the length of the list doesn't exceed 100 and that there is at least one element in the list.

"def addNumber_pre_condition(self, number):" defines a pre-condition for the addNumber function. The conditions that have to be met are a variable must contain an integer only and the number must be less than 100 and greater than zero.

"def length_post_condition(self, result):" Is the post condition for the length function. This insures that after the length is found that the list is never bigger than

The pre-condition for addNumber and the post-condition for length together make up the contract of this class. The contract is enforced through the assertions and invariants.

The example below is from link 4.

class SampleTool(StandardTool):

      def _initparms(self):
          self.lst = []

      def _invariant(self):
          assert len(self.lst) < 100

      def addNumber(self, number):
          self.lst.append(number)

      def addNumber_pre_condition(self, number):
          assert type(number) == type(1), "Type must be integer"
          assert (number < 100) and (number > 0), "Number must be less than 100, but greater than 0"

      def length(self):
          return len(self.lst)

      def length_post_condition(self, result):
          assert (result < 100) and (result >= 0), "Result must be less than 100, but greater or equal 0"

Example 3

Below is a C example of two contracts for functions. Contracts in C begin with "/**" and end with "*/". They are placed directly on top of the function.

The contract below contains two preconditions and one post condition. The first pre-condition make sure that the index is greater than zero. The second makes sure that the index is less than the length of the array. The post-condition simply states that a pointer to the index element within the array passed in is what is returned.

/**
  pre: index >= 0
  pre: index < ary->length
  post: return == ary->ptr[index]
 */
void *DArray_get(DArray_T ary, long index)
{
  return ary->ptr[index];
}

The function below returns a copy of the array that is a parameter. The contract for this function contaisn a post conditions which states that the array returned must not be null. Also, the length of the copy must be equal to the length of the array copied. The last post-condition states that each element in the copied array equals each element in the original array.

/**
  post: return != NULL implies return->length == ary->length and
    forall (long i in 0...ary->length | return->ptr[i] == ary->ptr[i])
 */
DArray_T DArray_copy(DArray_T ary)
{
  /* ... */
}

Example 4

This example is written in Java and is an implementation of a stack. The implementation contains functions to push and pop off on the stack. Also, the size of stack can be determined by the Size function. The remaining function returns how many more objects can be pushed onto the stack. Pre and post conditions are implemented as well as an invariant.

"preconditions()" defines a prec-onditon for Push and a pre-condition for Pop. The pre-condition for Push is to assure that the size of the stack is less than the maximum capacity of the stack before pushing another element on it. The pre-condition for Pop is that the stack contains at least one element to be popped off.
"postconditions()" defines one post-condition for push. This post condition simply assures that after placing something on the stack it is greater than zero.
The invariant asurres that at all times the size of the stack is greater than zero and less than the maximum capacity.
The contract consists of the preconditions and post-conditions in this example.
The example is taken from link 7.

class Stack
{  
   public Stack()
   {  
      objects = new Object[MAX];
      top = 0;
   }
   public void Push(Object o)
   {  
      objects[top] = o;
      top++;
   }
   public Object Pop()
   {  
      top--;
      return  objects[top];
   }
   public int Size()
   {  
      return  top;
   }
   
   private int Remaining()
   {  
      assert (false);
      return  MAX - top;
   }
   
   private Object[] objects;
   private int top;
   private static final int MAX = 10;
   
   preconditions()
   {  
      Push:
      top < MAX;
      Pop:
      top > 0;
   }
   
   postconditions()
   {  
      Push:
      top > 0;
   }
   
   invariants()
   {  
      top >= 0;
      top <= MAX;
   }
}

CSC/ECE 517 Fall 2007/wiki3 2 c4

Contents

Introduction

Problem

Programming By Contract

Implementation and Reasons For

Why Use Programming By Contract?

How it works

Example 1

Example 2

Example 3

Example 4

References

Navigation menu

CSC/ECE 517 Fall 2007/wiki3 2 c4

Introduction

Problem

Programming By Contract

Implementation and Reasons For

Why Use Programming By Contract?

How it works

Example 1

Example 2

Example 3

Example 4

References

Navigation menu

Search