[PRL] Contracts vs aspects

[Paul A. Steckler]

>     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.

-- Paul