Deriving programs by combining and adapting refinement scripts

Although program refinement is usually presented as a top-down process, real programs are usually constructed by extending, adapting and combining existing programs. We show how this kind of program development can be performed within the refinement calculus using editable refinement scripts, which can be extended, adapted and combined in this way. Our approach is illustrated by a sequence of examples, beginning with a list insertion algorithm and culminating in a stable sorting algorithm