Re: specification of destructive operation


I think that you're correct that this notion of reified states in Larch
interface languages is right at the research frontier, and mostly

It is distinctly non-trivial to get the details right so that proofs that
ought to be done at the abstract level are possible and sound.  Greg Nelson
and Dave Detlefs here at SRC have been fighting their way through this for
their Extended Static Checking system for Modula-3.  Again, not-yet-
published work.

Jim H.