Skip navigation
Use este identificador para citar ou linkar para este item: https://repositorio.ufpe.br/handle/123456789/20828
Título: Program synthesis from denotational semantics
Autor(es): MARANHÃO, Heitor Paceli
Palavras-chave: Síntese de programas; Alloy; Linguagens específicas de domínio
Data do documento: 13-Set-2016
Editor: Universidade Federal de Pernambuco
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.
URI: https://repositorio.ufpe.br/handle/123456789/20828
Aparece na(s) coleção(ções):Dissertações de Mestrado - Ciência da Computação

Arquivos deste item:
Arquivo Descrição TamanhoFormato 
Dissertacao_Heitor_Maranhao.pdf1,09 MBAdobe PDFVer/Abrir


Este arquivo é protegido por direitos autorais



Este item está licenciada sob uma Licença Creative Commons Creative Commons