|
|
| Line 2: |
Line 2: |
| Find some concise examples that illustrate the principle of programming by contract, and are accessible to a general audience of programmers. | | Find some concise examples that illustrate the principle of programming by contract, and are accessible to a general audience of programmers. |
|
| |
|
| | |
| | <br> |
| | 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== |
|
| |
|
| 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 preconditions define the conditions whose truth the caller guarantees to ensure before calling the function, and the postconditions define the conditions whose truth the function guarantees to establish by virtue of its execution. One of the purposes in this is to avoid redundant validity checks at each level in a stack of called functions. | | 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. <br> |
| | |
| | |
| Design by contract is characterized by at least four simple assertion mechanisms. Here are some examples example written in the syntax in C++. [5]
| |
| | |
| 1. It is possible to describe function preconditions, that is, logical conditions that the implementer of the function expects to be true when the function is called.
| |
| | |
| <pre>
| |
| Example:
| |
| double sqrt( double r )
| |
| in // start a block with preconditions
| |
| {
| |
| r > 0.0: throw bad_input();
| |
| }
| |
| do // normal function body
| |
| { ... }
| |
| | |
| The precondition is read as "if r > 0.0, continue; otherwise throw an exception".
| |
| </pre>
| |
| | |
| 2. It is possible to describe function postconditions, that is, logical conditions that the implementer of the function expects to be true when the function has ended normally.
| |
| | |
| <pre>
| |
| Example:
| |
| int foo( int& i )
| |
| out // start block with postconditions
| |
| {
| |
| i == in i + 1;
| |
| return % 2 == 0;
| |
| }
| |
| do // normal function body
| |
| {
| |
| i++;
| |
| return 4;
| |
| }
| |
| | |
| The idea is that "in i" means the value of the expression "i" before the function body is evaluated. "return" is a
| |
| special variable that equals the result of the function if it exits normally.
| |
| </pre>
| |
| | |
| 3. It is possible to describe class invariants, that is, logical conditions that the implementer of the class expects to be true after the constructor has executed successfully and before and after any execution of a public member function.
| |
| | |
| <pre>
| |
| Example:
| |
|
| |
| class container
| |
| {
| |
| // ...
| |
| invariant
| |
| {
| |
| size() >= 0;
| |
| size() <= max_size();
| |
| is_empty() implies size() == 0;
| |
| is_full() implies size() == max_size();
| |
| distance( begin(), end() ) == size();
| |
| }
| |
| };
| |
| | |
| The last assertion is an example of a constraint that is infeasible even in debug code if random-access iterators
| |
| are not supported. Invariants are inherited and can never be weaker in a derived class.
| |
| </pre>
| |
| | |
| 4. It is possible to formalize the notion of overriding a virtual function; the idea can be justified by substitution principles and is referred to as subcontracting. Subcontracting consists of two simple rules that the overriding function must obey [Mey97].
| |
| (1) the precondition cannot be stronger, and
| |
| (2) the postcondition cannot be weaker.
| |
| <pre>
| |
| Example:
| |
| void Base::foo( int i ) in { i > 5; } do { ... }
| |
| void Derived::foo( int i ) do { ... }
| |
| Base& b = *new Derived;
| |
| b.foo( 5 ); // will trigger assertion
| |
| | |
| Thus the compiler will automatically OR preconditions from the base class function with the preconditions of the
| |
| overriding function and it will automatically AN D postconditions from the base class function with the
| |
| postconditions of the overriding function. Once a programmer has specified contracts, the language provides a
| |
| mechanism for checking whether the conditions hold at run-time and a mechanism to turn off this run-time check for
| |
| the sake of efficiency.
| |
| </pre>
| |
| | |
| === Some other useful examples ===
| |
| ==== Example 1 ====
| |
| Consider the following example for counting the number of vowles [1]:
| |
| | |
| <pre>
| |
| int is_vowelpair (const char *p)
| |
| {
| |
| return is_vowel(*p) && is_vowel (*(p+1));
| |
| }
| |
| | |
| int count_vowelpairs (char *s)
| |
| {
| |
| int sum = 0;
| |
|
| |
| for (; *s != '\0'; s++)
| |
| if (is_vowelpair(s))
| |
| sum++;
| |
| return sum;
| |
| }
| |
| </pre>
| |
| | |
| The functions count_vowelpairs receive as input argument a pointer to a C string. Neither function applies any validity check to the pointer, so there is an implicit precondition that the caller supply a valid pointer. To follow the rules of programming by contract we should make this an explicit precondition, albeit one that is so common and obvious that it hardly seems to need stating.
| |
| | |
| There are four possibilities for the pointer passed in as argument:
| |
| | |
| It contains a valid address that is indeed the address of a valid C string (including the null string).
| |
| It contains a valid address but the memory at that address does not comprise a valid C string.
| |
| It contains a bit pattern that is not a valid address (e.g., it is outside the addressing range, or the memory is not readable).
| |
| It contains the null pointer.
| |
| Our contract imposes the precondition that the pointer must be valid as specified in the first case above. There is no reasonable way to detect the second case, and for the third case it is usual to delegate detection (and handling) to the exception mechanism of the operating system11.
| |
| | |
| The fourth case is the interesting one. Null is a valid value for a pointer, but it is (by definition) an invalid address that will generally cause an addressing exception if dereferenced. It is, however, trivial for the function to detect that a null pointer argument has been passed. Therefore, we can propose a general rule that makes life easier for callers of a function: If a pointer to a null object is a valid argument, a null pointer should also be a valid argument with the same meaning. In the specific examples we are studying here, we should change the contract by weakening the precondition to allow the first and fourth cases, and implement the function to immediately return the value 0 if a null pointer is passed as the argument. The purpose of this rule is to relieve callers of the need to make the test for a null pointer; for a language like C the gain is not obvious, but for functional style languages like Lisp the gain is significant.
| |
| | |
| | |
| ==== Example 2 ====
| |
| Consider the following sort function in python [3]:
| |
| <pre>
| |
| def sort(a):
| |
| """Sort a list *IN PLACE*.
| |
| | |
| 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))])
| |
| </pre> | |
| This tells us everything we need to know about sort. During debugging, these statements are actually executed. If any of the pre-conditions are false, an exception is raised so the caller can be debugged. If any of the post-conditions are false, a similar exception is raised so the sort function can be debugged.
| |
| | |
| | |
| A programming language called Eiffel was created to facilitate Design by Contract. Eiffel provides built-in features to support the implementation of Design by Contract. The example below illustrates those features: [4]
| |
|
| |
|
| ==== Example 3 ====
| | One may specify the task performed by a routine by two assertions associated with the routine: |
| | | a precondition and a postcondition. The precondition states the properties that |
| The following example shows a partial implementation of a bounded queue, with methods put and remove. The pre- and post-conditions for those methods are coded explicitly with the "require" and "ensure" features of Eiffel.
| | must hold whenever the routine is called; the postcondition states the properties that the |
| | routine guarantees when it returns. |
|
| |
|
| | Consider the following example: |
| <pre> | | <pre> |
| class BoundedQueue[G] feature
| | class STACK [G] feature |
| put(x:G) is
| | ...Declaration of the features: |
| -- add x as newest element
| | count, empty, full, put, remove, item |
| require
| | end |
| not full
| |
| do
| |
| -- implementation of put
| |
| . . .
| |
| ensure
| |
| not empty
| |
| end;
| |
| remove is
| |
| -- remove oldest element
| |
| require
| |
| not empty
| |
| do
| |
| -- implementation of remove
| |
| . . .
| |
| ensure
| |
| not full
| |
| end;
| |
| empty: BOOLEAN is
| |
| -- is the queue empty?
| |
| do Result:=. . . end;
| |
| full: BOOLEAN is
| |
| -- is the queue full?
| |
| do Result:=. . . end;
| |
| end
| |
| </pre>
| |
| | |
| The assertions are checked at run-time. This checking can be turned on or off as a result of a compilation switch.
| |
| | |
| ==== Example 4 ====
| |
| The following is an example of how Programming by Contract can be implemented in C++ [5]:
| |
| | |
| The first precondition could be called a default precondition. It should be possible to remove such preconditions from object code. However, the second and the third precondition must always be part of the object code.
| |
|
| |
|
| int not_ok( int& );
| | An implementation will appear below. Before considering implementation issues, however, it is important to note that the routines are characterized by strong semantic properties, independent of any specific representation. <br> |
| int ok( int );
| |
| struct Foo { int foo(); int bar() const; };
| |
| Foo f;
| |
| Foo* f_ptr;
| |
| ...
| |
| void foo( int i )
| |
| in
| |
| {
| |
| not_ok( i ); // error: ’not_ok()’ takes a reference argument
| |
| ok( i ); // ok: ’ok()’ takes a value argument
| |
| f.foo(); // error: cannot call a non-const member
| |
| f_ptr->foo(); // error: not even through a pointer
| |
| f_ptr->bar(); // ok: bar is a const member function
| |
| f_ptr; // ok: conversion to bool
| |
| "a comment"; // ok: conversion to bool
| |
| if( ... ); // error: statements not allowed
| |
| i = 2; // error: assignment not possible
| |
| i > 0; return FAILURE_CODE; // error: ’return’ not allowed
| |
| }
| |
|
| |
|
| Postconditions are much like preconditions: (1) they are optional, (2) can include throw clauses (which are never compiled away), and (3) has the same rules regarding const-correctness. Note that postconditions are only checked when the function exits normally.
| | For example: |
| | • Routines <b>remove</b> and <b>item</b> are only applicable if the number of elements is not zero. |
| | • <b>put</b> increases the number of elements by one; <b>remove</b> decreases it by one. |
| | <br> |
|
| |
|
| int foo( int& i )
| | 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. |
| out
| |
| {
| |
| i == in i + 1; // keep track of changes to ’i’
| |
| return == 5: terminate(); // call ’terminate()’ on failure
| |
| }
| |
| do
| |
| {
| |
| ++i;
| |
| if( i % 2 == 0 )
| |
| return 5;
| |
| else
| |
| return 4;
| |
| }
| |
| Programming by contract places responsibility squarely on the shoulders of the caller for ensuring that specified preconditions for a function are met, and relieves the function of any responsibility for verifying that preconditions are met. As intended, this has the desirable effect of eliminating redundant validity checking. In real life, however, it also has an undesirable side effect: If the caller makes a mistake and does not in fact meet the preconditions, the function is likely to fail, and the cause of the failure may be difficult to track down. A pointer that is null or contains an invalid address is usually easy to diagnose; since an exception will be caused immediately an attempt is made to deference it, but other errors may cause failures far removed from the root cause.
| |
|
| |
|
| == See Also == | | == See Also == |