ABSTRACT
The refinement calculus [6] generalizes the weakest precondition technique of Dijkstra [10] to prove the correctness of refinement steps during program construction. It is based on the weakest precondition predicate transformer semantics of the underlying programming language. All correctness reasoning is carried out within the calculus relying ultimately on the predicate transformers. However, within the calculus we can define transformation rules and base the derivation on these rules. The rules can be general purpose or targeted and domain specific. The correctness of the transformation rules is proven within the calculus. In this chapter, we will take this approach and define a small collection of transformation rules particularly suitable for derivations within the field of scientific computing.
