Step 1: Precondition and Postcondition

We start by determining the state of the input and how it relates to the state upon completion.

Notice that the computation

B := L-1 B

indicates that upon completion of the loop variable B must be in a state, the postcondition, where it satisfies

B = L-1 B&circ.

Here B&circ indicates the original contents of B .

We indicate that B originally contains B&circ by asserting at the top of the algorithm that

B = B&circ,

which is called the precondition.

Note: In filling in the worksheet, we will use B with a "hat" above it to indicate the original contents of B. This is to be consistent with conventions we use in our papers.
Note: Strictly speaking, other conditions like the fact that the dimensions of L and B conform and the special structure of L should also be expressed in the precondition and in the predicates that describe state at various points. We do not state these other conditions to keep the worksheet simple.

[ UPDATE SOURCE ] [ VIEW PDF PS ]

[ BACK ] [ NEXT ]