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

6.2.2 Allocated and Assigned

The domain of a state is the set of objects that are allocated in that state. Informally, being allocated means, as you would expect, that the object is in the domain of that state. The idea that an object loc is allocated in a state st can be written in a specification as the term allocated(obj, st). (Chalin calls such objects "active" [Chalin95].)

An object can exist without being allocated. One example of such as an object would be an object on the run-time stack of C++ that was allocated by a procedure that has returned. Another example is an object that was allocated with operator new, but which has since been deleted. Formally, such objects are not in the domain of the state modeled by the trait State (see section 2.8.2 Formal Model of States).

In Larch/C++, the formal model of objects distinguishes between typed and untyped objects. (See section 2.8.1 Formal Model of Objects.) Thus by widening an untyped object, obj, to some random type Loc[T], one obtains a typed object, widen(obj). But an untyped object, even one that is allocated in a state, only underlies a finite number of typed objects, and so not all such widenings should be considered to be allocated. Hence for a typed object, the trait function allocated takes the type of the object and the types recorded in the state into account. See section 6.2.3 The Modifies Clause for one way that this distinction helps in the semantics.

Once allocated, an object may be assigned a value; objects that have no well-defined value (Chalin's term again), are unassigned. The standard example is an uninitialized variable. The term assigned(obj, st) is true if the object obj is allocated in st and has a well-defined value in st.

The details are given in the following trait. See section 2.8.1 Formal Model of Objects for the traits assumed by this trait, and for more details on the general model of objects and values.

% @(#)$Id: AllocatedAssigned.lsl,v 1.7 1995/11/10 07:42:11 leavens Exp $
AllocatedAssigned(Loc, T): trait
  assumes State, WithUnassigned(T), WidenNarrow(Loc[T], Object),
          WidenNarrow(WithUnassigned[T], Value)
  includes SortNames(Loc[T], TYPE, type_of for sort_of)
    allocated, assigned: Loc[T], State -> Bool

    \forall loc: Loc[T], st: State
      allocated(loc, st)
         == allocated(widen(loc), st)
            /\ type_of(loc) \in types_of(widen(loc), st);
      assigned(loc, st)
         == allocated(loc, st)
            /\ narrow(eval(widen(loc), st)) ~= unassigned;

    \forall loc: Loc[T], st: State
      allocated(loc, st) => widen(loc) \in domain(st);
      assigned(loc, st) => allocated(loc, st);
      assigned, allocated: Loc[T], State -> Bool

Because not all objects are allocated in a state or assigned a value (see section 6.2.2 Allocated and Assigned), and because the logic of LSL gives an arbitrary value to an expression such as eval(i,pre) when i is not assigned, one should generally avoid using a state function on an unassigned object. This can be done by requiring objects to be assigned in the precondition.

In general, you only need to specify that an object is allocated when using pointer variables. (See section 11.8 Pointer Types for the trait functions used with pointers.) Larch/C++ has constraints on variables and reference parameters used in specifications that eliminate the need to state explicitly whether variables are allocated, except for pointers.

Larch/C++ does provide a syntactic sugar that implicitly requires reference parameters and global variables used in functions to be allocated. Implicitly, the term allocated(x,pre) is conjoined to the precondition of each function specification, for each such reference parameter and global variable, x. Note that such objects are not required to be assigned, only allocated.

For example, the following is the desugared form of the specification of add_one given above (see section 6.2.1 State Functions). The desugaring actually produces a redundant requirement in this example (because assigned(x, pre) implies allocated(x, pre)), but this illustrates the sugaring process.

// @(#)$Id: add_one_desugared.lh,v 1.5 1997/06/03 20:29:56 leavens Exp $
extern void add_one(int& x) throw();
//@ behavior {
//@   requires allocated(x, pre)   // added by the syntactic sugar
//@            /\ assigned(x, pre) // x is allocated and has a value
//@            /\ x^ < INT_MAX;    // x^ : pre-value of x
//@   modifies x;                  // x  : an object
//@   ensures x' = x^ + 1;         // x' : post-value of x
//@ }

Similarly, the implicit parameter (this) in a member function specification is required to be a well-defined, non-null pointer variable that points to an assigned object (self). (Recall that the pre-state of a constructor is not considered a visible state.) See section 7 Class Specifications for more about the this pointer and self.) Furthermore, if there are class members visible, then because of the last conjunct for the implicit argument, these class members are also required to be assigned.

These implicit preconditions are summarized in the following table.

what               declaration   implicit precondition conjuncts
----------------   -----------   -------------------------------
formal parameter   T & x         allocated(x, pre)
formal parameter   T * x                             // none!
global variable    extern T x    allocated(x, pre)
implicit argument                assigned(this, pre) /\ assigned(self, pre)
                                 /\ assigned(self^, pre)
class member       T dm          assigned(dm, pre)   // follows from above

Recall that objects that are allocated or assigned stay allocated or assigned unless they are mentioned in a trashes-clause. Hence it is not usually necessary to state that parameters or implicit arguments remain allocated or assigned in a postcondition. See section 6.3.2 The Trashes Clause for more details on this point.

When a new object is created by a function, there is no implicit conjunct in a post-condition that says that it must be allocated or assigned. Such a conjunct must be written explicitly if desired. Often, however, you will write such an assertion using fresh, to assert both that the storage returned is allocated, and that it was not allocated in the pre-state (see section 6.3.1 Fresh). The following is an example.

// @(#)$Id: new_int.lh,v 1.4 1997/06/03 20:30:15 leavens Exp $
int & new_int() throw();
//@ behavior {
//@   ensures fresh(result);
//@ }

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