Program synthesis from denotational semantics

Abstract

Program synthesis aims to automate the task of programming. Through program synthesis it is possible to let the programmer free to care about the description (specification) of the problem to be solved by the program under development, reducing human interaction with coding tasks. Automating new algorithms creation and transferring responsibility for writing code are some of the benefits propitiated by program synthesis. In this work, program synthesis is presented as an Alloy* specification for an imperative language. We synthesize programs described by pre and post-conditions (contracts) written using a Domain Specific Language proposed in this work. We embed the syntax and the denotational semantics of Winskel’s imperative language in Alloy*. Alloy* has proven to be an easy and productive way of building program synthesizers. Our experiments show that synthesis based on Alloy* is competitive once contracts, scopes and, if needed, sketches, are correctly chosen. As a consequence, our Alloy* program synthesizer can provide, in a single high-level framework, different features in comparison to other synthesizers: (i) synthesis based on scope; (ii) synthesis based on sketches; and (iii) verification. We introduce our Domain Specific Language for contracts and present a detailed description on the synthesis of the swap problem, the product of two numbers, the maximum of 2 and of 3 numbers, and the greatest common divisor. Another contribution of this work is a source code generator, using the programming language C#, of the algorithms created by our synthesizer.