Re: LSL boolean combinations involving undefined terms

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

Follow-Up(s): Reference(s):