article · 1989
Stepwise Derivation of a Parallel Matrix Multiplication Algorithm
J. von Wright
Cited by 0Abstract and details only
Abstract
A standard multiplication algorithm for square matrices is transformed into a distributed algorithm. Every transformation step is verified within the refinement calculus. Some high-level rules of refinement that are used in the derivation are proved. 1 Introduction This report is a case study, intended to show how the refinement calculus, combined with the action system formalism gives a powerful and uniform method for constructing parallel and distributed algorithms by stepwise refinement. The refinement calculus is a formalization of the stepwise refinement approach to program construction. The refinement calculus, based on the weakest precondition technique of [Dijkstra76], was first described in [Back78, Back80] and has been further elaborated in [Back87, Back88a, Back88b, MoRoGa88, Morris87]. A statement S is said to be (correctly) refined by a statement S', denoted S S 0 , if 8 P; Q:(P [S]Q ) P [S 0 ]Q) where P [S]Q stands for the total correctness of S w.r.t. precondition...
Cite this paper
von Wright, J. (1989). Stepwise Derivation of a Parallel Matrix Multiplication Algorithm.
von Wright, J. “Stepwise Derivation of a Parallel Matrix Multiplication Algorithm.” 1989.
von Wright, J. 1989. “Stepwise Derivation of a Parallel Matrix Multiplication Algorithm.”
von Wright, J. (1989) ‘Stepwise Derivation of a Parallel Matrix Multiplication Algorithm’.
@article{vonwright1989stepwise,
title = {{Stepwise Derivation of a Parallel Matrix Multiplication Algorithm}},
author = {von Wright, J.},
year = {1989}
}Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.