[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 think about it...
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,
so I still wonder about...
>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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Comments?
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):