Programming with angelic nondeterminism

11 years 2 months ago
Programming with angelic nondeterminism
Angelic nondeterminism can play an important role in program development. It simplifies specifications, for example in deriving programs with a refinement calculus; it is the formal basis of regular expressions; and Floyd relied on it to concisely express backtracking algorithms such as N-queens. We show that angelic nondeterminism is also useful during the development of deterministic programs. The semantics of our angelic operator are the same as Floyd's but we use it as a substitute for yet-to-be-written deterministic code; the final program is fully deterministic. The angelic operator divines a value that makes the program meet its specification, if possible. Because the operator is executable, it allows the programmer to test incomplete programs: if a program has no safe execution, it is already incorrect; if a program does have a safe execution, the execution may reveal an implementation strategy to the programmer. We introduce refinement-based angelic programming, describe...
Rastislav Bodík, Satish Chandra, Joel Galen
Added 29 Sep 2010
Updated 29 Sep 2010
Type Conference
Year 2010
Where POPL
Authors Rastislav Bodík, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, Casey Rodarmor
Comments (0)