Consider the following C++ type definition.
struct Entry { char *sym; int val; };
According to the semantics of C++, one can equivalently also write the following.
class Entry {public: char *sym; int val; };
The sort of a global variable e of this type is ConstObj[Entry].
Declaration Name Its Sort (when used as a global variable) ------------- ---- ----------------------------------------- Entry e; e ConstObj[Entry]
That e has sort ConstObj[Entry] means that
it is an object whose abstract value cannot be changed.
This may seem strange, but the explanation reveals a lot about how Larch/C++
automatically models C++ objects.
A picture of how C++ stores e in memory follows.
In this picture, the crudely-drawn box and the two sub-boxes
represent locations.
The point is that e and e.sym share the same address
in memory.
!-----------------------------------!
e: ! ! !
!-----------------------------------!
e.sym e.val
A picture of the storage set aside for e by C++.
The Larch/C++ model, on the other hand, has a single abstract value inside
each location.
Even though there is more than one location within e,
namely e.sym and e.val,
Larch/C++ does not model the abstract value of e as two locations.
Instead, Larch/C++ must model the abstract value of e
as a single mathematical entity: a tuple containing the locations
for e.sym and e.val.
The picture for Larch C++ thus looks as follows.
!-----------------------------------!
! [ * , * ] !
!-------|------------|--------------!
e | |
v v
!-----------------------------------!
! ! !
!-----------------------------------!
e.sym e.val
A picture of the Larch/C++ model of e.
The above picture shows that e is modeled in Larch/C++ as a location,
which contains as its abstract value a tuple (drawn as [*,*],
where the two asterisks, *, are the tails of two pointers).
This tuple contains two locations, namely the locations for e.sym
and e.val.
However, this tuple of locations is fixed,
because e always has the same two fields in C++.
So since the abstract value of e cannot change,
it is modeled in Larch/C++ as a constant object.
Hence the sort of e is ConstObj[Entry], not Obj[Entry].
The sort Entry is thus a tuple of two locations.
See section 11.10 Structure and Class Types for details on the trait that specifies the sort
Entry.
The meaning of the sort ConstObj[Entry] is given
by the trait ConstObj(Entry)
which Larch/C++ implicitly uses when it encounters the declaration of e.
See section 2.8.1.2 Formal Model of Constant Objects for the trait ConstObj.
All of this is rather more complex than one might like,
but in actual use it's not so bad.
Before getting to the reasons for the complexity, it is important to point
out how it can be avoided:
one can use a trait that defines the sort Entry
(and the trait function contained_objects).
When one specifies such a trait,
one can specify an abstraction that hides the details of locations, etc.
By using a trait with a sort of the same name as the struct,
the specifier prevents Larch/C++ from automatically constructing the
(complex) model, and instead directly supplies the model.
This enables the specifier to use something simple as the abstract value of
an instance of a class, such as a tuple of a character string and an integer.
(Compare that to a tuple of locations,
the first of which contains a pointer to an array containing objects
containing characters,
and the second of which contains a location containing an integer!)
See section 7 Class Specifications for details on how to specify
classes and structs with such models.
See section 7.1.1 A First Class Design (Person)
for a comparable example, the class Person.
Now for the reasons for the complexity of the automatically-supplied
Larch/C++ model of structs.
The main reason is that, if one is to model C++ faithfully,
then one has to model a struct variable, such as e, as an object.
This is because in C++ one can, for example, take the address of e.
So without further information from the specifier, Larch/C++ cannot
know how e is to be used.
Because Larch/C++ cannot make any assumptions about how e
is to be used, no simpler model will do.
The second reason for this complexity is that Larch/C++ generally models objects and their values in layers. That is, informally, an object contains a single abstract value, an abstract value may contain objects, and these objects may each contain a single abstract values, etc. The illusion of multiple abstract values may be imposed using a tuple for the abstract value, but mathematically there is only one abstract value.
Returning to more mundane considerations,
consider applying state functions to e
(see section 6.2.1 State Functions).
The sort of e' is Entry,
which is a (LSL) tuple of two objects (see section 11.10 Structure and Class Types for details).
The field sym denotes an object of sort Obj[Ptr[Obj[char]]]
and the field val denotes an object of sort Obj[int].
That is, the term e'.sym has sort Obj[Ptr[Obj[char]]]
and e'.val has sort Obj[int].
Go to the first, previous, next, last section, table of contents.