[Prev][Next][Index]

# Re: LSL boolean combinations involving undefined terms

```leavens@cs.iastate.edu (Gary Leavens) writes:

>Here's a question about LSL that's starting to bother me.
>I don't see a discussion of this in the Larch book.

No one else has answered yet, so let me say more of what

I realized yesterday after sending off this, that it's
impossible to answer my question without knowing what
I had in mind.  Of course, a trait is "correct" or not
only if it corresponds to some intuition.
What I had intended was that the traits specify
a function, isPositive that returns true if and only if
its argument has tag 'theInt' and is positive.
I didn't want to leave the case isPositive(theBool(b))
underspecified.  So I suppose I should have added some
checkable redundancy:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
QTrait : trait
includes Integer

Q union of theBool: Bool, theInt: Int

introduces
isPositive: Q -> Bool

Q1: trait
includes QTrait
asserts \forall q: Q
isPositive(q) == (tag(q) = theInt) /\ q.theInt > 0
implies
converts isPositive
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Now perhaps the following makes more sense...

>My first question is, is the trait Q1 written correctly?

I think, looking at the trait Boolean in the Larch book,
that this is correct.  There is a rule in that trait:
false /\ b == false,
which seems to give the required false when tag(q) = theBool.
However, despite the implication (implies AC(/\, Bool) in that trait,
I don't see where the commutivity comes from in the axioms,

>If the trait Q1 is ok, how about Q2, below?

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Q2: trait
includes QTrait
asserts \forall q: Q
isPositive(q) == q.theInt > 0 /\ (tag(q) = theInt)
implies
converts isPositive
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

I believe now, however, that the following is equivalent
to Q1.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Q3: trait
includes QTrait
asserts \forall q: Q
isPositive(q) == if (tag(q) = theInt)
then q.theInt > 0
else false
implies
converts isPositive
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%