Go to the first, previous, next, last section, table of contents.

11.10 Structure and Class Types

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

    eval: Entry, State -> Val
    allocated, assigned: Entry, State -> Bool

    \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.sym, st) /\ allocated(entry.val, st);
         == assigned(entry.sym, st) /\ assigned(entry.val, st);

      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 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.