Title
A Virtual Machine for Supporting Reversible Probabilistic Guarded Command Languages
Abstract
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.
Year
DOI
Venue
2010
10.1016/j.entcs.2010.02.005
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
formal semantics,probability,naked guarded command,reversible computing,sequential programming language,virtual machine,formal description,forth,non-deterministic choice,backtracking,reversible probabilistic guarded command,operational interpretation,probabilistic choice,execution platform,example program,formal development environment,programming language,development environment,satisfiability
Programming language,Virtual machine,Computer science,Formal development,Reversible computing,Formal description,Theoretical computer science,Probabilistic logic,Backtracking,Semantics of logic,Dijkstra's algorithm
Journal
Volume
Issue
ISSN
253
6
Electronic Notes in Theoretical Computer Science
Citations 
PageRank 
References 
10
0.56
11
Authors
3
Name
Order
Citations
PageRank
Bill Stoddart113515.69
Robert Lynas2151.03
Frank Zeyda313113.83