Retrenchment: Extending the Reach of Refinement

Abstract

Discusses a simple example that demonstrates various expressive limitations of the refinement calculus, and suggests a liberalization of refinement, called retrenchent, which supports 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, while monotonicity w.r.t. the specification language constructors gives piecewise construction of retrenchments.