Step 6: Determine the state of the exposed submatrices
The exposed submatrices are what will be updated. To determine
how to update them requires us to first determine what their
contents are immediately after the repartitioning that exposed
them.
The key here is to realize that the double lines in the repartitioning
have semantic meaning:
,
Thus, by substituting the exposed matrices into the appropriate parts
of the loop-invariant, we derive a predicate that indicates the
contents of the different submatrices:
becomes
.
Finally, by simplifying the expression on the right of the equal sign,
we determine the state of the submatrices of B :
[
UPDATE SOURCE
]
[
VIEW
PDF
PS
]
[
BACK
]
[
NEXT
]