[Prev][Next][Index]

Oversight in the definition of LSL(?)


Here's what seems to be a small oversight in the definition of LSL (as
given in the report on Larch 2.3).  Suppose I want to say

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


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

The definition of Larch 2.3 seems to say that Foo is illegal, because
it says:

[pg. 25]

The sort set of a trait, or a traitRef, is the set of sorts appearing
in its operator list.

The operator list of a trait is the union of the operator list of its
simpleTrait and the operator lists of the traitRefs in its externals.

The operator list of a traitRef is the image, under its name mapping,
of the union of the operators lists of the normalizations of the
referenced traits.

[pg. 24]

The operator list of a simpleTrait is "introduces" followed by the
union of the operator lists of its opDcls.

[pg. 26, on the semantic check on "newSort for oldSort"]

Each oldSort must be in the sort set of a trait referenced by the
enclosing traitRef.

Reading these strictly, Foo is illegal because Two does not belong to
the sort set of AtMostTwo. 

- David Guaspari
  davidg@oracorp.com