An assertion that precedes a statement is called a precondition of the state-
ment. An assertion that follows a statement is called a postcondition . Such a pre-
condition-statement-postcondition triple has the following meaning:
Execution of the statement begun with the precondition true is
guaranteed to terminate, and when it terminates, the postcondition
will be true.
When you see a relation enclosed in braces within a comment, you should
assume that the program author is asserting that that relation is true at that point.
The earlier code ensures that the relation is true; the later code relies on it being
true. In later sections, you will see hints from time to time about when and where
to use such assertions.
A model of execution
We now show you precisely how a method call is executed. Learning this mate-
rial, and being able to execute method calls yourself using our model of execu-
tion, will make writing programs much easier. You will know what is going on
inside the computer. Further, from time to time you will want to execute a
method call by hand in order to pinpoint a difficult-to-find error in your program.
This section requires knowledge of classes and our view of a class as a file
drawer of manila folders.
Frames for method calls
Whenever a method is called, some memory is set aside to contain information
related to the call: parameter values, the current statement being executed, and
so on. This memory is called the frame for the call . Figure 2.8 shows the format
of the frame that we use throughout this text. We discuss its components:
gives a pictorial
Method-name. The method name appears in a box in the upper-left of
local variable n
local variable 2
local variable 1
Format of the frame for a method call