A carregar...
Publicação
A Mechanized Proof of Kleene’s Theorem in Why3
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 3.62 MB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
In this dissertation we present a mathematically minded development of the correction
proof of Kleene’s theorem conversion of regular expressions into finite automata, on
the basis of equivalent expressive power. We formalise a functional implementation of
the algorithm and prove, in full detail, the soundness of its mathematical definition,
working within the Why3 framework to develop a mechanically verified implementation
of the conversion algorithm. The motivation for this work is to test the feasibility of
the deductive approach to the verification of software and pave the way to do similar
proofs in the context of a static analysis approach to (object-oriented) programming. In
particular, on the subject of behavioural types in typestate settings, whose expressiveness
stands between regular and context-free languages and, therefore, can greatly benefit
from mechanically certified implementations.
Nesta dissertação apresentamos um desenvolvimento matemático da prova de correcção da conversão de expressões regulares em autómatos finitos do teorema de Kleene, com base no seu poder expressivo equivalente. Formalizamos uma implementação funcional do algoritmo e provamos, em detalhe, a correcção da sua definição matemática. Trabalhando no framework Why3 para desenvolver uma implementação mecanicamente certificada do algoritmo de conversão. A motivação para este trabalho é testar a viabilidade da metodologia e preparar o caminho para fazer provas semelhantes no contexto de uma abordagem de análise estática na programação (orientada para objectos). Em particular, no tópico dos tipos comportamentais com typestates, cuja expressividade está entre a das linguagens regulares e livres-de-contexto. Podendo, por isso, beneficiar enormemente de implementações mecanicamente certificadas
Nesta dissertação apresentamos um desenvolvimento matemático da prova de correcção da conversão de expressões regulares em autómatos finitos do teorema de Kleene, com base no seu poder expressivo equivalente. Formalizamos uma implementação funcional do algoritmo e provamos, em detalhe, a correcção da sua definição matemática. Trabalhando no framework Why3 para desenvolver uma implementação mecanicamente certificada do algoritmo de conversão. A motivação para este trabalho é testar a viabilidade da metodologia e preparar o caminho para fazer provas semelhantes no contexto de uma abordagem de análise estática na programação (orientada para objectos). Em particular, no tópico dos tipos comportamentais com typestates, cuja expressividade está entre a das linguagens regulares e livres-de-contexto. Podendo, por isso, beneficiar enormemente de implementações mecanicamente certificadas
Descrição
Palavras-chave
Deductive verification Formal languages Automata theory Regular expressions Kleene’s theorem Why3