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.