Re: specification of destructive operation

• To: leavens@cs.iastate.edu (Gary Leavens)
• Subject: Re: specification of destructive operation
• From: horning
• Date: Fri, 13 Jan 95 11:00:37 -0800
• Cc: pys@info.fundp.ac.be, larch-interest@src.dec.com
• Delivery-Date: Fri, 13 Jan 95 11:12:09 -0800
• In-Reply-To: Message of Fri, 13 Jan 95 10:02:04 CST from leavens@cs.iastate.edu (Gary Leavens)

Gary,

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

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.

• Prev: Is there a way of better managing larch-interest?
• Next: Re: specification of destructive operation
• Index: Larch archive index