Step 2: Determine the loop-invariant
We now show how to determing an intermediate state of the
variable B. The idea is to recognize that inherently
one will sweep through the arrays that store L and B
in a consistent fashion. In particular,
partition the variables like
,
where the partitioning is conformal so that
- LTL is square, and
- the number of rows in BT equals the
number of rows in B&circT
which equals the dimension of LTL .
Next, we substitute these partitioned matrices into the postcondition
to yield
,
which, since
.
simplifies to
,
[
BACK
]
[
NEXT
]