A design-based model of reversible computation

We investigate, within the UTP framework of Hoare He Designs, the effect of seeing computation as an essentially reversible process. We describe the theoretical link between reversibility and the minimum power requirements of a computation, and we review Zuliani's work on Reversible Probabilistic Guarded Command Language. We propose an alternative formalisation of reversible computing which accommodates backtracking. To obtain a basic backtracking language able to search for a single result we exploit the already recognised properties of nondeterministic choice, using it as provisional choice rather than implementor's choice. We add a "prospective values" formalism which can describe programs that return all the possible results of a search, and we show how to formally describe the premature termination of such a search, a mechanism analogous to the "cut" of Prolog. An appendix describes some aspects of the wp calculus in terms of Designs, as needed for our proofs. Support for the programming structures described has been incorporated in a reversible virtual machine for i386 platforms with Posix compatibility.