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

11.11 Union Types

In C++, a union is "a structure whose member objects all begin at offset zero (i.e., member objects overlap in memory) and whose size is sufficient to contain any of its member objects" (Section 9.5 of [Ellis-Stroustrup90]). For example, the following declarations

union U {int i_var; char *char_p;};
U x;

declare a union variable x of type U with two members. See section 5.4.5 Union Declarations for more details on the sort of x in such a declaration. In this section we describe the automatically-constructed trait that models the abstract values of unions. (This model can be overridden by the specifier, who may provide a trait to define the abstract values. This is done by using a trait which has a sort with the same name as the union's sort. See section 7 Class Specifications for details. In the rest of this section, we assume that the user has not provided such a trait.)

The abstract value of a C++ union is a tagged discriminated union, with field names and sorts for its declaration. All the fields of a union that are simple variables are modeled by typed locations that widen to the same untyped object (See section 2.8.1 Formal Model of Objects). That is, changing the value in one location (e.g., in the field i_var) may change the value in the other locations (e.g., in the field char_p). This is just what would happen in C++, and hence each location depends on the others [Chalin95].

For each union 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 U is modeled by the following LSL trait.

% @(#)$Id: U_Trait.lsl,v 1.17 1997/07/31 21:14:02 leavens Exp $

U_Trait: trait
  assumes int, Pointer(Obj, char)
  includes MutableObj(int), MutableObj(Ptr[Obj[char]]),
           ConstObj(int), ConstObj(Ptr[Obj[char]])
  includes U_Pre_Trait(U, Obj, Val[U]),
           U_Pre_Trait(Const[U], ConstObj, Val[U])

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.5 Union 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 U_Trait defines three sorts: U, Const[U], and Val[U]. Since the theories of U and Const[U] are nearly identical, they are defined by including the trait U_Pre_Trait (given below) with two different renamings.

The sort U is used for the abstract values of global variables objects of type U. The sort Const[U] is used for the abstract values of global variables objects of type const U. The sort Val[U] is the abstract values of value parameters of type U (or type const U). The sort U is a LSL union of two locations, both of which share the same untyped object. The sort Const[U] is a LSL union of two constant locations, both of which share the same untyped object. The sort Val[U] has no contained objects.

The following is the trait U_Pre_Trait.

% @(#)$Id: U_Pre_Trait.lsl,v 1.2 1997/07/31 21:14:14 leavens Exp $

% Improved in response to a criticism of Chalin's [Chalin95]

U_Pre_Trait(U, Loc, Val): trait

  assumes int, Pointer(Obj, char),
          TypedObj(Loc, int), TypedObj(Loc, Ptr[Obj[char]]),
          contained_objects(Loc[int]), contained_objects(Loc[Ptr[Obj[char]]])
  includes NoContainedObjects(Val),

  U union of i_var: Loc[int], char_p: Loc[Ptr[Obj[char]]]
  Val union of i_var: int, char_p: Ptr[Obj[char]]

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

    \forall st: State, u: U, s: Loc[Ptr[Obj[char]]], i: Loc[int]

       % both tags share the same untyped object
       widen(i_var(i).char_p) == widen(i_var(i).i_var);
       widen(char_p(s).i_var) == widen(char_p(s).char_p);

       % a union with a given tag contains the object tagged with each sort
       contained_objects(i_var(i), st)
         == {asTypeTaggedObject(i)}
            \U {asTypeTaggedObject(narrow(widen(i)):Loc[Ptr[Obj[char]]])};
       contained_objects(char_p(s), st)
         == {asTypeTaggedObject(s)}
            \U {asTypeTaggedObject(narrow(widen(s)):Loc[int])};

       eval(i_var(i), st) == i_var(eval(i, st));
       eval(char_p(s), st) == char_p(eval(s, st));

       allocated(i_var(i), st) == allocated(i, st);
       allocated(char_p(s), st) == allocated(s, st);
       assigned(i_var(i), st) == assigned(i, st);
       assigned(char_p(s), st) == assigned(s, st);

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

The shorthand notation for union definitions in LSL traits is explained in Chapter 4 of [Guttag-Horning93]. The notation for referring to a "field" of a union is the same as in C++, but there is also a way to create a union with a particular tag; for example, i_var(i) creates a U value with tag i_var.

[[[Fields that are arrays overlap as dictated by C++. An example might be good here.]]]

The parts of a union 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 (see section 6.2.1 State Functions). For example, one can write x'.i_var which has sort Obj[int], but not x.i_var. A state function cannot be applied to a union abstract value, because it is not clear what tag should apply. The following table shows terms involving the global variable x and their sorts. Note that both of the last two lines will be defined in every state, although the exact values obtained by changing the value with one type and reading it out using another are not specified.

Terms    Sorts                  Terms       Sorts
-----    -------------------    ---------   ------------------
x        Obj[U]                 x'          U
                                tag(x')     U_tag
x.i_var  Obj[int]               x'.i_var'   int
x.char_p Obj[Ptr[Obj[char]]]    x'.char_p'  Ptr[Obj[char]]

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