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 unsigned int[]
are not directly the names of sorts,
but instead have names like Arr[Obj[unsigned]]
(see section 5 Declarations for the details on the names of sorts for such types).
One other exception is that the C++ type bool
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 int.
For types with simple names, like int,
the type's abstract values are the equivalence classes of LSL terms
of the sort with the same name (int)
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.
For example,
//@ 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 uses clause.
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 uses clause.
(See section 9.2 The Uses Clause for details on the replace-list syntax.)
For example, one might write the following uses clause,
to rename the sort D to be the type name date
in the trait DateTrait.
//@ uses DateTrait(date for D);
In this example the abstract values of the type date
are the equivalence classes of the sort date,
in the newly constructed trait;
in essence the abstract values are those of sort D in the trait
DateTrait,
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 < and > to [ and ]
they become LSL sorts.
Thus a C++ type such as Set<int> is based on a sort named
Set[int].
This translation,
mapping the C++ < and > to the LSL [ and ],
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 Obj[int],
does not mean that there is a C++ type named Obj<int>.
Furthermore, in Larch/C++, the sort-name Obj[int]
is written just like that: Obj[int].
(See section 6.1.3.2 Quantifiers for details on the syntax for sort-name.)
Traits for all of the C++ built-in types, such as int,
are automatically used in a Larch/C++ specification.
Each C++ built-in type name, such as int,
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,
such as unsigned and unsigned int,
are considered to be equivalent sort names for the purpose of sort checking.
(Unlike LCL [Guttag-Horning93], but like C++,
in Larch/C++
the types char* and 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.