COMP2511
Design by Contract
Prepared by
Dr. Ashesh Mahidadia
Defensive Programming Vs Design by Contract
Defensive programming:
Tries to address unforeseen circumstances, in order to ensure the continuing functionality of the software
element. For example, it makes the software behave in a predictable manner despite unexpected inputs
or user actions.
• often used where high availability, safety or security is needed.
• results in redundant checks (both client and supplier may perform checks),
more complex software for maintenance.
• difficult to locate errors, considering there is no clear demarcation of responsibilities.
• may safeguard against errors that will never be encountered, thus incurring run-time and
maintenance costs.
Design by Contract:
At the design time, responsibilities are clearly assigned to different software elements, clearly
documented and enforced during the development using unit testing and/or language support.
• clear demarcation of responsibilities helps prevent redundant checks,
resulting in simpler code and easier maintenance.
• crashes if the required conditions are not satisfied! May not be suitable for high availability
applications.
COMP2511: Design By Contract 2
Design by Contract (DbC)
v Bertrand Meyer coined the term for his design of the Eiffel programming language (in 1986).
Design by Contract (DbC) has its roots in work on formal specification, formal verification and
Hoare logic.
v In business, when two parties (supplier and client) interact with each other, often they write and
sign contracts to clarify the obligations and expectations. For example,
COMP2511: Design By Contract 3
Obligations Benefits
Client (Must ensure precondition) (May benefit from post-condition)
Be at the Santa Barbara airport at
least 5 minutes before scheduled
departure time. Bring only
acceptable baggage. Pay ticket price.
Reach Chicago.
Supplier (Must ensure post-condition) (May assume pre-condition)
Bring customer to Chicago. No need to carry passenger who is late, has
unacceptable baggage, or has not paid ticket
price.
The example is from https://www.eiffel.com/values/design-by-contract/introduction/
Design by Contract (DbC)
Every software element should define a specification (or a contract) that governs its interaction
with the rest of the software components.
A contract should address the following three questions:
v Pre-condition – what does the contract expect?
If the precondition is true, it can avoid handling cases outside of the precondition.
For example, expected argument value (mark>=0) and (marks<=100).
v Post-condition - what does the contract guarantee?
Return value(s) is guaranteed, provided the precondition is true.
For example: correct return value representing a grade.
v Invariant - what does the contract maintain?
Some values must satisfy constraints, before and after the execution (say of the method).
For example: a value of mark remains between zero and 100.
COMP2511: Design By Contract 4
Design by Contract (DbC)
A contract (precondition, post-condition and invariant) should be,
v declarative and must not include implementation details.
v as far as possible: precise, formal and verifiable.
COMP2511: Design By Contract 5
Benefits of Design by Contract (DbC)
v Do not need to do error checking for conditions that not satisfy the preconditions!
v Prevents redundant validation tasks.
v Given the preconditions are satisfied, clients can expect the specified post-conditions.
v Responsibilities are clearly assigned, this helps in locating errors and resulting in easier
code maintenance.
v Helps in cleaner and faster development.
COMP2511: Design By Contract 6
Design by Contract (DbC) : Implementation Issues
v Some programming languages (like Eiffel) offer native support for DbC.
v Java does not have native support for DbC, there are various libraries to support DbC.
v In the absence of a native language support, unit testing is used to test the contracts
(preconditions, post-conditions and invariants).
v Often preconditions, post-conditions and invariants are included in the documentation.
v As indicated earlier, contracts should be,
• declarative and must not include implementation details.
• as far as possible: precise, formal and verifiable.
COMP2511: Design By Contract 7
Design by Contract : Example using Eiffel
COMP2511: Design By Contract 8
Precondition
Postcondition
invariant
Design by Contract: Examples in Java
COMP2511: Design By Contract 9
Pre-Conditions
v A pre-condition is a condition or predicate that must always be true just prior to the execution of
some section of code
v If a precondition is violated, the effect of the section of code becomes undefined and thus may
or may not carry out its intended work.
v Security problems can arise due to incorrect pre-conditions.
v Often, preconditions are included in the documentation of the affected section of code.
v Preconditions are sometimes tested using guards or assertions within the code itself, and some
languages have specific syntactic constructions for testing .
v In Design by Contract, a software element can assume that preconditions are satisfied,
resulting in removal of redundant error checking code.
v See the next slide for the examples.
COMP2511: Design By Contract 10
Pre-Conditions: Examples
COMP2511: Design By Contract 11
Design by Contract
No additional error checking for pre-conditions
Defensive Programming:
Additional error checking for pre-conditions
Throws runtime exception
if (i >= number_of_students)
Incorrect behaviour if mark
is outside the expected range
Pre-Conditions in Inheritance
v An implementation or redefinition (method overriding) of an inherited method
must comply with the inherited contract for the method.
v Preconditions may be weakened (relaxed) in a subclass, but it must comply with the inherited
contract.
v An implementation or redefinition may lessen the obligation of the client, but not increase it.
v For example,
COMP2511: Design By Contract 12
Weaker Pre-condition
X – not valid
Stronger Pre-condition
valid
Post-Conditions
v A post-condition is a condition or predicate that must always be true just after the execution of
some section of code
v The post-condition for any routine is a declaration of the properties which are guaranteed upon
completion of the routine’s execution[1] .
v Often, preconditions are included in the documentation of the affected section of code.
v Post-conditions are sometimes tested using guards or assertions within the code itself, and some
languages have specific syntactic constructions for testing .
v In Design by Contract, the properties declared by the post-condition(s) are assured, provided the
software element is called in a state in which its pre-condition(s) were true.
[1] Meyer, Bertrand, Object-Oriented Software Construction, second edition, Prentice Hall, 1997.
COMP2511: Design By Contract 13
Post-Conditions in Inheritance
v An implementation or redefinition (method overriding) of an inherited method
must comply with the inherited contract for the method.
v Post-conditions may be strengthened (more restricted) in a subclass, but it must comply with the
inherited contract.
v An implementation or redefinition (overridden method) may increase the benefits it provides to
the client, but not decrease it.
v For example,
v the original contract requires returning a set.
v the redefinition (overridden method) returns sorted set, offering more benefit to a client.
COMP2511: Design By Contract 14
Class Invariant
v The class invariant constrains the state (i.e. values of certain variables) stored in the object.
v Class invariants are established during construction and constantly maintained between calls to
public methods. Methods of the class must make sure that the class invariants are satisfied /
preserved.
v Within a method: code within a method may break invariants as long as the invariants are
restored before a public method ends.
v Class invariants help programmers to rely on a valid state, avoiding risk of inaccurate / invalid
data. Also helps in locating errors during testing.
Class invariants in Inheritance
v Class invariants are inherited, that means,
“the invariants of all the parents of a class apply to the class itself.” !
v A subclass can access implementation data of the parents, however, must always satisfy the
invariants of all the parents – preventing invalid states!
COMP2511: Design By Contract 15
End
COMP2511: Design By Contract 16