Go to the first, previous, next, last section, table of contents.


11.4 bool

The latest draft of the C++ standard [ANSI95] includes the type bool (see also [Stroustrup95]).

The abstract values of bool variables are modeled by the LSL sort Bool. This exception to the rule that sort names are the same as type names is made because the Booleans are so basic, and because having two separate sorts with conversions was inherently error-prone.

The trait Boolean that defines the sort Bool, and hence its synonym bool is found on page 161 of [Guttag-Horning93]. It is implicitly included in every LSL trait, and also by Larch/C++.

Larch/C++ also uses a built-in trait that defines some of the C++ Boolean operators as lsl-ops (see section 6.1.5 LSL Operator Terms). This trait is given below. See section 6.1.2 Logical Connectives for details on the syntax of logical connectives in Larch/C++ with better precedence than these.

% @(#)$Id: bool_sugars.lsl,v 1.1 1997/06/13 02:12:15 leavens Exp $

bool_sugars: trait
  % assumes Boolean
  % in Larch/C++, bool is a synonym for Bool
  introduces
    !__: bool -> bool
    __&&__: bool, bool -> bool
    __||__: bool, bool -> bool
  asserts \forall b, b1, b2: bool
    !b == ~b;
    b1 && b2 == b1 /\ b2;
    b1 || b2 == b1 \/ b2;
  implies
    AC(&&, bool), AC(||, bool)

Technically the identification of the bool and Bool is accomplished at the LSL level by having the following synonym declaration in the Larch/C++ LSL initialization file `lslinit.lsi'.

synonym   Bool   bool

This synonym declaration is standard with the LSL initialization file that ships with Larch/C++ and the LSL checker. The complete initialization file is given below.

commentSym  %

% @(#)$Id: lslinit.lsi,v 1.2 1995/11/03 05:56:37 leavens Exp $

%  Larch Shared Language (LSL) Initialization File

%  Original from page 223 in Guttag and Horning, "Larch: Languages and
%  Tools for Formal Specification"

% Modifications

%  93.11.09  Garland at MIT	Add synonym: formulas for equations
%  93.11.26  Garland at MIT	Add synonym: <=> for \iff
%  94.05.23  Garland at MIT	Remove [ as openSym, ] as closeSym
%				Remove synonyms: & for \and, | for \or,
%					! for \not, != for \neq
%				Remove synonyms used for checking LCL
%				Add synonym: with for \forall
%  95.01.03  Leavens at ISU	took out Bool synonym
%  95.11.02  Leavens at ISU	put back Bool synonym bool

idChar	    '
opChar	    ~!#$&?@|
singleChar  ;

openSym	    { \< \langle
closeSym    } \> \rangle
selectSym   .

simpleId    \bot \top

synonym	    \and	/\
synonym	    \or		\/
synonym	    \implies	=>
synonym	    \iff	<=>
synonym	    \not	not
synonym	    \not	~
synonym	    \eq		=
synonym	    \neq	~=
synonym	    \arrow	->
synonym	    \marker	__
synonym	    \equals	==
synonym     \forall     forall
synonym	    \forall	with
synonym     \eqsep      ;
synonym	    equations	formulas

synonym	    Bool	bool


Go to the first, previous, next, last section, table of contents.