Program synthesis by model finding

• Embedding of the syntax and denotational semantics of a subset of IMP in Alloy*.
• Program synthesiser with and without sketches.
• Program synthesis for expressions and commands, including loops.
• Case study synthesising the Euclid's algorithm (the greatest common divisor).
• Experiments illustrating the performance of the synthesiser.

Program synthesis aims to automate the task of programming. In this paper, we present a clear and elegant formulation of program synthesis as an Alloy* specification by applying its model finder to search for a program that satisfies a contract in terms of pre and post-conditions. Our proposal embeds in Alloy* both the syntax and the denotational semantics of Winskel's IMP(erative) language. We illustrate our approach by synthesising Euclid's greatest common divisor algorithm. Our experiments show that our synthesis time is competitive. In addition, Alloy* provides us a great platform for the development of a synthesiser: an elegant synthesiser based on the denotational semantics of a language that can be implemented very quickly.