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


6.12.1 Terminates

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.