[Prev][Next][Index]

# LSL boolean combinations involving undefined terms

• Subject: LSL boolean combinations involving undefined terms
• From: leavens@cs.iastate.edu (Gary Leavens)
• Date: 17 Jul 95 16:03:20 GMT
• Keywords: undefined, lazy evaluation
• Newsgroups: comp.specification.larch
• Organization: Iowa State University, Ames, Iowa

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

Consider the following traits.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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

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)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Or should I have written the axioms about isPositive

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

That is, what I'm asking is in LSL can one can use boolean
combinations of terms when some of them may be undefined?
Can such terms be thought of as being evaluated lazily?

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):