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

The Larch/C++ keyword result stands for the result of a function (when it does not throw an exception). Its sort is determined as if result were a formal parameter declared like the result type of the function. For example, consider the following.

Function Declaration   Sort of result (used in body of foo)
--------------------   ------------------------------------
int foo(float x)       int
int & foo(float x)     Obj[int]
int * foo(float x)     Ptr[Obj[int]]
void foo(int & i)      void
void *foo(int *ip)     Ptr[Obj[void]]

See section Sorts for Formal Parameters for details on determining the sorts of formal parameters; these details are the same for determining the sort of result. See section 11.5 void for the trait that defines the abstract values of the C++ type void.

See section 6 Function Specifications for a simple example. See section Quantifiers for a more interesting example, where result is described more indirectly.

Although result can be used in functions whose return type is void, doing so is confusing and is best avoided. The Larch/C++ model for the type void is a set whose only element is written theVoid. Because of there is only one element in this sort the term result = theVoid is always true [Jones95e]. If you want to assert that a function that returns void returns instead of signaling an exception, the correct term to use is returns (see section 6.11 Exceptions for more details and examples).

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