Proof rules for both directly and indirectly indexed data-parallel array assignment are presented. Consequently, the correctness of two programs, (i) a representation of Cannon’s algorithm and (ii) sparse matrix-vector multiplication, are established by application of the rules.
Author and article information
Department of Computer Science, The Queen's University of Belfast
Belfast BT7 1NN