Dissertação

{en_GB=Program Synthesis with Constraint Solving for the OutSystems Language} {} APPROVED

{pt=Síntese de programas é o problema de gerar automaticamente implementações concretas de programas a partir de especificações de alto nível que definem a intenção do utilizador. OutSystems é uma plataforma low-code para desenvolvimento rápido de aplicações e integração simples com sistemas já existentes, com recurso a programação visual ou textual. Neste trabalho, focamo-nos no lado da programação textual. Abordamos o problema de sintetizar expressões OutSystems em um ambiente onde as especificações são fornecidas na forma de exemplos de entrada-saída, com foco em expressões que manipulam dados dos tipos inteiro e texto. Fazemos um estudo do estado da arte em síntese de programas e implementamos dois sintetizadores baseados em componentes e numa arquitectura de síntese inductiva guiada a oráculos. Ambos os sintetizadores aplicam uma mistura de satisfação de restrições com procura enumerativa básica, diferindo um do outro na quantidade de trabalho que colocam na fase de satisfação de restrições. Ambos os sintetizadores são aferidos e comparados com o SyPet num conjunto de problemas do mundo real fornecidos pela OutSystems, demonstrando resultados interessantes para programas até tamanho 4., en=Program synthesis is the problem of automatically generating concrete program implementations from high-level specifications that define user intent. OutSystems is a low-code platform for rapid application development, and easy integration with existing systems, featuring both visual and textual programming. In this work, we focus on the textual programming side. We tackle the problem of synthesizing OutSystems expressions in a setting where the specifications are given in the form of input-output examples, focusing on expressions that manipulate the integer and text datatypes. We survey the state of the art in program synthesis, and implement two component-based synthesizers based on an oracle-guided inductive synthesis architecture. Both synthesizers employ a mixture of constraint solving with basic enumerative search, differing from each other on the amount of work they put on the constraint solving phase. Both synthesizers are benchmarked and compared to SyPet on a set of real world problems provided by OutSystems, showing promising results for expressions of up to 4 lines in their correspondent static single assignment form.}
{pt=Síntese de Programas, Síntese Baseada em Componentes, Satisfação de Restrições, Satisfação Módulo Teorias, en=Program Synthesis, Programming by Examples, Component-Based Synthesis, Constraint Solving, Satisfiability Modulo Theories}

Junho 7, 2019, 10:30

Orientação

ORIENTADOR

Maria Inês Camarate de Campos Lynce de Faria

Departamento de Engenharia Informática (DEI)

Professor Associado

ORIENTADOR

Miguel Monteiro Ventura

OutSystems

Lead Software Engineer