A function call terminates if it returns to its caller or throws an exception. A function call does not terminate if it goes into an infinite loop, halts execution of the program (gracefully or not), or jumps in such a way that it does not return or throw an exception that could be caught by its caller.
Taking termination into account, we can model a C++ function by
a nontotal relation from proper pre-states to post-states.
A state is proper if it is not bottom
(see section 2.8.2 Formal Model of States);
bottom represents infinite looping and other kinds of
abnormal termination.
A pre-state may or may not be related to a post-state by the relation
specified in a Larch/C++ specification,
and if it is related to a post-state, that post-state could be bottom.
(A pre-state that is not related to a post-state value is one for which
execution is "refused" [Nelson89] [Hesselink92].
Such relations cannot be implemented in C++, but are useful for purposes
of program refinement.)
Go to the first, previous, next, last section, table of contents.