Software Design and Implementation Principles

Software Design and Implementation: Composition and Substitution Dror Feitelson Hebrew University

Composition Software systems are composed of multiple modules Modules are built and tested in isolation Should be enough because modules are defined by their interface But still may not work correctly when composed together (that s why we need integration testing)

Agenda Preconditions and postconditions Defining the interface Contracts Integrating with the programming language Liskov substitution principle When can a subclass be used in place of a superclass

C. A. R. Hoare, An Axiomatic Basis for Computer Programming . Comm. ACM 12(10) pp. 576-580,583, Oct 1969. Inventor of Quicksort (at age 26) Inventor of switch/case construct Took responsibility for null references Inventor of Hoare Logic (this paper) Inventor of formalisms like CSP Recipient of 1980 Turing Award (and many other awards)

What does this code do? r := x q := 0 while (r >= y) do r := r y q := q + 1 done And how can we express this?

Hoare Triplet {P} S {Q} P and Q are predicates P is the precondition S is a statement Q is the postcondition Semantics: if P holds before you execute S, then Q will hold after you execute it

{what is the precondition?} r := x q := 0 while (r >= y) do r := r y q := q + 1 done {what is the postcondition?}

{x >= 0 y > 0} r := x q := 0 while (r >= y) do r := r y q := q + 1 done { (y <= r) x = q y+r}

Axioms Rule of consequence: If {P0} S {Q0} and P P0 and Q0 Q Then {P} S {Q}

Axioms Rule of composition: If {P} S1 {R} and {R} S2 {Q} Then {P} S1; S2 {Q}

Axioms Rule of iteration: If {P B} S{P} Then {P} while(B) do S done { B P} P is loop invariant B is loop condition

Axioms Rule of conditional: If {P B} S{Q} and {P B} T{Q} Then {P} if(B) then S else T end{Q}

Axioms Axiom of assignment: Denote by P[E/x] the predicate P with free instances of variable x replaced by expression E Then {P[E/x]} x := E {P} Not the other way around! P will hold after the assignment if it would have held before the assignment had the assignment been made

Bertrand Meyer, Applying Design by Contract . Computer25(10) pp. 40-51, Oct 1992. Famous for: Advocacy and teaching of object-oriented programming Eiffel programming language and IDE Design by contract Prof. at ETH Zurich Recipient of ACM Software Systems Award

The problem: Coordinate between the two sides of an interface Who is responsible for what? Solution 1: Defensive programming Assume the other side is stupid and irresponsible Solution 2: Contracts

Contracts Supplier What supplier will do Client What client must conform to What client may expect to get Obligations What supplier does not have to worry about Benefits

Contracts Supplier What supplier will do Client What client must conform to What client may expect to get Obligations What supplier does not have to worry about Benefits

Contracts preconditions Supplier What supplier will do Client What client must conform to What client may expect to get Obligations What supplier does not have to worry about Benefits postconditions

Indexing description: "Simple bank accounts" class ACCOUNT feature -- Access balance: INTEGER -- Current balance deposit_count: INTEGER is -- Number of deposits made since opening do if all_deposits /= Void then Result := all_deposits.count end end Automatic documentation Public member Default initial value is 0

feature -- Element change deposit (sum: INTEGER) is -- Add sum to account. require non_negative: sum >= 0 do if all_deposits = Void then create all_deposits end all_deposits.extend (sum) balance := balance + sum ensure one_more_deposit: deposit_count = old deposit_count + 1 updated: balance = old balance + sum end Pre-condition Optional label used in error messages Post-condition

Private member (seen by no other class) feature {NONE} -- Implementation all_deposits: DEPOSIT_LIST -- List of deposits since account s opening. invariant consistent_balance: (all_deposits /= Void) implies (balance = all_deposits.total) zero_if_no_deposits: (all_deposits = Void) implies (balance = 0) end -- class ACCOUNT Class invariant Holds before and after every call to every function

Invariants A general property of the class Expressed as a predicate describing the state of objects of this class Always true Holds after the constructor Holds before and after each method call Not necessarily during method execution Effective precondition is precondition AND invariant Effective postcondition is postcondition AND invariant

Advantages Better methodology Think clearly and express your assumptions Documentation The contract is part of the interface This is all the client needs to know Runtime verification by the system Debugging (identify bugs early) During production execution

Potential Disadvantage Supplier x function f has precondition p All clients will replicate the calling code if p then x.f else But: p may be known already from context (postcondition of previous operation) else may be different in different clients (e.g. what to do if popping from an empty stack)

Inheritance Class SUB inherits from class SUPER SUB may have a weaker precondition SUPER.pre SUB.pre If caller satisfies SUPER, will also work with SUB SUB may have a stronger postcondition SUB.post SUPER.post What SUB does is good enough for callers of SUPER SUB may also have stronger invariant Part of the Liskov Substitution Principle

Violations Contracts do not check for special conditions A runtime assertion violation is the manifestation of a bug Precondition: bug in client Postcondition or invariant: bug in supplier

Verification Client is responsible for precondition Supplier is responsible for postcondition System can check this Contract is part of the language Supplier can ignore bad input Simpler code Safe Client can assume result is correct If not there should have been an exception

Verification Options None If program is correct, why waste time on checks? Preconditions only (default) Useful for libraries with unknown clients Preconditions and postconditions Preconditions, postconditions, and invariants All (development and debugging): the above plus Loop invariants Loop variants (monotonically decreasing positive value to ensure termination) Assertions

Verification Options None If program is correct, why waste time on checks? Preconditions only (default) Useful for libraries with unknown clients Preconditions and Postconditions Preconditions, Postconditions, and invariants All (development and debugging): the above plus Loop invariants Loop variants (monotonically decreasing positive value to ensure termination) Assertions

Exceptions Violating a monitored assertion causes an exception An exception may cause a failure But you can sometimes avoid this! Catch exception Change something in conditions Retry

connect_to_server (server: SOCKET) -- Connect to a server or give up after 10 attempts require server /= Void and then server.address /= Void local attempts: INTEGER do server.connect ensure connected: server.is_connected rescue ifattempts < 10 then attempts := attempts + 1 retry end end

Examples r = sqrt( x ) l = log( x )

Examples { x 0 } r = sqrt( x ) { x = r } Precondition is an algorithmic necessity { x > 0 } l = log( x ) { el = x }

Examples account.deposit( s )

Examples Precondition reflects logic and semantics: if s < 0 it is a withdrawal { s > 0 } account.deposit( s ) { balance = old balance + s }

Examples account.withdraw( s )

Examples Precondition reflects design decision: does this function deal with attempted overdraft or does it just handle the technicalities? { s balance} account.withdraw( s ) { balance = old balance - s }

B. H. Liskov and J. M. Wing, "A behavioral notion of subtyping". ACM Trans. Programing Languages and Systems16(6) pp. 1811 1841, Nov 1994 Famous for: Contributions to programming languages and distributed computing Liskov Substitution Principle (this paper) Recipient of IEEE John von Neumann Medal (2004) Recipient of Turing Award (2008)

Substitution If S is a subtype of T then objects of type S may be used in place of objects of type T without affecting correctness

Polymorphism abstract class Animal { abstract String sound(); } class Cat extends Animal { String sound() { return "Meow!"; } } class Dog extends Animal { String sound() { return "Woof!"; } } Vector<Animal> macdonalds = new ; for (Animal farmAnimal : macdonalds) { farmAnimal.sound(); }

Problem Example Inheritance embodies the ISA relationship A square is a special case of a rectangle So it seems natural to use inheritance Rectangle Square

Problem Example But a rectangle has separate width and height And they can be changed independently While in a square setting one changes the other So a square does not behave like a rectangle Rectangle int: width int: height setWidth() setHeight() Square

Boolean checkArea(Rectangle r) { r.setWidth(4); r.setHeight(5); return (r.getWidth()*r.getHeight() == 20); }

An Idea Square can do the following: Override setWidth() and setHeight() to return an exception Include a new method setSide() Is this a good solution?

Formal Statement of LSP If x is of type T and P(x) and S is a subtype of T and y is of type S then P(y) // property P holds for x // property P also holds for y

Requirements Method signatures should be compatible Contracts and invariants should be compatible Exceptions should be compatible Behavior should be indistinguishable When using the subtype via the supertype interface Subtype may add only things that are invisible via the supertype interface

Syntactic Constraints

Method Signatures Return type of a method in a subtype can be more specific returning a Dog instead of an Animal is OK Argument types of a method in a subtype can be more general accepting any Animal instead of just a Cat is OK

Example AnimalShelter What happens if we substitute a DogShelter for an AnimalShelter? Void: accept(Animal) Animal: adopt() DogShelter Void: accept(Dog) Dog: adopt()