Oversight in the definition of LSL(?)
Subject: Oversight in the definition of LSL(?)
From: email@example.com (David Guaspari)
Date: 23 Oct 1995 10:11:39 -0400
Organization: Odyssey Research Associates, Inc., Ithaca NY
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
forall x, y, z:Two
(x = y or x = z) or y = z
... whatever ...
AtMostTwo(T for Two)
The definition of Larch 2.3 seems to say that Foo is illegal, because
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
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
Reading these strictly, Foo is illegal because Two does not belong to
the sort set of AtMostTwo.
- David Guaspari