COMP2511
Design by Contract
Prepared by
Dr. Ashesh Mahidadia
Design by Contract
These lecture notes use material from the Wikipedia page on this topic, the reference book “Head First Design Patterns”,
and the website at https://www.eiffel.com/values/design-by-contract/introduction/.
2COMP2511: Design By Contract
http://shop.oreilly.com/product/9780596007126.do
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 3
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 4
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 5
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 6
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 7
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 8
Design by Contract : Example using Eiffel
COMP2511: Design By Contract 9
Precondition
Postcondition
invariant
Design by Contract: Examples in Java
COMP2511: Design By Contract 10
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 11
Pre-Conditions: Examples
COMP2511: Design By Contract 12
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 13
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 14
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 15
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 16
Exceptions in Java
COMP2511: Design By Contract 17
Exceptions in Java
v An exception is an event, which occurs during the execution of a program, that disrupts the
normal flow of the program’s instructions.
v When error occurs, an exception object is created and given to the runtime system, this is called
throwing an exception.
v The runtime system searches the call stack for a method that contains a block of code that can
handle the exception.
v The exception handler chosen is said to catch the exception.
COMP2511: Design By Contract 18
The call stack. Searching the call stack for
the exception handler.
From the webpage at https://docs.oracle.com/javase/tutorial/essential/exceptions/definition.html
Exceptions in Java
The Three Kinds of Exceptions
v Checked exception (IOException, SQLException, etc.)
v Error (VirtualMachineError, OutOfMemoryError, etc.)
v Runtime exception (ArrayIndexOutOfBoundsExceptions, ArithmeticException, etc.)
Checked vs. Unchecked Exceptions
v An exception’s type determines whether it’s checked or unchecked.
v All classes that are subclasses of RuntimeException (typically caused by defects in your
program’s code) or Error (typically ‘system’ issues) are unchecked exceptions.
v All classes that inherit from class Exception but not directly or indirectly from class
RuntimeException are considered to be checked exceptions.
COMP2511: Design By Contract 19
Exceptions in Java
v Good introduction on Exceptions at
https://docs.oracle.com/javase/tutorial/essential/exceptions/index.html
v Unchecked Exceptions — The Controversy
https://docs.oracle.com/javase/tutorial/essential/exceptions/runtime.html
COMP2511: Design By Contract 20
https://docs.oracle.com/javase/tutorial/essential/exceptions/index.html
https://docs.oracle.com/javase/tutorial/essential/exceptions/runtime.html
Hierarchy of Java Exceptions
COMP2511: Design By Contract 21
From the book “Java How to Program, Early Objects”, 11th Edition,
by Paul J. Deitel; Harvey Deitel
Unchecked Exceptions
Checked Exceptions
Example
COMP2511: Design By Contract 22
From the example at https://docs.oracle.com/javase/tutorial/essential/exceptions/putItTogether.html
try
catch
finally
User Defined Exceptions in Java
v We can also create user defined exceptions.
v All exceptions must be a child of Throwable.
v A checked exception need to extend the Exception class,
but not directly or indirectly from class RuntimeException.
It will be enforced by the Handle or Declare Rule.
v An unchecked exception (like a runtime exception) need to extend the
RuntimeException class.
v Demo …
COMP2511: Design By Contract 23
User Defined / Custom Exceptions
• We can define our own exception classes! Often called as a user defined/custom
exception
• User defined exceptions can be either checked or unchecked exception.
• Normally we define a checked exception, by extending the Exception class.
COMP2511: Design By Contract 24
User Defined / Custom Exceptions: A Simple Example
COMP2511: Design By Contract 25
Exceptions in Inheritance
v If a subclass method overrides a superclass method,
a subclass’s throws clause can contain a subset of
a superclass’s throws clause.
It must not throw more exceptions!
v Exceptions are part of an API documentation and contract.
COMP2511: Design By Contract 26
Demo: Exceptions in Java
Demo …
COMP2511: Design By Contract 27
Assertions in Java
• An assertion is a statement in the Java that enables you to test your assumptions about your
program. Assertions are useful for checking:
• Preconditions, Post-conditions, and Class Invariants (DbC!)
• Internal Invariants and Control-Flow Invariants
• You should not use assertions:
• for argument checking in public methods.
• to do any work that your application requires for correct operation.
• Evaluating assertions should not result in side effects.
• The following document shows how to use assertions in Java :
https://docs.oracle.com/javase/8/docs/technotes/guides/language/assert.html
Important: for backward compatibility, by default, Java disables assertion validation feature.
It needs to be explicitly enabled using the following command line argument:
• -enableassertions command line argument, or
• -ea command line argument
COMP2511: Design By Contract 28
https://docs.oracle.com/javase/8/docs/technotes/guides/language/assert.html
Assert : Example
COMP2511: Design By Contract 29
Exceptions: Summary Points
v Consider your exception-handling and error-recovery strategy in the design process.
v Sometimes you can prevent an exception by validating data first.
v If an exception can be handled meaningfully in a method, the method should catch the
exception rather than declare it.
v If a subclass method overrides a superclass method, a subclass’s throws clause can contain a
subset of a superclass’s throws clause. It must not throw more exceptions!
v Programmers should handle checked exceptions.
v If unchecked exceptions are expected, you must handle them gracefully.
v Only the first matching catch is executed, so select your catching class(es) carefully.
v Exceptions are part of an API documentation and contract.
v Assertions can be used to check preconditions, post-conditions and invariants.
COMP2511: Design By Contract 30