Eiffel Language and Design by Contract Contract –An agreement between the client and the supplier Characteristics –Expects some benefits and is prepared.

1 Eiffel Language and Design by Contract Contract –An agr...
Author: Earl Dorsey
0 downloads 8 Views

1 Eiffel Language and Design by Contract Contract –An agreement between the client and the supplier Characteristics –Expects some benefits and is prepared to incur some obligations –Documented in a contract document Eiffel –A language that implements the Design by Contract principles by Bertrand Meyer –Applying Design by Contract, B. Meyer, IEEE Computer, pp. 40-51, October 1992.

2 Design by Contract and Module Design Design by contract promotes using pre and post-conditions (such as assertions) in a module design Eiffel is an object oriented programming language that supports design by contract –In Eiffel the pre and post-conditions are written using require and ensure constructs, respectively Pre and post condition of a procedure between the caller and the callee Pre and post condition of a procedure between the caller and the callee Obligations and benefits of a contract between the client and the supplier Obligations and benefits of a contract between the client and the supplier

3 Eiffel Example -- A typical Eiffel procedure: procedure_name(argument declarations) is -- Header comment require Precondition do Procedure body ensure Postcondition End -- A typical Eiffel procedure: procedure_name(argument declarations) is -- Header comment require Precondition do Procedure body ensure Postcondition End -- An example: put_child(new_child: NODE) is -- Add new to the children -- of current node require new_child /= Void do... Insertion algorithm... ensure new_child.parent = Current; child_count = old child_count + 1 end -- put_child -- An example: put_child(new_child: NODE) is -- Add new to the children -- of current node require new_child /= Void do... Insertion algorithm... ensure new_child.parent = Current; child_count = old child_count + 1 end -- put_child

4 Contracts The pre and postconditions are assertions –Evaluate to true or false –Precondition Requirements that any call must satisfy –Postcondition Properties that are ensured at the end of the procedure execution The precondition or postcondition is assumed to be true

5 Assertion Violations The assertions can be checked dynamically at run- time as an approach to debugging the software Precondition Violation Precondition Violation Caller Bug Postcondition Violation Postcondition Violation Callee Bug

6 Defensive Programming vs. Design by Contract Defensive Programming –An approach that promotes putting checks in every module to detect unexpected situations –This results in redundant checks –A lot of checks makes the software more complex and harder to maintain In Design by Contract the responsibility assignment is clear and it is part of the module interface

7 Class Invariants An assertion that holds for all instances of the class –A class invariant must be satisfied after creation of every instance of the class –The invariant holds at the method entry it should hold at the method exit –conjunction added to the precondition and postcondition of each method in the class Example: A class invariant for a binary tree invariant left /= Void implies (left.parent = Current) right /=Void implies (right.parent = Current) Example: A class invariant for a binary tree invariant left /= Void implies (left.parent = Current) right /=Void implies (right.parent = Current)

8 Inheritance ClassA aMethod() ClassB Client aMethod() What happens to pre and postconditions in inheritance? By definition we enforce (1) The precondition of a derived method to be weaker (2) The postcondition of a derived method to be stronger