Re: LSL boolean combinations involving undefined terms

In article <leavens.806079418@bambam.cs.iastate.edu>,
 leavens@cs.iastate.edu (Gary Leavens) writes:

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

The three definitions of isPositive (given in the traits Q1, Q2, and
Q3) are equivalent and they fully define isPositive.

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

LSL is defined in terms of a multisorted first-order logic with equality; see
[GHM90, p. 22 and Appendix I].  The Boolean trait is for documentation only.

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

Commutativity can be proven by induction and probably so can associativity.


[GHM90]  is 

@TechReport(    Guttag90,
       Author = {Guttag, John~V. and Horning, James~J. and Modet, Andr\'es},
        Title = {Report on the {L}arch {S}hared {L}anguage: Version 2.3},
         Type = {Report},
       Number = 58,
  Institution = {DEC Systems Research Center},
      Address = {Palo Alto, CA},
        Month = {April 14},
         Year = 1990,
         Note = {Superseded by Chapter 4 of \cite{Guttag93}}

P. Chalin			    http://www.cs.concordia.ca/~faculty/chalin
Computer Science Department	    TEL: (514) 848-3000    FAX: (514) 848-2830
Concordia University		    E-MAIL: chalin@cs.concordia.ca
1455 de Maisonneuve Boulevard West, Montreal, Quebec, Canada H3G 1M8	

Follow-Up(s): Reference(s):