In Larch/C++, the interface layer specifies types, which can be used
in C++ programs.
The shared layer specifies sorts, which are used in traits.
Each type identifier specified in a Larch/C++ specification
must also be the name of an LSL sort.
However, compound C++ type expressions like
are not directly the names of sorts,
but instead have names like
(see section 5 Declarations for the details on the names of sorts for such types).
One other exception is that the C++ type
is modeled by the LSL sort
Bool (see section 11.4 bool).
There can also be sorts that are not names of types;
these auxiliary sorts may ease the task of writing a specification.
Larch/C++ also automatically introduces certain auxiliary sorts
to model some features of C++.
An example is the sort
Obj[int] which is a sort for
objects (i.e., variables, see section 2.8 Objects and Values)
whose abstract values are of sort
For types with simple names, like
the type's abstract values are the equivalence classes of LSL terms
of the sort with the same name (
that also satisfy the type's invariant (see section 7.3 Class Invariants).
For classes and structures, Larch/C++ can automatically construct
a trait that defines the abstract values.
Alternatively, the user can explicitly specify the
abstract values by naming a LSL trait that defines the
type name as a sort in the
uses clause in a specification.
//@ uses MyTrait;
If, as often happens, the C++ type name is different than the
sort name used in the trait,
one can change the name in the trait in the
In effect this constructs a new trait on the spot,
with the sort renamed to be the desired type name.
One does this using a replace-list in the
(See section 9.2 The Uses Clause for details on the replace-list syntax.)
For example, one might write the following
to rename the sort
D to be the type name
in the trait
//@ uses DateTrait(date for D);
In this example the abstract values of the type
are the equivalence classes of the sort
in the newly constructed trait;
in essence the abstract values are those of sort
D in the trait
but it is convenient to think of the process as producing a new trait.
The names of C++ template types are not legal as LSL sorts,
but by changing the
they become LSL sorts.
Thus a C++ type such as
Set<int> is based on a sort named
mapping the C++
> to the LSL
happens automatically when moving from C++ to LSL,
and users normally need not be concerned with it.
However, this translation does not work in the other direction.
That is, just because there is a sort named
does not mean that there is a C++ type named
Furthermore, in Larch/C++, the sort-name
is written just like that:
(See section 22.214.171.124 Quantifiers for details on the syntax for sort-name.)
Traits for all of the C++ built-in types, such as
are automatically used in a Larch/C++ specification.
Each C++ built-in type name, such as
is also the name of a sort.
See section 11 Built-in Types for the details on how the abstract values
of these types are modeled in LSL.
Equivalent C++ type-ids,
are considered to be equivalent sort names for the purpose of sort checking.
(Unlike LCL [Guttag-Horning93], but like C++,
char are the same when used as
formal parameters [Chalin95] [Chalin-etal96].)
C++ typedefs (see section 5.2.5 Typedef Specifiers) are expanded before being used in sort checking, and so do not introduce new types or sort names.
Go to the first, previous, next, last section, table of contents.