Vladimir Jojic, Sumit Gulwani, and Nebojsa Jojic
We present a novel algorithm for inferring an imperative program that satisfies examples of given input-output pairs. The algorithm can be used for automatic bug finding and correction from test examples. In addition to providing input-output pairs (which are concrete combinations of states at the beginning and the end of the program), the constraints describing program correctness can also be provided in terms of abstract state representations anywhere in the program. Our approach to solving this set of problems is to describe the program as a graph consisting of instructions and states as potentially unknown variables, connected by constraint nodes. Then, a probabilistic inference technique, known as belief propagation in the machine learning community, is used to infer both the intermediate program states and the instructions that satisfy all the constraints. To illustrate the power of the approach, we show examples of inferring imperative program fragments that execute polynomial computations and list manipulations from small sets of pairs of desired input-output combinations. In addition, we show how a buggy piece of code can be used to initialize the instructions in the graph, after which belief propagation leads to altering the code so as to satisfy the input-output constraints. We believe that the ideas discussed here have many applications in fast software development and debugging.
© 2008 Microsoft Corporation. All rights reserved.