CSC/ECE 517 Fall 2007/wiki3 2 at
Topic:
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 is a way of specifying the behavior of a function, and the name arises from its formal similarity to a legal contract. The key concept is viewing the relationship between a class and its clients as a formal agreement, expressing each party’s rights and obligations. Defining a precondition and a postcondition for a routine is a way to define a contract that binds the routine and its callers. The precondition states the properties that must hold whenever the routine is called; the postcondition states the properties that the routine guarantees when it returns.
By associating clauses require pre and ensure post with a routine r, the class tells its clients:
If you promise to call r with pre satisfied then I, in return, promise to deliver a final state in which post is satisfied.
Consider the following example:
'''Stack Example:''' [1] class STACK [G] feature ...Declaration of the features: count, empty, full, put, remove, item end
Before considering implementation issues, however, it is important to note that the routines are characterized by strong semantic properties, independent of any specific representation.
For example:
• Routines remove and item are only applicable if the number of elements is not zero.
• put increases the number of elements by one; remove decreases it by one.
Such properties are part of the abstract data type specification, and even people who do not use any approach remotely as formal as ADTs understand them implicitly. But in common approaches to software construction software texts reveal no trace of them. Through routine preconditions and postconditions you can turn them into explicit elements of the software.
We will express preconditions and postconditions as clauses of routine declarations introduced by the keywords require and ensure respectively. For the stack class, leaving the routine implementations blank, this gives [1]:
<u>Stack Example:</u> [1] class STACK1 [G] feature -- Access count: INTEGER -- Number of stack elements item: G is -- Top element require not empty do .... end feature -- Status report empty: BOOLEAN is -- Is stack empty? do .... end full: BOOLEAN is -- Is stack representation full? do .... end feature -- Element change put (x: G) is -- Add x on top. require not full do .... ensure not empty item = x count = old count + 1 end remove is -- Remove top element. require not empty do .... ensure not full count = old count – 1 end end
Both the require and the ensure clauses are optional; when present, they appear at
the places shown. The require appears before the local clause, if present.
Preconditions:
A precondition expresses the constraints under which a routine will function properly.
Here:
• put may not be called if the stack representation is full.
• remove and item may not be applied to an empty stack.
A precondition applies to all calls of the routine, both from within the class and from
clients. A correct system will never execute a call in a state that does not satisfy the
precondition of the called routine.
Postconditions
A postcondition expresses properties of the state resulting from a routine’s execution.
Here:
• After a put, the stack may not be empty, its top is the element just pushed, and its
number of elements has been increased by one.
• After a remove, the stack may not be full, and its number of elements has been
decreased by one.
The presence of a postcondition clause in a routine expresses a guarantee on the part
of the routine’s implementor that the routine will yield a state satisfying certain properties,
assuming it has been called with the precondition satisfied.
A precondition-postcondition pair for a routine will describe the contract that the
routine (the supplier of a certain service) defines for its callers (the clients of that service).
The following will be true for contracts between classes:
• The precondition binds the client: it defines the conditions under which a call to the
routine is legitimate. It is an obligation for the client and a benefit for the supplier.
• The postcondition binds the class: it defines the conditions that must be ensured by
the routine on return. It is a benefit for the client and an obligation for the supplier.
The benefits are, for the client, the guarantee that certain properties will hold after
the call; for the supplier, the guarantee that certain assumptions will be satisfied whenever
the routine is called. The obligations are, for the client, to satisfy the requirements as stated
by the precondition; for the supplier, to do the job as stated by the postcondition.
Here is the contract for one of the routines in stack example:
A routine contract: routine 'put' for stack class
OBLIGATIONS | BENEFITS | |
---|---|---|
Client | (Satisfy precondition:) Only call put (x) on a nonfull stack. |
(From postcondition:) Get stack updated: not empty, x on top (item yields x, count increased by 1). |
Supplier | (Satisfy postcondition:) Update stack representation to have x on top (item yields x), count increased by 1, not empty. |
(From precondition:) Simpler processing thanks to the assumption that stack is not full. |
See Also
http://en.wikibooks.org/wiki/Computer_programming/Design_by_Contract
http://www.eventhelix.com/RealtimeMantra/Object_Oriented/design_by_contract.htm
http://www.cs.uno.edu/~c1581/Labs2006/lab7/lab7.htm
http://www.phpunit.de/pocket_guide/3.2/en/test-first-programming.html
http://www.python.org/dev/peps/pep-0316/
http://www.artima.com/cppsource/deepspace2.html
http://java.sun.com/j2se/1.4.2/docs/guide/lang/assert.html
http://www.csc.calpoly.edu/~dstearns/SeniorProjectsWWW/Rideg/dbc.html
http://taipei-jackie.info/Slides/presentation_slides_2.ppt
References
[1] Object-Oriented Software Construction SECOND EDITION.
[2] http://www.ibm.com/developerworks/rational/library/455.html#N10324
[3] http://archive.eiffel.com/doc/manuals/technology/contract/page.html
[4] http://www.wayforward.net/pycontract/
[5] http://www.patentstorm.us/patents/6442750-description.html
[6] http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2004/n1613.pdf