In angelic programming, the programmer asks an oracle for a demonstration of an algorithm under development. He writes a program with nondeterministic choose statements, with the goal of divining values that he does not yet know how to compute. Given an input, angelic choose statements produce values that, if possible, pass all the assertions in the program. A trace of these values typically exposes the insight behind the algorithm, allowing the programmer to refine the angelic program into a desired deterministic program.
A challenge with angelic programming is that not all safe traces correspond to a plausible algorithm; some achieve a safe execution by abusing the clairvoyance of the oracle. For example, a trace may first break a data structure, only to miraculously correct it later. Clearly, we want a method for identifying (sets of) traces that correspond to a plausible algorithm.
We approach this problem by computing sets of angelic traces that can each be abstracted with a single trace. The abstraction is based on entanglement of choose statements. Intuitively, two choose statements are entangled when their values are correlated, i.e., if you change one, you may have to change the other in order to meet the specification. The abstract trace exposes entangled angels and thus often also the logic behind the algorithm in these traces.
In general, correlation of angels can be a complex relation. We approximate entanglement as an equivalence relation, which allows us to represent entanglement as simple partitioning of angels. We also introduce a two-lattice structure that relates partitions of angels to sets of traces. We develop useful queries on this structure and design efficient algorithms for computing this structure on demand. Finally, we show on several case studies that entanglement helps identify algorithms in angelic programs.
By: Shaon Barman; Rastislav Bodík; Satish Chandra; Emina Torlak
Published in: RC25023 in 2010
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .