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 6.1.8.1 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 6.1.3.2 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.