Programming Research Group Technical Report TR-1-92

Designing arithmetic circuits by refinement in Ruby

G Jones and Mary Sheeran (Univ. Glasgow)

January 1992, 27pp.

This paper presents in some detail the systematic derivation of a static bit-level parallel algorithm to implement multiplication of integers, that is to say one which might be implemented as an electronic circuit. The circuit is well known, but the derivation shows that its design can be seen as the consequence of decisions made (and explained) in terms of the abstract algorithm. The systematic derivation serves both as an explanation of the circuit, and as a demonstration that it is correct "by construction". We believe that the technique is applicable to a wide range of similar algorithms.

This paper was presented at Mathematics of Program Construction, Oxford, England, 29 June - 3 July 1992, and has also been published in Mathematics of Program Construction, ed. R S Bird, C C Morgan and J C P Woodcock, Springer Verlag, LNCS 669, 1993.

It is available as a 100,321 byte compressed PostScript file.