A struct (the C++ keyword for structure)
or class is automatically regarded as a collection of
objects of various types
(See Sections 3.6.2 and 9 of [Ellis-Stroustrup90]).
This interpretation can be overridden by the specifier,
who may provide a trait to define the abstract values by hand
(see section 7 Class Specifications for details).
However, if the user does not supply a trait that defines a sort
with the same name as the struct or class,
then Larch/C++ will provide one automatically,
as described in this section.
In the rest of this section, we assume that the user
has not provided such a trait.
Each object in a structure is denoted by a member name in C++. The corresponding idea in the LSL values is called a field name. For example, the following declarations
struct Entry { char *sym; int val; };
Entry e;
declare a struct variable e of type Entry with
two members.
See section 5.4.4 Structure and Class Declarations for more details
on the sort of e in such a declaration.
We now describe the abstract values that are automatically specified
for structs and classes.
The automatically constructed abstract value is a fixed-length tuple with
fields and sorts as appropriate.
For each structure type declaration,
the trait defining its abstract model is implicitly used in any specification
module in which the declaration appears.
For example, the above declaration of the type Entry
is modeled by the following LSL trait.
% @(#) $Id: Entry_Trait.lsl,v 1.26 1997/07/31 21:10:11 leavens Exp $
Entry_Trait: trait
assumes char, Pointer(Obj, char), int
includes MutableObj(Ptr[Obj[char]]), MutableObj(int),
ConstObj(Ptr[Obj[char]]), ConstObj(int)
includes Entry_Pre_Trait(Entry, Obj, Val[Entry]),
Entry_Pre_Trait(Const[Entry], ConstObj, Val[Entry])
In the above trait,
the assumed traits are those included automatically by Larch/C++ to model
the types
explicitly mentioned in the declaration.
The first set of included traits models the fields both for normal
(see section 5.4.4 Structure and Class Declarations)
and constant declarations
see section 5.4.7 Constant Declarations).
In this example, the traits assumed for the field types
are an char (see section 11.1.4 Char Trait),
an instantiation of Pointer
(see section 11.8 Pointer Types),
and int (see section 11.1 Integer Types).
See section 2.8.1 Formal Model of Objects for the traits MutableObj,
and ConstObj.
The trait Entry_Trait defines three sorts: Entry,
Const[Entry],
and Val[Entry].
Since the theories of Entry and Const[Entry]
are nearly identical,
they are defined by including the trait Entry_Pre_Trait
(given below) with two different renamings.
The sort Entry is used for the abstract values of global variables
objects of type Entry.
The sort Const[Entry] is used for the abstract values of global variables
objects of type const Entry.
The sort Val[Entry] is the abstract values of value parameters
of type Entry (or type const Entry).
The sort Entry is a tuple of two objects,
the sort Const[Entry] is a tuple of two constant objects,
while the sort Val[Entry] has no contained objects.
The following is the trait Entry_Pre_Trait.
% @(#) $Id: Entry_Pre_Trait.lsl,v 1.1 1998/08/27 15:11:53 leavens Exp $
Entry_Pre_Trait(Entry, Loc, Val): trait
assumes char, Pointer(Obj, char), int,
TypedObj(Loc, Ptr[Obj[char]]), TypedObj(Loc, int),
contained_objects(Loc[Ptr[Obj[char]]]), contained_objects(Loc[int])
includes NoContainedObjects(Val), contained_objects(Entry)
Entry tuple of sym: Loc[Ptr[Obj[char]]], val: Loc[int]
Val tuple of sym: Ptr[Obj[char]], val: int
introduces
eval: Entry, State -> Val
allocated, assigned: Entry, State -> Bool
asserts
\forall entry: Entry, opoc: Loc[Ptr[Obj[char]]], oi: Loc[int], st: State
contained_objects([opoc,oi], st)
== {asTypeTaggedObject(opoc)} \U {asTypeTaggedObject(oi)};
eval(entry,st) == [eval(entry.sym, st), eval(entry.val, st)];
allocated(entry,st)
== allocated(entry.sym, st) /\ allocated(entry.val, st);
assigned(entry,st)
== assigned(entry.sym, st) /\ assigned(entry.val, st);
implies
converts
contained_objects: Entry, State -> Set[TypeTaggedObject],
eval: Entry, State -> Val,
allocated: Entry, State -> Bool, assigned: Entry, State -> Bool
The tuple notation is a LSL shorthand explained in
Chapter 4 of [Guttag-Horning93].
It should not pose any problems, as tuples are built by listing
the values, in the order of their declaration in the trait,
within square brackets ([]).
The fields are extracted with the familiar dot (.) notation.
The trait function eval allows
state functions (see section 6.2.1 State Functions) to be applied to abstract
values of sort Entry or Const[Entry];
it forms a value consisting of the values
of the component objects in the given state.
The objects contained in a structure's abstract value
are the fields of the structure.
This is described by the trait function contained_objects.
The fields of the automatically-specified abstract value
can be referenced by terms using the dot notation (.),
as in C++. Note however, that for global variables and reference
parameters, a state function must be applied first, to extract
the abstract value from the variable.
For example, one can write e'.val which has sort Obj[int],
but not e.val.
The following table shows terms involving the global variable e
and their sorts.
Term Sort Term Sort ----- ---------------- --------- ------------ e Obj[Entry] e^ Entry e^.sym Obj[Ptr[Obj[char]] e^.sym^ Ptr[Obj[char]] e^.val Obj[int] e^.val^ int e^ Entry e^^ Val[Entry]
See section 6.1.8.1 Sorts for Formal Parameters for a discussion of the sort of a formal parameter structure (and its fields).
Note that a structure or class type name in C++ is used as a sort name in Larch/C++. This is so Larch/C++ mimics C++ by-name type checking for structure and class types.
There is no distinction made between the public, protected, and private members of a structure or class for purposes of automatically defining a trait for their abstract values.
Note that if the structure or class has member functions, they are also part of the automatically constructed abstract value. See section 11.12 Function Types for a discussion of their abstract values. See section 7.1.1 A First Class Design (Person) for an example of such a trait.
Go to the first, previous, next, last section, table of contents.