Programming with Angelic Nondeterminism

TitleProgramming with Angelic Nondeterminism
Publication TypeConference Paper
Year of Publication2010
AuthorsBarman, S., Bodik R., Chandra S., Galenson J., Kimelman D., Rodarmor C., & Tung N.
Conference Name37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '10)
Date Published01/2010
Conference LocationMadrid, Spain

Angelic nondeterminism can play an important role in program de-
velopment. It simplifies specifications, for example in deriving pro-
grams with a refinement calculus; it is the formal basis of regular
expressions; and Floyd relied on it to concisely express backtrack-
ing 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 our embedding of angelic operators into Scala, report on our imple-
mentation with bounded model checking, and describe our experi-
ence with two case studies. In one of the studies, we use angelic operators to modularize the Deutsch-Schorr-Waite (DSW) algorithm.
The modularization is performed with the notion of a parasitic
stack, whose incomplete specification was instantiated for DSW
with angelic nondeterminism.

angelic-acm-dl.pdf423.22 KB