[Grace-core] Another inheritance/initialisation example - invariants

[James Noble]

Here's another use-case for inheritance:
supporting method pre/post conditions, and then class invariants. 

The basic scheme is taken from Scala, see "Contracts for Scala"
by Martin Odersky in  RV 2010 & a little from .Net code contracts.

The difficult bit is class invariants.  We can use either annotations
or method calls in bodies to set up invariants.  Something like this
(showing both options)

class BankAccount
 is invariant {balance >= 0 }  // invariant as annotation
{
 var balance := 0 
 invariant {balance >= 0} // OR as a method call in the body
}

where "invariant" takes a block, stores in in a list, and then 
say when a method runs, evaluates the block to ensure
the invariant is maintained. 

The catch is that these calls take blocks, and those blocks
will need to be bound to the right objects.   This will all
be fine if the inheritance semantics is classical - so that
the superclass/object annotations or body code is run
in the same "self" as the ultimate whole-object. 

But with delegation semantics, the blocks will be bound
to the "self" that holds only the "superclass" portion of the object;
with concatenation+copy the blocks will be bound to part-objects
that are unrelated to the actual whole-objects.   I can't see easy
ways to make this work, unless we start allowing blocks (not
closures but the block objects) to be cloned and somehow
*rebound* to different objects.  So when cloning an object
with invariants, we'd have to clone its blocks and reattach
them to the clone.  This all seems rather hard to me - 
but if there are designs that can make this work with nonclassical
semantics, I'd love to hear them. 

James 

PS: Method Pre & Post conditions can also be represented either by annotations:

> method foo (x) is 
>   requires { x > 0 }
>   ensures { balance == balance + x } 
>      { balance := balance + x } 

or keywords in method bodies:

> method foo (x) { 
>   requires { x > 0 }
>   ensures { balance == balance + x } 
>   
>   balance := balance + x
> }

note that if they are to be annotations, method arguments must be in scope 
of annotations on that method.  There's actually another option with annotations
something like this, giving us refined types

> method foo (x : Number is refined {x-> x <0} ) ... // rest as above 

ensure and require can be implemented quite easy as methods taking a block
returning a boolean that throw an exception or something if the block evalutes
to false. 

J