Software Construction: Assignment 3 (Worth 100 Points)
NDSU CSCI 717 Software Construction
Design By Contract
Textbook
Bertrand Meyer. Object-Oriented Software Construction, 2nd Edition, Prentice-Hall PTR, 1997. Chapters 11 and 12.
2
Outline
Correctness Formula
Assertions and Contracts
Class Invariants
When Is a Class Correct?
ADT Connection
Loop Invariants and Variants
Using Assertions
Exception Handling
3
Is x := y + 1 Correct?
“Make sure that x and y have different values”
“Make sure that x has a negative value”
Correctness is a relative notion.
Need to get not only the program but also a precise description of what it is supposed to do
Specification!
4
Reliability: Correctness & Robustness
Correctness
The ability of software products to perform their exact tasks, as defined by their specification
Robustness
The ability of software systems to react appropriately to abnormal conditions
Need a mechanism for expressing and validating correctness arguments.
5
Reliability via Design By Contract
Viewing the relationship between a class and its clients as a formal agreement
Expressing each party’s rights and obligations.
Through a precise definition of every module’s claims and responsibilities, we hope to attain a significant degree of trust in large systems.
6
Correctness Formula
{P} A {Q} – a.k.a. Hoare Triples
A – operation/routine
P – precondition
Q – postcondition
“Any execution of A, starting in a state where P holds, will terminate in a state where Q holds.”
7
Correctness Formula: Example
{x >= 9} x := x + 5 {x >= 13}
Given {x >= 9}, the most interesting postcond?
{x >= 14}
Strongest possible
Given {x>=13}, the most interesting precond?
{x>=8}
Weakest possible
8
Weak and Strong Conditions
P1 is stronger than P2 if P1 implies P2 (P1≠P2)
i.e. P2 is weaker than P1
legitimate to speak of True as the weakest and False as the strongest of all possible assertions.
Every proposition implies True
False implies every proposition
9
{P}A{Q}: Employee Perspective
Job Ad: “We are looking for someone whose work will be to start from initial situations as characterized by P, and deliver results as defined by Q”.
Assume a friend is looking for a job and comes across several such ads, all with similar salary and benefits, but differing by their Ps and Qs.
Lazy friend wants the easiest possible job: sinecure
Recommend for P/Q: choose a job with a weaker or stronger precondition/postcondition?
10
{P}A{Q}: Employee Perspective-cont
Sinecure 1: {False} A {…}
The stronger the P, the easier for the employee
Only have to deal with a more limited set of situations
False, the strongest possible, is never satisfied
Any request to execute A will be incorrect, the fault lies not with A but with the requester
Who did not observe the required precondition
Whatever A does or does not do may be useless, but A is always correct!
Do you want/know any of such jobs?
11
{P}A{Q}: Employee Perspective-cont
“Obvious — it is the only job where the customer is always wrong”
why a famous police chief had chosen his career.
12
{P}A{Q}: Employee Perspective - cont
Sinecure 2: {…} A {True}
A strong postcond is bad news - you have to deliver more results.
The weaker the Q, the better for the employee.
True, the weakest possible, is satisfied by all states
Sinecure1 and Sinecure2, which is better?
13
{P}A{Q}: Employee Perspective - cont
With Sinecure1, A is always correct!
No states satisfy P, so it does not matter what A does, even if A’s execution would go into an infinite loop or crash the computer.
With Sinecure 2, there must be a final state.
The final state does not need to satisfy any specific properties, but it must exist.
“You need to do nothing, but must do it in finite time”
Sinecure 2 is only the “second best” job!
14
{P}A{Q}: Employer Perspective
Everything is reversed.
A weaker precond is good news: a job that handles a broader set of input cases
A stronger postcond means more significant results
For contracts between clients and suppliers, a benefit for one is an obligation for the other!
15
Introducing Assertions into Programs
Assertion
An expression stating a property that some entities may satisfy at certain stages of program execution.
Notation: predicates+ extensions
; and
: between label and component
n > 0 ; x /= Void
Positive: n > 0
Not_void: x /= Void
16
Preconditions and Postconditions
Routines are characterized by strong semantic properties, independent of specific representation
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.
Require: precondition stating the properties that must hold whenever the routine is called
Ensure: postcondition stating the properties that the routine guarantees when it returns.
17
Stack
class STACK1 [G]
feature -- Access
count: INTEGER is
-- Number of stack elements
item: G is
-- Top element
require // may not be applied to an empty stack
not empty
do
…
end
18
Stack: status report & element change
feature -- Status report
empty: BOOLEAN is
-- Is stack empty?
do … end
full: BOOLEAN is
-- Is stack representation full?
do … end
feature -- Element change
put, move (next two slides)
19
Stack: put
put (x: G) is
-- Add x on top.
Require // put may not be called
not full
do
…
ensure
not empty // the stack may not be empty
item = x // its top is the element just pushed
count = old count + 1 // count increased by one
end
20
Stack: remove
remove is
-- Remove top element.
require // may not be applied to an empty stack
not empty
do
…
ensure
not full // the stack may not be full
count = old count – 1 // count decreased by 1
end
21
Contracting for Software Reliability
Contract
require pre and ensure post with a routine r
A pre/postcond pair for a routine is the contract that the routine (supplier) defines for its callers (clients)
Rights and Obligations
“If you promise to call r with precond satisfied then I, in return, promise to deliver a final state in which postcond is satisfied.”
The precond is an obligation for the client and a benefit for the supplier.
The postcond is a benefit for the client and an obligation for the supplier.
22
Obligations and Benefits: Stack
| put | Obligations | Benefits |
| Client | (Satisfy precondition:) Only call put (x) on a non-full stack. | (From postcondition:) Get stack updated: not empty, x on top (item yields x, count increased by 1). |
| Supplier | (Satisfy postcondition:) Update stack 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. |
23
Non-Redundancy Principle
Under no circumstances shall the body of a routine ever test for its precondition.
A precondition is a benefit for the supplier;
If the call does not satisfy the precond, the routine is not bound by the postcond - it may do what it pleases
Advantages
Simplicity
“The more we write, the more we will have to write”.
Performance
Zen–style paradox – “get more reliability the best policy is often to check less”
Reverse of defensive programming
A redundant check might not help,but at least it will not hurt
24
Understanding Assertions
Assertions are no input checking mechanism
Concern: software-to-software communication, not software-to-human or software-to-outside-world.
In obtaining information from the outside you cannot rely on preconditions - use input validation or “filter”
Assertions are not control structures
Assertions express correctness conditions.
If sqrt handles negative arguments a certain way, and non-negatives another way, a require clause is not what you need.
25
Who’s Fault?
Programmer A
double x = -1;
double y = sqrt(x);
assert abs(y*y-x)<eps
// failure
26
Programmer B
double sqrt(double x)
{
//…
}
Assertion Violation Rules
A run-time assertion violation is the manifestation of a bug.
A precondition violation - a bug in the client
The client did not observe its part of the deal.
A postcondition violation - a bug in the supplier.
The supplier was not able to fulfill its contract.
27
Precondition Design
Demanding
Assign the responsibility to clients - the condition will appear as part of the routine’s precondition
An experienced contractor expects his clients to “do their homework” before calling on him;
He has no trouble finding business, and will reject requests that appear too broad or unreasonable.
Tolerant
The condition will appear in an if- then or an equivalent control structure in the routine.
A freshly established consulting practice, whose owner is so desperate for business
He will take anything
28
28
Tolerant Version of remove
remove is
-- Remove top element
// no precondition
do
if empty then
print ("Error: attempt to pop an empty stack")
else
count := count – 1
end
end
29
Demanding in Design by Contract
Demanding does not mean to produce routines that assign all things to all clients.
Insists that each routine
Do a well-defined job and do it well
Correctly, efficiently, generally enough to be reusable by many clients
Specify clearly what cases it cannot handle.
Only applicable if preconds remain reasonable
O.W. require False makes any routine body correct
30
Reasonable Precondition Principle
Every routine precond in a “demanding” design approach must satisfy these requirements:
The precond appears in the official documentation distributed to authors of client modules.
It is possible to justify the need for the precondition in terms of the specification only.
Examples
remove’s precond: not empty
sqrt’s precond: x>0
Logical requirements, not for supplier’s implementation convenience
31
Precondition Availability Rule
To be satisfiable by the clients
The precond must not use features hidden from the clients as a result of export restrictions
Every feature in the precond must be available to every client to which the routine is available
Every client that is in a position to call the feature will also be in a position to check for its precond.
No such rule for postconds
It’s not an error for a postcond to refer to secret features.
32
Precondition Availability Rule - cont
-- an invalid class, for illustration only
class SNEAKY feature
tricky is // exports tricky to all clients
require
accredited // keeps accredited secret
do … end
feature {NONE}
accredited: BOOLEAN is do … end
end
Clients have no way of finding out, before a call, whether the call is indeed correct.
33
Demanding vs Tolerant
Demanding
Usually the right one for modules whose clients are other software modules
Exception: modules intended for clients whose authors use a non-OO language or may not understand DBC
Tolerant
Useful for software elements that deal with data coming from the outside world, such as user input, or sensor data.
34
Class Invariants
Class invariant - a set of assertions, expressing general consistency constraints that every class instance will satisfy at all “stable” times:
The state that results from the creation of an object
The states immediately before and after a call
May involve attributes, routines, and both
0 <= count && count <= capacity
empty = (count = 0)
Does not need to be satisfied at all times
35
Invariants and Routine Execution
Execution of a.f (…)
begins by trying to work towards its postcond
destroys the invariant in the process
restores the invariant before termination
Obligation to maintain the invariant applies
only to the body of features exported;
not to a secret feature.
36
Invariant Rule
An assertion I is a correct class invariant for a class if and only if it meets:
E1: Every creation proc. yields a state satisfying I.
When applied to arguments satisfying its precond in a state where the attributes have their default values
E2: Every exported routine yields a state satisfying I
When applied to arguments and a state satisfying both I and the routine’s precondition.
37
Class Invariants and Contracting
Class invariant affects all the contracts between a routine and a client.
Implicit pre/post-cond of every exported routine (E2).
{INV && pre} body {INV && post}
If you implement the body, the invariant:
Makes your job easier - take this stronger precond for granted at the start of the routine;
Makes your job harder - ensure that the routine will satisfy the stronger postcond on termination
38
When Is a Class Correct?
If and only if its implementation is consistent with the preconds, postconds and invariant.
A class is correct w.r.t. its assertions iff:
For any valid arguments xp to creation procedure p:
{DefaultC && prep(xp)} Bodyp {postp (xp) && INV}
For every exported routine r and any valid args xr:
{prer (xr) && INV} Bodyr {postr (xr) && INV}
Role of creation procedures
They make sure that any instance of the class, when it starts its life, already satisfies the fundamental rules of its caste — the class invariant
39
The ADT Connection
A class is an implementation of an ADT
ADT: type, functions, axioms, preconds
Functions: creator, query, command.
Axioms, preconds: semantic properties of functions
ADT properties and class assertions
A precond of ADT function - precond for the routine
An axiom involving a command – postcond
Axioms involving only queries - postcond of function or invariant.
Axioms involving creators - postcond of creator
40
The ADT Connection - cont
Implementation invariants
Related to representation; meaningless in ADT
Assertions in invariant have no counterparts in ADT.
count_non_negative: 0 <= count
count_bounded: count <= capacity
Class interface is restricted to the features directly deduced from the ADT’s functions.
41
Loops
To reveal the bug, how many times should the be loop executed?
a = [1,2,3,4]
sum =0;
while (i>0) { /* i =0, 1, 2, 3…? */
i = i-1;
sum = a [i]; /*oops, should be +=*/
}
The wrong result is given only when the loop is executed more than once.
42
Loops - cont
Loop coverage for while (test) body requires:
The test be false on its first evaluation so the body is not executed
The test be true the first time, then false, so the loop body is executed exactly once
The test be true at least twice, forcing at least two executions of the loop
There are faults that can be detected only in one of these cases.
Coverage criteria: 0/1/n/Max…
Testing does not assure correctness!
43
Loop Invariants and Variants
Loop trouble
“Off-by-one” errors, performing one iteration too many or too few.
Improper handling of borderline cases
Infinite looping in some cases.
Getting loops right
loop invariant (assertions)
loop variant (an integer expression)
44
Loop Example: Maximum of an array
45
Loop Example - cont
maxarray (t: ARRAY [INTEGER]): INTEGER is
-- The highest of the values in the entries of t
require t.capacity >= 1
local i: INTEGER
do
from
i := t.lower
Result := t @ lower
until i = t.upper loop
i := i + 1
Result := Result.max (t @ i)
end // t @ i: the element at index i
end // a.max (b): max of {a, b}
46
Loop Example - cont
Loop invariant
at each stage through the loop Result is the maximum of the current approximation of the array.
Invariant maintenance
First, true after the initialization,
Then, on each iteration, extend the slice by one element, and update Result if the new value is higher than the previous maximum
At the end, the approximation covers the entire array
47
Ingredients for a provably correct loop
Postcondition or goal (post): a property that any satisfactory end state must satisfy.
Result is the maximum value in the array
Invariant (inv): a generalization of the goal
Result is the max in a non-empty array slice beginning at the lower bound
Initial point (init): satisfying inv
Transformation body: starting from a point in inv but not in post, yields a point closer to post and still in inv.
Upper bound on the number of applications of body necessary to bring a point in inv to post
48
Loop Variant
Termination is not difficult to prove for loops with finite interval (for, do),
For more sophisticated loops, the only universal technique is to find a variant.
A loop variant is an integer quantity such that
it is always non-negative.
any execution of body decreases the variant.
t.upper – i.
49
Using Assertions
Help in writing correct software
Spelling out the exact requirements on each routine, and the global properties of classes and loops
Documentation aid
Precond, postcond, and class invariants provide clients with concise/precise info about the services
Support for testing, debugging, fault tolerance
Need runtime monitoring of assertions
Assertion evaluation rule:
During the process of evaluating an assertion at runtime, routine calls used by the assertion shall be executed without evaluation of the associated assertions.
50
Exceptions – When Contract Is Broken
Success and Failure
A routine call succeeds if it terminates its execution in a state satisfying the routine’s contract.
It fails if it does not succeed.
Exception and Failure
Run-time event that may cause a routine call to fail
Every failure results from an exception, but not every exception results in failure
A failure of a routine causes an exception in its caller.
A routine call will fail iff an exception occurs and the routine does not recover from the exception.
51
Sources of Exceptions
Exception may occur during the exec of routine r:
Attempting call a.f and a is void.
Executing an operation that produces an abnormal condition detected by the hardware or OS.
Calling a routine that fails.
Finding r’s precond (postcond) doesn’t hold on entry (exit)
Finding that class invariant doesn’t hold on entry or exit.
Finding that the invariant of a loop is violated.
Finding that an iteration of a loop’s body does not decrease the variant.
Finding that its embedded assertion does not hold.
Executing an instruction meant explicitly to trigger an exception.
52
Disciplined Exception Handling Principle
Retrying
Hopeful strategy
“We have lost a battle, but we have not lost the war”
Battle: the current attempt at executing the routine body
War: the attempt to terminate the call so as to satisfy the contract
Attempt to change the conditions that lead to the exception and to exec the routine again from the start
If we succeed, the client will be entirely unaffected, and the contract is fulfilled.
Read an integer
53
53
Disciplined Exception Handling Principle
Failure (a.k.a. Organized Panic)
Give-up strategy
“Not only have lost the battle, but cannot win the war”
Clean up the environment, terminate the call and report failure to the caller.
Panic aspect
Making sure the caller gets an exception - the routine has failed to live up to its contract
Organized aspect
A routine execution may temporarily violate the invariant
Restoring a consistent execution state that satisfies the invariant.
sqrt
54
54
Call Chain
55
If a routine produces an exception, it may be necessary to go up the chain until finding a routine equipped to handle the exception, or stop execution if we reach r0