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),
contained_objects(U)
U union of i_var: Loc[int], char_p: Loc[Ptr[Obj[char]]]
Val union of i_var: int, char_p: Ptr[Obj[char]]
introduces
eval: U, State -> Val
allocated, assigned: U, State -> Bool
asserts
\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);
implies
converts
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.