ICS 121: Design by Contract

Overview

What is design by contract?
Why use design by contract?
Types of assertions
Examples

What is Design by Contract?

Design by Contract (DBC) is a simple design technique that helps components integrate more precisely by specifying the semantics of classes and operations with logical condition.
Before DBC:
- Your method may call my method (e.g., a square root function) by passing the right types of arguments.
- The programming language itself has no way to limit this to just the values that will actually work. E.g., only positive integers.
Some languages, e.g., Ada and Eiffel, allow subtypes, e.g., 0..10000. Subtypes make the language more complex and are not available in currently popular languages. Subtypes can only express some constraints on arguments. E.g., there is no good way to specify that my method only works with odd integers.
Example: in June 1996, an Ariane 5 rocket crashed 40 seconds after take-off at a cost of $500,000,000. The cause of the error was an integer out of bounds in a conversion function. This happened despite very rigorous development and testing processes.
With DBC:
- Each of my methods has a pre-condition and a post-condition. These are logical conditions that can be checked during testing or even mathematically proven in many cases.
- Your code must pass arguments that satisfy my pre-conditions. My code will always return results that satisfy my post-conditions.
Example: With DBC, the code that called the conversion function could have been flagged as passing values in a range that exceeded the range allowed in the function's precondition. Additional case analysis logic could have been implemented in the calling function, and that failure would not have occured.
In addition to pre- and post- conditions on operations, DBC can also include class invariants.

What is Design by Contract?

The process of thinking through these conditions helps clarify your own thinking. Many errors will be caught during writing, before the code is ever run.
DBC conditions help to document your code in a way that is more precise and concise than English.
DBC conditions are easy to add incrementally: you can add just a few and get some benefits immediately
DBC conditions are built-in tests that catch failures early in the testing process.
DBC conditions help to localize the failure during a program run, and provide more specific information for debugging.
DBC is conceptually simple and fairly widely used in industry (at least assert-statements for preconditions)

Types of Assertions

Pre-conditions:
- Checks that arguments to this operation reasonable. The check can be anything, not just subtypes.
- ONLY checks values, does not modify anything
- Can be implemented by an assert-statement, or an if-statement
- Condition can reference: arguments, state of the object
- When a method is overridden in a subclass, it should keep the same pre-condition, or make that condition weaker (make it accept more argument values).
Post-conditions:
- Checks the result of a method before it is passed back to
- ONLY checks results, does not modify anything
- Can be implemented by an assert-statement, or an if-statement
- Condition can reference: results, arguments, state of object after operation, copy of state of object before operation.
- When a method is overridden in a subclass, it should keep the same post-condition, or make that condition stronger (make it promise even better results).
Class invariants:
- Checks that the attributes of a class always have valid values.
- ONLY checks results, does not modify anything
- Can be implemented by a method with several assert-statements or if-statements. This method is called from other methods that do actual modifications.
- Condition can reference: state of the object
- Subclasses should keep the same class invariant or make it stronger
Loop invariants:
- Checks that a for-loop or while-loop is making progress
- ONLY checks results, does not modify anything
- Condtion can reference loop variable, arguments, state of object
- E.g., in the outer loop of bubble-sort, the array elements 0..i are sorted
DBC conditions may be checked at run-time or disabled. When disabled, they do not slow down the program at all. Now that CPUs are faster, it is more reasonable to leave most conditions enabled even when the product is shipped.

Examples

public float sqrt(float f)
- We only handle square roots of non-negative numbers
- Pre: f >= 0.0
- The result can be squared to get back to f, approximately
- Post: Math.abs((result * result) - f) < 0.001
public void enroll(Course c)
- Must be a valid course that I am not already enrolled in
- Pre: c != NULL && !myCourses.contains(c)
- After enrollment, I have one more course
- Post: (myCourses.size() == myCourses@pre.size() + 1)
- More precisely: After enrollment, I have all my old course and the new one
- Post: (myCourses.containsAll(myCourses@pre) && myCourses.contains(c))
public class Student
- Students never go above 188 units
- Inv: transcript.totalUnits() <= 188
- GPA is always between 0.0 and 4.0
- Inv: 0.0 <= gpa && gpa <= 4.0
- Students cannot retake a course that they passed
- Inv: forEach c in myCourses: (!transcript.contains(c) || transcript.getGrade(c) < 'C')
Assert-statement in Java 1.4:
- assert condition : optional-error-message;
- E.g., assert i >=0 : "got negative i: " + i;
- Must compile with 'javac -source 1.4' to allow this syntax
- See documentation
- We will cover assertions in more detail in week 7