As in Section 3.7 of [Ellis-Stroustrup90],
"an object is a region of storage."
Note that a C++ variable of type int is an object in this sense,
although it does not respond to messages.
We use the term instance for emphasis when discussing
an object of a class;
instances are what are usually called objects in object-oriented programming.
Instances respond to messages.
A variable of type int is not an instance.
All objects in C++ have an address, or location,
which we will sometimes call an object identifier.
Values are stored in objects.
To emphasize that a value is the value of an instance of a class,
we sometimes use the term instance value.
In contrast to the abstract values used in specifications,
the values manipulated by C++ programs,
are thought of as concrete values.
Each concrete value, a bit pattern, is thought of as a representation of
an abstract value.
For example, a C++ int variable holds a bit pattern that corresponds
to an abstract value which is a mathematical integer,
specified by the trait int (see section 11.1 Integer Types).
As an illustration of the concept of objects and values,
the following is a picture of the Larch/C++ model of an integer variable,
i.
In the picture, i is an object, which contains the abstract value 228.
To be more specific, the following is a picture of i in some
program state.
A state, as in the picture, associates to each object, an abstract value.
The abstract value of an assignment may change from state to state,
as the program executes (for example, the value of i may be changed
by an assignment statement in C++).
For the most part, Larch/C++ specifications only describe states just before
and just after the call of a C++ function.
!-----------------!
i: ! 228 !
!-----------------!
The Larch/C++ model of an integer variable,
containing the abstract value 228.
Unlike C++, in the Larch/C++ model, an object can contain an arbitrarily
complex abstract value.
That is, a state may map an object to any value defined by a trait.
For example, the Larch/C++ picture of a variable myHeap of type
IntHeap might be as follows.
See section 1.1 Larch-style Specifications for the specification
of the class IntHeap and the trait that defines its abstract values.
!------------------------!
myHeap: ! add(6, add(7, empty)) !
!------------------------!
The Larch/C++ model of an IntHeap variable,
containing the abstract value add(6, add(7, empty)).
Finally, in Larch/C++, values can contain objects,
which enables complex, even circular, object structures to be modeled.
(One way to think of this is that objects are just a special kind of
abstract value.)
For example, the following is a picture of variable mySet,
whose abstract value is a set of point objects.
The picture represents the abstract value of the set as {*,*,*},
where the *s are the tails of three arrows that show what object
is contained in the set. Each of the point objects has an abstract value
that is a LSL tuple of two integers.
In general, users of Larch/C++ will model objects and values in such layers.
!----------------------------!
mySet: ! { * , * , * } !
!----!---------!---------!---!
! ! !
v v v
!--------! !--------! !----------!
! [3, 4] ! ! [5, 6] ! ! [-12, 5] !
!--------! !--------! !----------!
The Larch/C++ model of a Set variable with an abstract
value that contains containing three other objects.
The word lvalue means a term (something like a C++ expression, see section 6.1 Predicates for details) that denotes an object or a function. Recall that in C++ an array name is not an lvalue.
In contrast to C++ (but like LCL), Larch/C++ does not consider
formal parameters passed by value to be objects.
This is because parameters passed by value cannot be changed from the point
of view of the client (the caller),
and so are not objects from the point of view of the client.
Therefore in Larch/C++, only formal parameters passed by reference are objects.
Pointers that are passed by value are not objects but do point to objects.
For example, within the specification of a function with the following heading
the expressions cr and *ip are lvalues (denote objects), but
i and ip are not.
int foo(int i, char & cr, int * ip)
Whether or not a formal parameter is declared to be const
does not affect this distinction.
For example, within the specification of a function with heading
int foo(const int ci, const char & ccr, const int * cip)
the expressions ccr and *cip are lvalues, but
ci and cip are not.
The name result is used in postconditions to stand for what
is returned by the C++ function being specified.
It is considered to be an object only
if the return type of the function is a reference type.
That is, result is treated in the same way as a formal parameter.
For example, within a function specification with the above header,
result is not an lvalue.
However, if the return type were specified as int &, then
result would be an lvalue.
Values are formally modeled by various traits, most of which are specified by Larch/C++ users in LSL. Objects are formally modeled by the traits described below. These traits build on the more primitive notion of a state; states are formally modeled by another trait described below.
(Some of the discussion in the subsections below is quite technical. If you are new to Larch/C++, feel free to skim these subsections.)
Go to the first, previous, next, last section, table of contents.