| 1 |
Ddoc |
|---|
| 2 |
|
|---|
| 3 |
$(SPEC_S Contract Programming, |
|---|
| 4 |
|
|---|
| 5 |
Contracts are a breakthrough technique to reduce the programming effort |
|---|
| 6 |
for large projects. Contracts are the concept of preconditions, postconditions, |
|---|
| 7 |
errors, and invariants. |
|---|
| 8 |
Contracts can be done in C++ without modification to the language, |
|---|
| 9 |
but the result is |
|---|
| 10 |
clumsy and inconsistent. |
|---|
| 11 |
<p> |
|---|
| 12 |
|
|---|
| 13 |
Building contract support into the language makes for: |
|---|
| 14 |
|
|---|
| 15 |
$(OL |
|---|
| 16 |
$(LI a consistent look and feel for the contracts) |
|---|
| 17 |
$(LI tool support) |
|---|
| 18 |
$(LI it's possible the compiler can generate better code using information gathered |
|---|
| 19 |
from the contracts) |
|---|
| 20 |
$(LI easier management and enforcement of contracts) |
|---|
| 21 |
$(LI handling of contract inheritance) |
|---|
| 22 |
) |
|---|
| 23 |
|
|---|
| 24 |
<img src="d4.gif" alt="Contracts make D bug resistant" border=0> |
|---|
| 25 |
|
|---|
| 26 |
The idea of a contract is simple - it's just an expression that must evaluate to true. |
|---|
| 27 |
If it does not, the contract is broken, and by definition, the program has a bug in it. |
|---|
| 28 |
Contracts form part of the specification for a program, moving it from the documentation |
|---|
| 29 |
to the code itself. And as every programmer knows, documentation tends to be incomplete, |
|---|
| 30 |
out of date, wrong, or non-existent. Moving the contracts into the code makes them |
|---|
| 31 |
verifiable against the program. |
|---|
| 32 |
|
|---|
| 33 |
<h2>Assert Contract</h2> |
|---|
| 34 |
|
|---|
| 35 |
The most basic contract is the |
|---|
| 36 |
<a href="expression.html#AssertExpression">assert</a>. |
|---|
| 37 |
An assert inserts a checkable expression into |
|---|
| 38 |
the code, and that expression must evaluate to true: |
|---|
| 39 |
------ |
|---|
| 40 |
assert(expression); |
|---|
| 41 |
------ |
|---|
| 42 |
C programmers will find it familiar. Unlike C, however, an <code>assert</code> |
|---|
| 43 |
in function bodies |
|---|
| 44 |
works by throwing an <code>AssertError</code>, |
|---|
| 45 |
which can be caught and handled. Catching the contract violation is useful |
|---|
| 46 |
when the code must deal with errant uses by other code, when it must be |
|---|
| 47 |
failure proof, and as a useful tool for debugging. |
|---|
| 48 |
|
|---|
| 49 |
<h2>Pre and Post Contracts</h2> |
|---|
| 50 |
|
|---|
| 51 |
The pre contracts specify the preconditions before a statement is executed. The most |
|---|
| 52 |
typical use of this would be in validating the parameters to a function. The post |
|---|
| 53 |
contracts validate the result of the statement. The most typical use of this |
|---|
| 54 |
would be in validating the return value of a function and of any side effects it has. |
|---|
| 55 |
The syntax is: |
|---|
| 56 |
|
|---|
| 57 |
------ |
|---|
| 58 |
in |
|---|
| 59 |
{ |
|---|
| 60 |
...contract preconditions... |
|---|
| 61 |
} |
|---|
| 62 |
out (result) |
|---|
| 63 |
{ |
|---|
| 64 |
...contract postconditions... |
|---|
| 65 |
} |
|---|
| 66 |
body |
|---|
| 67 |
{ |
|---|
| 68 |
...code... |
|---|
| 69 |
} |
|---|
| 70 |
------ |
|---|
| 71 |
By definition, if a pre contract fails, then the body received bad |
|---|
| 72 |
parameters. |
|---|
| 73 |
An AssertError is thrown. If a post contract fails, |
|---|
| 74 |
then there is a bug in the body. An AssertError is thrown. |
|---|
| 75 |
<p> |
|---|
| 76 |
Either the <code>in</code> or the <code>out</code> clause can be omitted. |
|---|
| 77 |
If the <code>out</code> clause is for a function |
|---|
| 78 |
body, the variable <code>result</code> is declared and assigned the return |
|---|
| 79 |
value of the function. |
|---|
| 80 |
For example, let's implement a square root function: |
|---|
| 81 |
------ |
|---|
| 82 |
long square_root(long x) |
|---|
| 83 |
in |
|---|
| 84 |
{ |
|---|
| 85 |
assert(x >= 0); |
|---|
| 86 |
} |
|---|
| 87 |
out (result) |
|---|
| 88 |
{ |
|---|
| 89 |
assert((result * result) <= x && (result+1) * (result+1) >= x); |
|---|
| 90 |
} |
|---|
| 91 |
body |
|---|
| 92 |
{ |
|---|
| 93 |
return cast(long)std.math.sqrt(cast(real)x); |
|---|
| 94 |
} |
|---|
| 95 |
------ |
|---|
| 96 |
The assert's in the in and out bodies are called <dfn>contracts</dfn>. |
|---|
| 97 |
Any other D |
|---|
| 98 |
statement or expression is allowed in the bodies, but it is important |
|---|
| 99 |
to ensure that the |
|---|
| 100 |
code has no side effects, and that the release version of the code |
|---|
| 101 |
will not depend on any effects of the code. |
|---|
| 102 |
For a release build of the code, the in and out code is not |
|---|
| 103 |
inserted. |
|---|
| 104 |
<p> |
|---|
| 105 |
If the function returns a void, there is no result, and so there can be no |
|---|
| 106 |
result declaration in the out clause. |
|---|
| 107 |
In that case, use: |
|---|
| 108 |
------ |
|---|
| 109 |
void func() |
|---|
| 110 |
out |
|---|
| 111 |
{ |
|---|
| 112 |
...contracts... |
|---|
| 113 |
} |
|---|
| 114 |
body |
|---|
| 115 |
{ |
|---|
| 116 |
... |
|---|
| 117 |
} |
|---|
| 118 |
------ |
|---|
| 119 |
In an out statement, $(I result) is initialized and set to the |
|---|
| 120 |
return value of the function. |
|---|
| 121 |
|
|---|
| 122 |
<h2>In, Out and Inheritance</h2> |
|---|
| 123 |
|
|---|
| 124 |
$(P If a function in a derived class overrides a function in its |
|---|
| 125 |
super class, then only one of |
|---|
| 126 |
the $(TT in) contracts of the function and its base functions |
|---|
| 127 |
must be satisfied. |
|---|
| 128 |
Overriding |
|---|
| 129 |
functions then becomes a process of $(I loosening) the $(TT in) |
|---|
| 130 |
contracts. |
|---|
| 131 |
) |
|---|
| 132 |
|
|---|
| 133 |
$(P A function without an $(TT in) contract means that any values |
|---|
| 134 |
of the function parameters are allowed. This implies that if any |
|---|
| 135 |
function in an inheritance hierarchy has no $(TT in) contract, |
|---|
| 136 |
then $(TT in) contracts on functions overriding it have no useful |
|---|
| 137 |
effect. |
|---|
| 138 |
) |
|---|
| 139 |
|
|---|
| 140 |
$(P Conversely, all of the $(TT out) contracts needs to be satisfied, |
|---|
| 141 |
so overriding functions becomes a processes of $(I tightening) the |
|---|
| 142 |
$(TT out) |
|---|
| 143 |
contracts. |
|---|
| 144 |
) |
|---|
| 145 |
|
|---|
| 146 |
<h2>Class Invariants</h2> |
|---|
| 147 |
|
|---|
| 148 |
$(P Class invariants are used to specify characteristics of a class that |
|---|
| 149 |
always |
|---|
| 150 |
must be true (except while executing a member function). |
|---|
| 151 |
They are described in $(LINK2 class.html, Classes). |
|---|
| 152 |
) |
|---|
| 153 |
|
|---|
| 154 |
<h2>References</h2> |
|---|
| 155 |
|
|---|
| 156 |
$(LINK2 http://people.cs.uchicago.edu/~robby/contract-reading-list/, Contracts Reading List)<br> |
|---|
| 157 |
$(LINK2 http://pandonia.canberra.edu.au/java/contracts/paper-long.html, Adding Contracts to Java)<br> |
|---|
| 158 |
|
|---|
| 159 |
) |
|---|
| 160 |
|
|---|
| 161 |
Macros: |
|---|
| 162 |
TITLE=Contract Programming |
|---|
| 163 |
WIKI=DBC |
|---|