>
0/0/00
Design by Contract
1
Design by contract
Object-Oriented
Software Construction by Bertrand Meyer, Prentice Hall
The presence of
a precondition or postcondition in a routine is viewed as a contract.
0/0/00
Design by Contract
2
Rights and obligations
Parties in the contract:
class and clients
require pre, ensure
post with method r: If you promise to call r with pre satisfied then
I, in return, promise to deliver a final state in which post is satisfied.
Contract: entails
benefits and obligations for both parties
0/0/00
Design by Contract
3
Rights and obligations
Precondition binds
clients
Postcondition binds
class
0/0/00
Design by Contract
4
Example
0/0/00
Design by Contract
5
If precondition
is not satisfied
If client00 part
of the contract is not fulfilled, class can do what it pleases: return
any value, loop indefinitely, terminate in some wild way.
Advantage of convention:
simplifies significantly the programming style.
0/0/00
Design by Contract
6
Source of complexity
Does data passed
to a method satisfy requirement for correct processing?
Problem: no checking
at all or: multiple checking.
Multiple checking:
conceptual pollution: redundancy; complicates maintenance
Recommended approach:
use preconditions
0/0/00
Design by Contract
7
Class invariants
and class correctness
Preconditions and
postconditions describe properties of individual methods
Need for global
properties of instances which must be preserved by all routines
0<=nb_elements;
nb_elements<=max_size
empty=(nb_elements=0);
0/0/00
Design by Contract
8
Class invariants
and class correctness
A class invariant
is an assertion appearing in the invariant clause of the class.
Must be satisfied
by all instances of the class at all 00table00times (instance in
stable state):
on instance creation
before and after
every remote call to a routine (may be violated during call)
0/0/00
Design by Contract
9
Class invariants
and class correctness
A class invariant
only applies to public methods; private methods are not required to
maintain the invariant.
0/0/00
Design by Contract
10
Invariant Rule
An assertion I is
a correct class invariant for a class C iff the following two conditions
hold:
The constructor
of C, when applied to arguments satisfying the constructor00 precondition
in a state where the attributes have their default values, yields a
state satisfying I.
Every public method
of the class, when applied to arguments and a state satisfying both
I and the method00 precondition, yields a state satisfying I.
0/0/00
Design by Contract
11
Invariant Rule
Precondition of
a method may involve the initial state and the arguments
Postcondition of
a method may only involve the final state, the initial state (through
old) and in the case of a function, the returned value.
The class invariant
may only involve the state
0/0/00
Design by Contract
12
Invariant Rule
The class invariant
is implicitly added (anded) to both the precondition and postcondition
of every exported routine
Could do, in principle,
without class invariants. But they give valuable information.
Class invariant
acts as control on evolution of class
A class invariant
applies to all contracts between a method of the class and a client
0/0/00
Design by Contract
13
Definitions
Class C
INV class invariant
method r: prer(xr)
precondition; postr postcondition
xr: possible
arguments of r
Br: body
of method r
DefaultC:
attributes have default values
0/0/00
Design by Contract
14
Correctness
of a class
A class C is said
to be correct with respect to its assertions if and only if
For every public
method r other than the constructor and any set of valid arguments xr:
{INV and prer(xr)} Br {INV and postr}
For any valid set
of arguments xCreate to the constructor:
{DefaultC and preCreate(xCreate)} BCreate
{INV}
0/0/00
Design by Contract
15
Subcontracting:
what inheritance is about
Subcontractor must
do job originally requested. Can do more but not less.
Could do less by
requesting a
stronger precondition
ensuring a weaker
postcondition
Could do more by
accepting weaker
precondition
guaranteeing a stronger
postcondition
0/0/00
Design by Contract
16
How to prove
correctness
A complex story
0/0/00
Design by Contract
17
The End
download Design by contract
