Towards Squiggly Refinement Algebra
D. A. Naumann · 1998
The algebra of functions and relations has been used so successfully in program construction that textbooks have appeared. Despite the importance of predicate transformers in imperative programming, the algebra of transformers has been less explored. To show its promise, we prove results on exponents and recursion on inductive data types, sufficient for carrying out a polytypic derivation that has been given as a substantial example for functions and relations. We also give a data refinement from exponents of specifications to the concrete exponents needed for program semantics.