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