Strategies for testing and formalizing properties of modern programming languages

• Ano de defesa: 2019
• Autor(a) principal: Feitosa, Samuel da Silva
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Pelotas; Centro de Desenvolvimento Tecnológico; Programa de Pós-Graduação em Computação; UFPel; Brasil
• Palavras-chave em Português: Computação; Property-based testing; Formal verification; Featherweight Java; QuickCheck; Agda; Testes baseados em propriedades; Verificação formal; CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
• Link de acesso: http://guaiaca.ufpel.edu.br/handle/prefix/6280

O mundo atual está repleto de dispositivos e máquinas controladas por software, os quais dependem de linguagens de programação e compiladores para serem produzidos e executados. A importância do desenvolvimento de software correto vai além de computadores pessoais e aplicativos de smartphones. Um erro em um sistema crítico, como em uma usina nuclear ou em um controlador de aviação, pode causar danos catastróficos em nossa sociedade. Hoje em dia, essencialmente duas técnicas de validação de software são utilizadas para evitar tais problemas: teste e verificação de software. Nesta tese, são combinadas ambas as técnicas de validação na área pesquisa de linguagens de programação, aplicando testes baseados em propriedades inicialmente para melhorar especificações e depurar programas, antes de uma tentativa de verificação formal. Por usar esta abordagem de testes, é possível eliminar falsas conjecturas rapidamente e usar os contra-exemplos gerados para corrigí-las. Então, tendo confiança de que a especificação está correta, é possível ir além, formalizando a especificação e provando propriedades em um provador de teoremas interativo, o qual usa um aparato matemático para garantir que estas propriedades são válidas para uma dada especificação. Aplicou-se diferentes estratégias para testar e formalizar duas linguagens de programação, o Cálculo Lambda, e o cálculo orientado a objetos Featherweight Java. A primeira parte desta tese define um procedimento direcionado por tipos para gerar programas aleatórios para cada linguagem de modo a aplicar testes baseados em propriedades para verificar propriedades de segurança, usando Haskell e a biblioteca QuickCheck. E, na segunda parte, foram aplicadas duas abordagens, extrínseca e intrínseca, para formalizar e provar segurança de tipos para ambas as linguagens de programação estudadas, usando a linguagem de tipos dependentes Agda, comparando as sutilezas de cada técnica. Além disso, foi demonstrado que as formalizações apresentadas podem ser estendidas para novas construções de linguagens, a partir da especificação e provas das mesmas propriedades para construções do Java 8. Acredita-se que esta combinação de testes baseados em propriedades com verificação formal pode melhorar a qualidade de software em geral e aumentar a produtividade durante o desenvolvimento de provas formais.