Dissertação
{en_GB=FOREST: An interactive multi-tree synthesizer for regular expressions} {} EVALUATED
{pt=Os formulários são um método popular para recolha de dados. O suporte para validações em tempo real que filtram dados inválidos torna-os particularmente desejáveis. Validações baseadas em expressões regulares são usadas frequentemente em formulários para evitar que os utilizadores introduzam dados no formato errado. No entanto, a escrita destas validações pode representar um desafio para alguns utilizadores. Neste documento, apresentamos FOREST, um sintetizador de expressões regulares para validação de formulários. FOREST produz uma expressão regular que corresponde ao padrão desejado para os valores de input, um conjunto de grupos de captura que permitem extrair deles mais informação, e um conjunto de condições sobre grupos de captura que garantem a validade de valores inteiros no input. O nosso método de síntese é baseado em procura enumerativa e usa Satisfazibilidade Módulo Teorias (SMT) para explorar e podar o espaço de procura. Propomos uma nova representação para a síntese de expressões regulares, multi-árvore, que induz padrões nos exemplos que usa para dividir o problema através de uma abordagem dividir para conquistar. Apresentamos ainda uma nova codificação SMT para sintetizar condições sobre capturas numa dada expressão regular. Para aumentar a confiança na expressão regular sintetizada, implementamos um modelo de interação com o utilizador com base em inputs distintivos. Avaliámos o FOREST em instâncias de validação de formulários do mundo real com base em expressões regulares. Os resultados experimentais mostram que o FOREST retorna com sucesso a expressão regular desejada em 74% das instâncias e supera o REGEL, um sintetizador de expressões regulares estado-da-arte., en=Digital forms are a popular method for collecting data. The support for real-time validations that filter invalid provided data makes them particularly desirable. Form validators based on regular expressions are often used on digital forms to prevent users from inserting data in the wrong format. However, writing these validators can pose a challenge to some users. In this document, we present FOREST, a regular expression synthesizer for digital form validations. FOREST produces a regular expression that matches the desired pattern for the input values, a set of capturing groups that extract some information from them, and a set of conditions over capturing groups that ensure the validity of integer values in the input. Our synthesis procedure is based on enumerative search and uses a Satisfiability Modulo Theories (SMT) solver to explore and prune the search space. We propose a novel representation for regular expressions synthesis, multi-tree, which induces patterns in the examples and uses them to split the problem through a divide-and-conquer approach. We also present a new SMT encoding to synthesise capture conditions for a given regular expression. To in- crease confidence in the synthesised regular expression, we implement a user interaction model based on distinguishing inputs. We evaluated FOREST on real-world form-validation instances using regular expressions. Experimental results show that FOREST successfully returns the desired regular expression in 74% of the instances and outperforms REGEL, a state-of-the-art regular expression synthesizer.}
novembro 16, 2020, 13:0
Publicação
Obra sujeita a Direitos de Autor
Orientação
ORIENTADOR
Maria Inês Camarate de Campos Lynce de Faria
Departamento de Engenharia Informática (DEI)
Professor Associado
