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.

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

/**
  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. Pre and post conditions are implemented as well as an invariant. 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;
   }
}

Example 5

This example is written in Java. Below is two functions that use assertions to check for null and in range. The example is taken from link 8.

/**
 * This method asserts that a specified object is not null.
 * @param object - the object that should not be null.
 * @param name - the name of the object to be used for error reporting.
 */
public final static boolean notNull(Object object, String name) {
	assert object != null: name + " must not be null";
	return true;
}

/**
 * This method asserts that an int value is within a specified range.
 * @param value - the value that must be within the specified range.
 * @param min - the minimum value specified of the specified range.
 * @param max - the maximum value of the specified range.
 * @param name - the name of the value to be used for error reporting.
 */
public final static boolean inRange(int value, int min, int max, String name) {
	assert value >= min && value <= max: name + " must be in the range [" + min + " to " + max + "]. Value is " + value;
	return true;
}

References

1. http://www.dugaldmorrow.com/index.php?option=com_content&task=view&id=19&Itemid=38
2. http://www.javaworld.com/javaworld/jw-02-2001/jw-0216-cooltools.html?page=1
3. http://www.wayforward.net/pycontract/
4. http://pyds.muensterland.org/wiki/programmingbycontractforwebservices.html
5. http://www.javaworld.com/javaworld/jw-11-2001/jw-1109-assert.html?page=2
6. http://www.codeproject.com/csharp/designbycontract.asp
7. http://mozart-dev.sourceforge.net/pi-assert.html
8. http://www.dugaldmorrow.com/index.php?option=com_content&task=view&id=19&Itemid=38
9. http://onestepback.org/index.cgi/Tech/Programming/DbcAndTesting.html
10. http://archive.eiffel.com/doc/manuals/technology/contract/
11. http://www.muc.de/~hoelzl/tools/dbc/dbc.lisp
12. http://www.onlamp.com/pub/a/onlamp/2004/10/28/design_by_contract_in_c.html