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

### 6.2.1 State Functions

If an object is assigned in a state (see section 6.2.2 Allocated and Assigned), then its abstract value can be obtained by using a state-function.

```state-function ::= `^` | `\pre` | `'` | `\post` | `\any` | `\obj`
```

The value in the pre-state will be called the pre-value and the value in the post-state will be called the post-value.

For example, consider the following.

```// @(#)\$Id: add_one.lh,v 1.6 1997/06/03 20:29:55 leavens Exp \$
extern void add_one(int& x) throw();
//@ behavior {
//@   requires 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
//@ }
```

Informally, `add_one` takes an integer object passed by reference, and adds 1 to it. More formally, assuming that `x` has a well-defined value, and that the value of `x` in the pre-state is not too large to be incremented, the post-value of `x` is one greater than the original value of `x`.

The following table summarizes the sorts of terms using the different state functions.

```term     sort (assuming x declared as: int & x)
----     -------------------------------------
x        Obj[int]
x^       int
x\pre    int
x'       int
x\post   int
x\any    int
x\obj    Obj[int]
```

The state-functions `^` and `\pre` are synonymous, and both are used to extract the pre-value of an object. The state-functions `'` and `\post` are synonymous, and both are used to extract the post-value of an object. For invariants (see section 7.3 Class Invariants) and other situations where one wishes to extract the value of an object, but for which no particular visible state is appropriate, the state-function `\any` can be used. By a visible state we mean a state that a client can observe. For a class with no public data members (see section 2.3 Accessibility of Class Members in Specifications), the visible states are the state just after an instance is created and initialized by a creator, and the states just before and just after the call to any member function (or friend function), in which the instance is passed. For a class with public data members, every state is a visible state, which is a good reason not to have public data members.

The state-function `\obj` can be used to explicitly refer to an object itself, instead of its value. It is essentially a no-op, and thus need only be used for emphasis.

Formally, the value of applying a state-function to a value (which will usually be an object), is given by passing the value and the appropriate state to the trait function `eval` in the trait `TypedObj` (see section 2.8.1 Formal Model of Objects for the trait `TypedObj`). For example, `i^` means `eval(i,pre)`. (See below for syntactic sugars that allow a state-function to be applied to a value that is not an object.)

(One can also write `eval(i,pre)` in specifications. However, `i^` is shorter, and hence is the preferred form in Larch/C++.)

Except for syntactic sugars discussed below, the state-functions can only be applied to terms that denote objects; that is to terms whose sort has the form `Obj[T]` or `ConstObj[T]` for some `T`. The sort of a term with state-function `\obj` is unchanged, but sorts `^`, `\pre`, `'`, `\post`, and `\any` take off the leading `Obj` or `ConstObj` sort generator.

You can only use a state-function on a formal parameter name if that name parameter is passed by reference. (More precisely, you can only use a state-function on values for which the trait function `eval` is defined, this is usually only object sorts.) Value parameters are not considered objects in Larch/C++ (see section 6.1.8.1 Sorts for Formal Parameters) and so the following is an error. (See section 11.1 Integer Types for the trait function `to_int`.)

```bool equal(int x, int y);
//@ behavior {
//@   ensures result = (x^ = y^); // error
//@ }
```

In the above example, both `x` and `y` denote values not objects; thus `^` cannot be used. A legal `ensures` clause would be `ensures result = (x = y);`.

For C++ arrays, one can apply a state-function to the elements of the array. For example, the following specifies a function that adds one to each element of an array. Recall the sort of the formal parameter declared `int ai[]` is `Ptr[Obj[int]]`, because such C++ syntax means that a pointer (into the array) is passed. The term `assignedUpTo(ai,siz)` (see section 11.8 Pointer Types) means that the pointer is not null, that the integers 0 to `siz`-1 (inclusive) are legal indexes for this pointer, and that each element in that range is an allocated object with a well-defined value. Thus the pointer can be treated as an initialized array of size `siz`. To avoid a syntax error, a parenthesis is needed around `ai[i]` in terms like `(ai[i])^`. This is because `ai[i]` is a secondary, and a state-function can only be applied to a primary. See section 6.1.7 Primaries for the syntax of primary. See section 6.1.6 Brackets and Braces for the syntax of secondary.

```// @(#)\$Id: array_add_one.lh,v 1.12 1997/06/03 20:29:57 leavens Exp \$
extern void array_add_one(int ai[], int siz) throw();
//@ behavior {
//@   requires 0 <= siz /\ assignedUpTo(ai, siz)
//@        /\ \A i:int ((0 <= i /\ i <= (siz-1))
//@                      => (ai[i])^ + 1 <= INT_MAX);
//@   modifies ai;
//@   ensures \A i:int ((0 <= i /\ i <= (siz-1))
//@                      => (ai[i])' = (ai[i])^ + 1);
//@ }
```

An array name (for global array variables), or a pointer formal, such as `ai` in the above example, is not an object. However, as in LCL we extend the meaning of the state-functions to arrays (and to pointers into arrays) element-wise. In the context of `array_add_one`, this extension makes `ai'` stand for the abstract value of sort `Arr[int]` that maps each legal index `i` of `ai` (if any) to `(ai[i])'`. Note that the sort of `ai'` is not a pointer sort, but an array sort. In the above example, both `(*ai)'` and `ai'[0]` would mean the same thing, and the syntax `(ai[i])^` could be equivalently written as `ai^[i]` (or even `(*(ai + i))^`).

These syntactic sugars are defined because the trait function `eval` is defined for pointers and arrays in the traits `Pointer` (see section 11.8 Pointer Types) and `Array` (see section 11.7 Array Types). That is, `ai'[i]` is defined when the term `(eval(ai,post))[i]` is defined, because the latter is the desugared version of the former.

The sort `Arr[int]` is defined by the trait `Array` (see section 11.7 Array Types), which is included in the trait `Pointer` (see section 11.8 Pointer Types).

The same sugar applies to multi-dimensional arrays. For example, if `aai` is a two-dimensional array of `int`s (declared as a global variable), then `aai'` means `eval(aai,post)`. As defined in the trait `MultiDimensionalArray` (see section 11.7 Array Types), this is the abstract value of sort `Arr[Arr[int]]` that assigns to each pair of legal indexs, `i` and `j`, the abstract value `((aai[i])[j])'`.

The same kind of sugar is defined for pointers to arrays. See section 11.8 Pointer Types for details in the trait `PointerToArray`.

For C++ structures and classes that use the default (automatically-constructed) trait, one can apply a state-function to the fields of its abstract value. For example, consider the following global structure variable definition.

```struct Ratl { int num, denom; };
Ratl my_ratl;
```

One can write `my_ratl^.denom^`, which has sort `int`, because `my_ratl^.denom` is an object of sort `Obj[int]`. See section 11.10 Structure and Class Types for details on the automatically constructed traits for structures and classes.

In the default traits for structures and classes, Larch/C++ extends the meaning of the state-functions to the tuples that are their abstract values element-wise. Thus one can write `my_ratl^^`, which means `eval(eval(my_ratl,pre),pre)`; because the trait function `eval` is defined on the sort `Ratl` to return a value of sort `Val[Ratl]`. That is, `my_ratl^^`, applies the state-function `^` to the tuple that is the result of `my_ratl^`, and is thus equal to the following.

```[my_ratl^.num^, my_ratl^.denon^]
```

This last term denotes an abstract value of sort `Val_Ratl`, containing the numerator and denominator values in the pre-state. Hence `my_ratl^^.num` has sort `int`. It follows that `my_ratl^^.num` and `my_ratl^.num^` mean the same thing. One way to see this is that `my_ratl^.num` has sort `Obj[int]`, because `my_ratl^` is a tuple of objects. See section 11.10 Structure and Class Types for more examples, and for details of how the trait functions `eval` and the sort `Val[Ratl]` are defined).

You may define a similar shorthand for the abstract values of a type you specify the abstract values of explicitly (see section 7 Class Specifications), by specifying in LSL what the trait function `eval` means for the abstract values. Once this is done, the meaning of a state function gives the appropriate shorthand.

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