[PRL] Contracts vs aspects

[Carl Eastlund]

On 4/28/05, Paul A. Steckler <steck at stecksoft.com> wrote:
> >     Every call to bar() within an action must be preceded by at least
> >     one call to foo(). After any call to bar(), foo() must be called
> >     at least once before bar() can be called again.
> >
> > What would a contract for this look like?
> 
> An aspect?
> 
> Unless the arguments passed to bar provide
> unambiguous evidence of the preceding call
> to foo, I don't see how this notion is
> contract-expressible.

I don't know if you have a specific theoretical model of contracts in
mind, but I could certainly write this in PLT contracts.  Contracts
can contain arbitrary predicates, so they can also use and maintain
mutable state recording whether foo has been called since the last
call to bar.  This is before even considering adding new contract
primitives for this kind of invariant.

--Carl