Program synthesis from denotational semantics

Detalhes bibliográficos
Ano de defesa: 2016
Autor(a) principal: MARANHÃO, Heitor Paceli
Orientador(a): MOTA, Alexandre Cabral
Banca de defesa: Não Informado pela instituição
Tipo de documento: Dissertação
Tipo de acesso: Acesso aberto
Idioma: eng
Instituição de defesa: Universidade Federal de Pernambuco
Programa de Pós-Graduação: Programa de Pos Graduacao em Ciencia da Computacao
Departamento: Não Informado pela instituição
País: Brasil
Palavras-chave em Português:
Link de acesso: https://repositorio.ufpe.br/handle/123456789/20828
Resumo: 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.