Authors: Lindsay Groves, Raymond G. Nickson, Mark Utting
Source: GZipped PostScript (0kb); Adobe PDF
(338kb)
This paper describes a refinement tool we are developing, with special emphasis on the use of tactics. The operation of the tool is illustrated by stepping through the derivation of a selection sort algorithm. Several aspects of the tool and its implementation are then discussed in more detail, stressing the way in which the tool assists the user in deriving programs using the refinement calculus.