Retrenchment: Extending the Reach of Refinement

Discussion of a simple example demonstrates various expressive limitations of the refinement calculus, and suggests a liberalization of refinement, called retrenchment, which will support an analogous formal development calculus. Useful concrete system behaviour can be specified outside the domain of pure refinement, and a case is made for fluidity between I/O and state components across the development step. A syntax and a formal definition are presented for retrenchment, which has some necessary properties for a formal development calculus: transitivity gives stepwise composition of retrenchments, and monotonicity w.r.t. the specification language constructors gives piecewise construction of retrenchments. 1 Introduction and r esum e of B From early concerns about proving correctness of programs such as Hoare's [19] and Dijkstra's [15], a mature refinement calculus of specifications to programs has developed. This development has been in two strands, the predicate transformer/ lattic..