Go backward to Gaussian Elimination
Go up to Top
Go forward to Program Structuring
Correctness
- invariant have same solutions.
- FP ( )
- FP ( notequal is a unit
column)
- Diagonal element is 1 and all other elements are zero.
- FP is reached:
- (,) decreases lexicographically with every state change.
- = number of unit columns in .
- = number of nonzero diagonals in .
For efficient implementation, non-determinism has to be restricted
(explicit ordering, mapping of processes, etc)
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine