Síntese de programas via localizador de modelo

Abstract

Uma das finalidades de Síntese de programas é mecanizar a tarefa de programar, a partir da intenção do usuário (expressa de diferentes formas como pré/pós condição, exemplos, sketches, etc). Há diversas abordagens de síntese de programas que costumam ser implementadas isoladamente: dedutiva, guiada por sintaxe, indutiva, etc. Neste trabalho, descrevemos o PSMF, como uma abordagem (implementada como um sintetizador) que combina modelo de busca e algoritmo genético. O PSMF proposto expressa a intenção do usuário em exemplos de entrada/saída (exemplos E/S), soft sketch (ou seja, um conjunto de comandos que devem aparecer no programa sintetizado, mas são escritos em qualquer ordem) e ingredientes sintáticos (quantidades de construtores sintáticos que devem aparecer no programa sintetizado). A saída gerada pelo PSMF é um programa imperativo de propósito geral. A combinação de síntese indutiva com algoritmo genético permitiu o PSMF sintetizar programas com (ou sem) arrays, totalizando 16 programas (Max2, Max3, Max4, GCD, IntSqrt, Maj5, Maj8, Modu, Fact, Fib, aMax; aDouble; aSum, eCount, aBubSort e aSelSort) bem conhecidos nas comunidades de síntese de programas (Competição SyGuS, Programação Genética). Executamos avaliações empíricas da efetividade da nova implementação e o tempo médio de síntese desses 16 programas variou de 5.0 segundos (Max2) até 15.9 minutos (Fib).