The Refinement of Reversible Computations

Abstract. We consider a language which allows bounded non-determinism, stand-alone guarded commands and speculative computations as imple-mentable constructs. We give the operational interpretation of such com-mands in terms of reversible computation, and consider the implications for refinement. The Knight’s Tour is used as a motivating case study