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)
introduces
allocated, assigned: Loc[T], State -> Bool
asserts
\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;
implies
\forall loc: Loc[T], st: State
allocated(loc, st) => widen(loc) \in domain(st);
assigned(loc, st) => allocated(loc, st);
converts
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.