Pointers are somewhat more complex than references. Consider the following.
Declaration Name Its Sort (when used as a global variable) ------------- ---- ----------------------------------------- int i = 7; i Obj[int] int * ip = &i; ip Obj[Ptr[Obj[int]]]
The sort of ip, when used as a global variable,
is Obj[Ptr[Obj[int]]], which means that ip is an object
containing a pointer to an integer variable.
(That is, ip is a pointer variable.)
The sort of ip' is Ptr[Obj[int]],
which means that ip' is a pointer value (address)
that points to an integer object.
The sort of *(ip') is Obj[int]
as the * dereferences the pointer value
(the address contained in ip in the state after the call).
The sort of (*(ip'))' is int,
which is the integer value in the object pointed to by the
address contained in ip in the state after the call.
A global variable declaration such as T *tp;,
makes Larch/C++ implicitly use the following traits:
MutableObj(Ptr[Obj[T]])
(see section 2.8.1.1 Formal Model of Mutable Objects),
and Pointer(Obj, T).
See section 11.8 Pointer Types for details on the trait Pointer
used to define the abstract values of pointers,
and the instantiations used for various pointer types.
See section 11.8 Pointer Types for the traits that define pointers to members.
They are the same as the pointer traits, except
that instead of using sorts of the form Ptr[T],
they use sorts of the form PtrMbr[T].
Go to the first, previous, next, last section, table of contents.