Re: Larch "oversight"

• To: davidg@oracorp.com
• Subject: Re: Larch "oversight"
• From: "Stephen J. Garland" <garland@larch.lcs.mit.edu>
• Date: Wed, 06 Dec 95 11:15:42 -0500
• Cc: garland@larch.lcs.mit.edu, (John Guttag) guttag@larch.lcs.mit.edu, horning@pa.dec.com
• Delivery-Date: Wed, 06 Dec 95 08:23:05 -0800
• In-Reply-To: Your message of "Wed, 29 Nov 95 11:28:34 EST." <9511291628.AA00930@goedel.oracorp.com>

David,

     I do recall seeing your short note to comp.spec.larch.  In fact, I
actually saved a copy.  I apologize for not responding to it at the time.
In my reading, your trait

   AtMostTwo: trait
     asserts
       forall x, y, z:Two
          (x = y or x = z) or y = z

is illegal because Two does not belong to its sort set, which is empty.
Hence

   Foo: trait
     ... whatever ...
     implies
       AtMostTwo(T for Two)

is also illegal, because it implies an illegal trait.

     Is it an oversight or a feature that the definition of the sort set 
of a trait excludes Two from the sort set of AtMostTwo?  I'm not sure
what the original authors of LSL (John Guttag and Jim Horning) would say.
I've never been completely happy that the sort set is defined implicitly
by the operator set, and would have preferred to see explicit and separate
"declare sorts", "declare operators", and "declare variables" sections as 
there are in LP.

					Steve

• Prev: Draft list of questions for a Larch FAQ list
• Next: Re: Should I CAPITALIZE const identifiers?
• Index: Larch archive index