Re: LSL boolean combinations involving undefined terms

• Subject: Re: LSL boolean combinations involving undefined terms
• From: leavens@cs.iastate.edu (Gary Leavens)
• Date: 20 Jul 95 20:17:51 GMT
• Keywords: undefined, lazy evaluation
• Newsgroups: comp.specification.larch
• Organization: Iowa State University, Ames, Iowa
• References: <leavens.805997000@bambam.cs.iastate.edu> <leavens.806079418@bambam.cs.iastate.edu> <3uiv5j$n60@newsflash.concordia.ca>

I think Jim and Patrice, and also Kiyotaka Kuroda at CMU,
who sent me email about this.  Kiyotaka Kuroda also went to
the trouble of doing the proof in LP, which bears out the
assertions of Jim and Patrice.

Patrice and I, along with Dave Evans, have been carrying on
an extended discussion about the semantics of "trashed"
and the modifies clause in interface specifications.
(This has been making me think more closely about the logical
foundations of LSL.  So I was doubting everything for a while.)
We'll share the resolution of that issue
with you all at some later date, I hope.
In the meantime, it's off the the library to read Cliff Jones's note...

	Gary Leavens
--
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/homepage.html

• Re: LSL boolean combinations involving undefined terms
• From: leavens@cs.iastate.edu (Gary Leavens)

• LSL boolean combinations involving undefined terms
• From: leavens@cs.iastate.edu (Gary Leavens)
• Re: LSL boolean combinations involving undefined terms
• From: leavens@cs.iastate.edu (Gary Leavens)
• Re: LSL boolean combinations involving undefined terms
• From: chalin@cs.concordia.ca (CHALIN patrice)

• Prev: Re: LSL boolean combinations involving undefined terms
• Next: Re: Step-by-step instructions to formal specification of a class needed!!
• Index: Larch archive index