[cap-talk] Haskell @inert-like construct

[Toby Murray]

On Wed, 2008-09-03 at 09:02 -0700, Tyler Close wrote:
> The purpose of the @inert annotation is to
> declare to the Joe-E verifier that no mutable state will be read or
> written via a particular variable. The proposed rules for the @inert
> annotation enforce this constraint. So, going back to the declaration
> of the encode() method, the @inert annotation colloquially says:
> "Although we're passing in a reference to some mutable state, the
> implementation won't touch it".


Thanks heaps for the clarification Tyler. I'm beginning to understand
this @inert thing. It looks to have great potential for helping one
reason about Joe-E code.

Cheers again

Toby