A Proposal for Interactive Program Generation

Programming-by-example (PBE) systems attempt to generate programs by learning a task from the user’s actions. It is a field with great potential, but little success so far. Most existing PBE systems are both highly specialised and quite limited in the tasks they can accomplish. This paper sets out a new approach to PBE that is general-purpose and can handle variables, branching and loops. It could therefore offer non-experts a genuine alternative to conventional programming. Our approach makes use of automated reasoning techniques, and is based on work in interactive theorem proving using model-instance based reasoning (where general theorems are proved by considering specific cases). The ‘proof-as-programs’ paradigm (where theorem provers are used to generate programs) leads us to propose that modelinstance based reasoning can be applied to program generation. The proposed method has the added benefit that - because of the link to an underlying logic - certain types of common bug cannot occur. We are currently working on an implementation for the domain of XML object manipulation.