Step 4: Determine the Initialization

We now turn to the initialization. What we need is an initialization step that ideally has the following properties:
  1. the precondition implies that the initialization puts the variables in a state where the loop-invariant is true and
  2. no actual computation needs to be performed.
In considering these conditions, and the fact that the loop-invariant requires a partitioning of the operands, we arrive at the initialization

Notice that after this initialization
  1. BB = B,
  2. B&circB = B,
  3. LBL has 0 columns,
  4. LTL is 0 × 0 , and
  5. LBL LTL-1 BT = 0 .
so that

is equivalent to

.

We conclude that the precondition followed by the initialization put the variables in a state where the loop-invariant is true.

[ UPDATE SOURCE ] [ VIEW PDF PS ]

[ BACK ] [ NEXT ]