A Virtual Machine for Supporting Reversible Probabilistic Guarded Command Languages

We describe a reversible stack based virtual machine designed as an execution platform for a sequential programming language used in a formal development environment. We revoke Dijkstra's “law of the excluded miracle” to obtain a formal description of backtracking through the use of naked guarded commands and non-deterministic choice, with an operational interpretation of the interaction between guards and choice provided by reversibility. Other constructs supported by the machine provide for the collection of all results of a search, a semantically clean “cut” which terminates a search when the accumulated results satisfy some given criteria, and forms of probabilistic choice, which we distinguish from non-deterministic choice. The paper includes a number of example programs.