2. Design by Contract

Created Saturday 16 August 2014

Assertions

Preconditions

Postconditions and Invariants

Strength

Inheritance

Correctness

Preconditions

Things that have to be true before you call the method

Defensive programming (problematic)

Used to check for hidden preconditions (if ... else ... statements)
The caller should check preconditions before making a call!

Empty Preconditions

Prove Preconditions

Postcondition

Invariant

Contract

We can prove that the caller is correct by comparing the postconditions of one method call with the preconditions of the next. If the call is correct then you can infer the preconditions from those prior postconditions. You can create an inference chain from the postconditions through the various lines of code of the caller in order to infer the preconditions.

On the other side of the interface we can prove that the method is correct by examining its preconditions, its implementation and its postconditions and invariants. We should be able to start with the preconditions assuming them to be true and then proceed through the method implementation line by line. If that method is correct then you'll be able to infer the postconditions and invariants from the preconditions and the implementation.

A class can also use its own invariant as a part of the proof. Since we know that the class insures its invariant after every public method call we know that the invariants are always true before the next public method call, and so we often find the nessessary to use the invariant at the beginning of the method to prove that same invariant in the end of the method. It's useful to start with the class invariant, make a few changes within the body of the method that invalidate that invariant and then return it to the state where the invariant is true before you finish. The class invariant is not garanteed to be true at every point within the body of implementation, nor is it garanteed to be true before or after a private method call. Private methods aren't part of the public contract. An invariant only needs to be true between public method calls.

Invariant Application

Rules

Strength

Strength Defined

Anything Implies True



Backlinks: