[e-lang] What is defensive consistency?

[Toby Murray]

On Fri, 2007-11-02 at 16:53 +0000, Karp, Alan H wrote:
> Toby Murray wrote:
> > 
> > Assuming that the only means a caller has of violating the 
> > preconditions
> > are in the arguments it passes with the invocation, which I believe is
> > guaranteed by the ocap model, then ensuring defensive 
> > consistency relies
> > upon checking only the arguments passed with the invocation. When
> > invoked, the object has all of the information it needs to maintain
> > defensive consistency. Hence, I do not see how maintaining defensive
> > consistency for individual method calls is difficult.
> > 
> The problem I see with that approach is identifying all the possible
> preconditions that need testing.

Indeed. 

>   There may well be a particular
> sequence of operations that leads to an incorrect result even though
> each individual operation is valid.  Consider an incrementer that
> guarantees to return a positive sum.  Alice makes a call that increments
> the state to the largest integer value.  Bob adds one and gets a bad
> result.  Neither one violated the contract.  The answer here is to use
> infinite precision arithmetic, but you get my point.

Absolutely. However, I'd argue that, in this case, either the
incrementer has violated one of its internal invariants, or it has
violated its contract. There is no precondition violation occurring
here. 

Suppose we have an objec Incrementer.

object Incrementer {
   // internal invariant: n >= 0
   private int n = 0;

   // precondition: n = c  [ where is some constant ]
   // postcondition: n = c + 1
   method int incr(void)
}

The precondition (n = c) is just a means of capturing the current value
of n in a constant, c, for use in the postcondition and is always
satisfied, no matter the value of n.

A call to incr() when n = INT_MAX that causes rollover of n violates not
only the invariant n >= 0 (presuming n is signed as is the case with
Java integers right?) but also the method's postcondition (n = c + 1,
where c holds the original value of n before the call). Hence, the
object has violated its own contract, since its precondition was met.

++++++++++++++