Step 7: Determine the required
state of the exposed submatrices
after moving the double lines
Again, the exposed submatrices are what will be updated. To determine
how to update them requires us to also determine what their
contents must be so that after moving the double lines
the partitioned matrices are again in a state where the
loop-invariant is true (at the bottom of the loop-body).
Again, the key here is to realize that the double lines in the
"move the double lines"
have semantic meaning:
,
Thus, by substituting the matrices that now become
parts of the different regions of the partitioned
matrices into the appropriate parts
of the loop-invariant, we derive a predicate that indicates what
the
contents of the different submatrices must be after moving the
double lines:
becomes
.
Finally, we simplify the expression on the right of the equal sign
and place the result into the worksheet.
[
UPDATE SOURCE
]
[
VIEW
PDF
PS
]
[
BACK
]
[
NEXT
]