Method Contracts, Hand-Coded 
----------------------------------------

There are two kinds of such conditions: 

 - preconditions: a condition that must be true *as* the method is
                  called typically, these conditions involve the
                  state of the object and the values of the
                  parameters

 - postconditions: a condition that must *after* the method's
                   computation is completed; typically, these
                   conditions involve the state of the object and
                   the *result* of the method.

In our example, the pre- and postconditions completely specify the
behavior of the method. Let's look at an implementation:

Directory

Here checking the postcondition is more expensive than computing
the result. So in general programmers don't turn all preconditions
and all postconditions from the purpose statement into
assertions. Instead, they just compute quick-and-cheap checks to
make sure the computation is on track.

Differently: the precondition checks that it is okay to call the
 method now and the postcondition checks that the method did its
 job. Method contracts are additional insurance (lightweight error
 checks).

Here is a canonical example: Stack. 

We could turn these purpose statements again into pre- and
postconditions that check *everything* about the stack's methods
(their *total* behavior). But, what really matters are the two
conditions in the purpose statements for top and pop. Let's turn
them into preconditions for an implementation of IStack:

Directory

Since we have a postcondition in push that says that the stack is
no longer empty when push returns, we can compose methods like
that:

 IStack s = new Stack(); 
 
 ...
 ... s.push(1).pop(); 
 ... 


Who benefits? 

Q: Who wants preconditions enforced and who wants postconditions
enforced?

A: The consumer of the class/component wants postconditions
enforced, the producer wants preconditions enforced.

Since neither has supremacy, we should check both. It is a basic
defense against errors and helps us think about the code as we go
from specification to programming.

Remarks: 

 - The above are simple checks. Most of them are obviously
   satisfied.  Don't let that deceive you.

 - If you work with inheritance, things get really tricky. 

 - What really matters is that you can pinpoint blame easily. 

 - We need languages where programmers can specify these things at
   the interface properly, where programmers can attach interfaces
   to objects as needed, and the language takes care of generating
   the pre and post methods and blaming the classes that break
   contracts.

 - In progress. 

Sequence Contracts
----------------------------------------

In addition to types (signatures) and basic conditions about the
before and after state of the world, we often also want to ensure
that methods are called in the proper order.

Take a look at this simple integer file interface: 

 IPort

Presumably, we create an IPort with a name and then work with it: 

 PortTest

 IPort ip = new IntegerPort("mydata"); 
 ... 

 ip.open();
 while (!ip.out_of_intsP())
   sum += ip.read(); 
 ip.close(); 

Clearly, the intention is that consumers call the methods of IPort
in a particular sequence, namely,

 one call to open
 followed by calls to read and out_of_intsP
 followed by one (optional) call to close

We call this a sequence contract and write something like the
above as

 open x { read | out_of_intsP }* x close

The braces group things.
The brackets make things optional. 
a x b means a followed by b. 
a | b means a or b. 
a* means 0 or more actions a. 
a+ means 1 or more actions a. 

 Port


Sequence Contracts via State Pattern
----------------------------------------

Here we clearly have a finite state machine: 

  port :

                open()	                          read(), 
       +------------------------------------+     out_of_intsP()
       |                                    |   +---------+
       |                                    v   |         |
 +------------+                          +----------+     |
 | ClosedPort |                          | OpenPort |     |
 +------------+                          +----------+     |
       ^                                    |   ^         |
       |                                    |   |         |       
       +------------------------------------+   +---------+
                close()

let's implement it as such: state pattern, have them look up the
pattern in the book.

 PortState