Advanced Programming I Lecture Notes

19 April 2007 • Design by Contract

Outline

• Design by contract.

• Contracts

• Software contracts.

• Assertions, pre- and postconditions.

• Conditions and classes.

• Invariants and correctness.

• Inheritance

• Subcontracting

Design by Contract

• Developed in the early 90s by Bertran Meyer.

• Part of the computational model provided by the Eiffel programming language.

  • Other languages since has proveded more or less specific support for design by contract.

• Work on design by contract continues today.

Objectives

• Design by contract has three main objectives:

  1. A method for designing and building correct and robust software.

  2. A systematic approach for dealing with abnormal cases (exception handling).

  3. A concrete interpretation of inheritance and related techniques (redeclarations, polymorphism, and dynamic binding).

Contracts

• A contract is a legal agreement between two parties (to keep it simple).

• The two parties are distinguishable.

  • One party is the client (buyer, caller).

  • The other party is the supplier (seller, callee).

• "Legal" means there's an established framework within which contracts operate.

Contract Objectives

• By entering into a contract, each party expects

  • benefits that accrue to each.

  • obligations that must be fulfilled by each.

• The contract specifies the benefits and obligations on both parties.

• A contract is a specification.

Advantages

• A contract defines the relation between two parties.

• A contract provides protection for both parties.

  • The benefits are bounded from above.

    • Expect more more than what the contract specifies.

  • The obligations are bounded from below.

    • Provide no less than what the contract specifies.

Contract Coverage

• The contract covers all actions between two parties.

• Anything not covered is left open and unconstrained.

• This is the No Hidden Clauses principle.

  • It provides freedom for the implementers and designers.

  • It's abstraction in specifications.

Software Contracts

• Contracts in software are between caller (client) and callee (implementor).

• There are a number of ways of implementing contracts in software.

• The simplest, oldest, and most broadly supported is by using assertions.

The Stack Example

• Contract for stack::push():

  • The client

    • is obliged to call stk.push() when stk is not full,

    • and benefits by having x pushed into stk.

  • The class

    • is obliged to store x on the top of stk,

    • and benefits eliminating the fullness test for stk.

Assertions

• An assertion is a predicate over a computation's variables.

  i < n ∧ a[i] ≠ x
  

• An assertion makes a statement about a desirable state of the computation.

Assertion Values

• As a predicate, an assertion is either true or false.

  • A true assertion is satisfied.

  • A false assertion is violated.

• A satisfied assertion usually does nothing.

• A violated assertion does something drastic.

  • What in particular depends on the assertion support.

Assertion Support

• All languages support boolean expressions.

• Some languages support assertions explicitly.

  • Java has the assert statement.

    • Violated exceptions throw an exception.

  • C and C++ have the assert macro.

    • Violated exceptions core dump.

• And you can always roll your own.

Assertions in Contracts

• For the moment, think of procedures.

  • The caller is the client.

  • The procedure (callee) is the supplier.

• A contract between a caller and a procedure takes the form of preconditions and postconditions.

Preconditions

• A precondition specifies the caller's obligations and the procedure's benefits.

• A precondition is a predicate over the procedure's parameters.

• The caller is obligated to pass values that satisfy the precondition.

  • Failure to do so violates the precondition.

• The procedure receives the benefit of knowing the parameter values are legitimate.

Postconditions

• A postcondition specifies the procedure's obligations and the caller's benefits.

• A postcondition is a predicate over the procedure's out parameters and the return value (if any).

• The procedure is obligated satisfy the precondition.

  • Failure to do so violates the postcondition.

• The caller receives the benefit of knowing the parameter values are legitimate.

Example

• Take our old pal the sort routine.

  sort(T a[], int n)
  
    pre: n > -1
  
    post: for all 0  i  j < n : a[i] < a[j] 
  

• This is not a complete postcondition.

Violating Conditions

• What happens when a pre- or postcondition fails?

  • This is a special case; conditions should always be satisfied.

• Violated conditions should be considered errors.

  • Violated preconditions are caller errors.

  • Violated postconditions are procedure errors.

Checking Conditions

• Should the caller or the procedure check preconditions?

  • Meyers argues for the caller.

  • Guaranteeing a precondition is not the same as checking for it.

• The alternative is to check in the procedure.

  • Meyer argues this indicates poor interface or procedure design.

Conditions and Classes

• Adding pre- and postconditions to classes requires a bit of work.

• Methods are similar to procedures, and follow procedures in their use of conditions.

• Classes also have instance variables, which are similar to global variables.

• Method conditions should not refer to instance variables.

• What makes sure class instances are in good shape?

Class Invariants

• A class invariant is a predicate over the instance variables of a class instance.

  • The class invariant specifies a sane state for an instance.

  • The instance can meet its contracutal obligations.

• An invariant is a global property of instances preserved by all non-private methods.

  • The class invariant is almost always true.

Example Invariant

• Assume an array-based stack ADT

  class stack
    private:
  
      T data[max]
      unsigned top
  
      // Invariant:
      //   0 < max
      //   0 ≤ top ∧ top ≤ max
      //   0 < top → head ≡ data[top - 1]
  
  

Invariant Scope

• Class instance I's invariant must be true:

  • Immediately after I's construction.

  • Before every call to any of I's non-private methods.

  • After returning from a non-private method call.

• These are an instance's observable states.

  • The invariant's always observed to be true.

Example Observations

The invariant starts out true. Each non-private method leaves it true. What happens during a method call?

Invariant Visibility

• Class invariants apply only to non-private methods.

  • Private methods are not required to maintain the invariant.

• Protected methods are considered public.

  • Inheritance makes the relation is a bit more complicated than that.

Invariant Exemptions

• Why don't private methods need to maintain the class invariant?

• What happens to the class invariant during a non-private method call?

Exemption Example

• Let a sorted-array ADT have the invariant sorted(data).

• add(x) uses insertion to add x to data.

  add(x)
    data[end++] = x
    for (i = end - 1, i > 0, i--)
      if data[i - 1] ≤ data[i] break
      swap(data[i - 1], data[i])
  

• The first assignment may violate the invariant.

• The for-loop restores it.

Class State

• A method's precondition may involve initial state and the arguments.

• A method's postcondition may only involve the final state, the initial state and the returned value, if any.

• The class invariant may only involve the instance variables.

Invariant Rule

• The class invariant is implicitly added to both the precondition and postconditions of every public method.

• Could do, in principle, without class invariants, but they give valuable information.

• Class invariants act as control on evolution of class.

• A class invariant applies to all contracts between a method of the class and a client.

Definitions

• Class C.

• INV class invariant.

• Method r: pre_r(x_r) precondition; post_r(x_r) postcondition;

• x_r: possible arguments of r.

• B_r: body of method r.

• Default_C: attributes have the default values.

Class Correctness

• A class C is correct with respect to its assertions iff

  • Every public method r other than the constructor and any set of valid argument x_r:

    { INV ∧ pre_r(x_r) } B_r { INV ∧ post_r(x_r) }

  • For any valid set of arguments x_C to the constructor:

    { Default_C ∧ pre_C(x_C) } B_C { INV }

Proving Correctness

• A complex story.

• Reason about imperative sequential programs such as Java programs.

• Imperative programs

  • define a state space

  • actions operating in the state space.

Inheritance

• Inheritance defines new classes from old ones.

• The new class may redeclare features in the old classes.

• Redeclaring features leads to subtype polymorphism via dynamic binding.

• Inheritance also introduces the question of what to do with with conditions in the parent classes.

Subcontracting

• The redeclared feature has its own conditions.

  • What is the relation between the new and old conditions?

• Subcontracts specify the relation between old and new features.

Subcontracts

• A new feature may require less from the caller than the old feature.

  • The new feature's precondition may weaken the old features precondition.

• A new feature may do more work than the old feature.

  • The new feature's postcondition may strengthen the old features postcondition.

References

• Applying "Design by Contract" by Bertrand Meyer, IEEE Computer, October 1992.

• A Practical Approach to Programming with Assertions by David Rosenblum, IEEE Transactions in Software Engineering, January, 1995.