Introducing Backward Refinement into B

Abstract

The B Method exploits a direct first-order wp predicate-transformer formulation of downward simulation to generate its proof obligations for a refinement, so B’s notion of refinement is restricted to that of forward refinement. Therefore some refinements we would intuitively recognise as valid cannot be proved so in B. While relational formulations of upward simulation abound in the refinement literature, the only predicate-transformer formulations proposed hitherto have been higher-order ones quantified over all postconditions, which cannot be conveniently exploited by the B Method. Here, we propose a new first-order predicate-transformer formulation of upward simulation suitable to be adopted by B for backward refinement.