[Prev][Next][Index]

LSL boolean combinations involving undefined terms

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
as follows instead?

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