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...

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Rastislav Bodík, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, Casey Rodarmor
• Keywords: Angelic Nondeterminism, Angelic Operators, POPL 2010, Programming Languages, Refinement-based Angelic Programming