Uma imagem geral de verificação formal em software

Question

Estou tentando juntar uma imagem geral do estado de verificação formal de software, e estou tendo um bom problema. Para contexto, venho principalmente um fundo de matemática. Estou muito familiarizado com o estado dos provadores de teóricos automatizados e assistentes de prova em relação ao seu uso para provar declarações matemáticas bem formadas (por exemplo, em CoQ, Isabelle, Lean, etc.). O que estou tendo problemas para entender é o que está acontecendo com "métodos formais" em aplicações práticas CS.

Eu descobri que as empresas como a Microsoft e a AWS usaram TLA + como um "método formal" em seu desenvolvimento de software um pouco substancialmente. Mas quando comecei a ler o livro TLA + Wayne, descobri que ele considerou um programa para ser formalmente verificado se apenas verificarmos um algoritmo de classificação em listas de comprimento $ com entradas entre 1 e $ n $ para alguma fixa $ n $ , ou seja, estamos apenas verificando finitamente muitos casos e dizendo que, portanto, o algoritmo deve funcionar em geral. Isso não parece particularmente interessante; apenas um exemplo de testes de unidade particularmente rigorosos. Nomeadamente não é uma prova formal de correção.

Por outro lado, eu vi murmúrios sobre Isabelle e CoQ sendo capazes de provar coisas sobre softwares como eles podem provar os teoremas matemáticos. Embora quando olho para os livros que parecem prometer isso, por exemplo, Programação certificada com tipos dependentes , vejo muitas coisas abstratas que parecem se relacionar vagamente com formalmente verificando programas, mas não há exemplos de tomar um programa real escrito em uma linguagem que tenha uso generalizado (por exemplo, C ++ , Python, java, etc.) ou mesmo apenas pseudocódigo e "verificando-o", o que quer que isso signifique.

Alguém pode tentar esclarecer minha confusão?

Answer 1

Um programa formalmente comprovado é um programa formalmente comprovado, independentemente de qual idioma está em. Só porque um programa é escrito em COQ e talvez extraído para Ocaml ou Haskell, em vez de escrito em uma linguagem mais" da empresa ", como C ++ ou Java, não faz nada menos de um programa.

Programas de Prova escritos em linguagens de programação de uso geral, até mesmo "TAMANHAS" como Haskell, é difícil porque essas linguagens normalmente incluem muitos recursos de conveniência, cantos escuros para desempenho e interface com o sistema operacional e rico e complexo. bibliotecas. Para provar uma propriedade de um programa, você primeiro precisa declarar essa propriedade, e a instrução incorpora a semântica da linguagem que o programa está escrito. Quando você tenta formalizar os idiomas que foram inicialmente projetados sem uma semântica formal (que é quase Todos eles), você rapidamente atingiu os cantos escuros que a descrição inglesa deixa não especificada, ou onde é ambíguo, ou onde é autocontradista, ou onde a implementação de referência não faz o que a descrição diz e isso é considerado um bug em o inglês em vez da implementação. O estado da arte de provar propriedades dos programas escritos em uma linguagem preexistente é restringir os programas a um subconjunto da linguagem.

O que entra nesse subconjunto é altamente variável. O açúcar sintático não é muito difícil: a semântica só precisa traduzi-la em construções mais simples. As propriedades de reflexão não são particularmente difíceis de modelar, mas podem tornar o modelo muito mais difícil de raciocinar sobre (por exemplo, invalida propriedades como "Este snippet de código não tem nenhuma maneira de fazer referência a essa variável, portanto, não pode Altere seu valor "), muitas estruturas regem isso. Interações com o sistema operacional (normalmente via bibliotecas) são problemáticas porque exigem modelar o sistema operacional, que é extremamente complexo. As operações de ponto flutuante são difíceis, porque acompanhar as aproximações entre as operações sucessivas provoca uma explosão enorme.

para C, um dos principais subceses principais com um modelo formal é a Compcert C, a linguagem de Compcert . A Compcert é um compilador formalmente verificado (escrito em COQ), por isso, se você provar uma propriedade do programa C, você também poderá obter uma prova do código de máquina gerado. compcert c é um subconjunto muito grande de C99, mas a formalização exclui a maior parte do padrão biblioteca e algumas peculiaridades da linguagem.

Para provar um programa que é escrito em um (subconjunto adequado de uma) linguagem de programação do mundo real, o programa precisa ser estruturado de forma a tornar a prova tráfica. Na prática, isso significa ter escrito e provou o programa primeiro em uma linguagem de nível superior (que não tem implementação em hardware real), e usando essa linguagem de nível superior como uma especificação do programa final. Muitas vezes há vários níveis de refinamentos sucessivos entre o programa executável e a especificação.

É bastante comum que o programa final não seja escrito manualmente, mas extraído mecanicamente de uma linguagem de nível superior. Por exemplo, escrevendo coq que é extraído para a OCAML, ou escrita f * que é extraído para C. Mas o A abordagem oposta é possível também, por exemplo, escrevendo ("Tame") C, anotando-o com propriedades de funções e outras subdivisões de código, e usando frama-c Para provar essas propriedades (e a propriedade implícita que o programa C não tem comportamento indefinido).

Quando você tem uma semântica formal de uma linguagem de programação e uma maneira de expressar propriedades de programas, provando essas propriedades é um teorema matemático. Normalmente, esses teoremas não envolvem qualquer matemática complexa, como cálculo (a menos que seja trazido pelo domínio do aplicativo, como rastrear o movimento de um objeto físico), mas eles são difíceis de provar porque envolve fórmulas muito grandes e contêm declarações aritméticas ( $ x ^ n + y ^ n= z ^ n $ não é uma equação complexa, mas resolver não é elementar!). É teoricamente impossível escrever um programa que possa provar uma propriedade semântica não trivial de todos os programas , e praticamente impossível escrever um programa que possa provar muitas propriedades interessantes de programas típicos. A verificação formal envolve uma combinação de quebrar o problema em etapas suficientemente pequenas (escrevendo pequenas funções e indicando propriedades precisas suficientes dessas funções), ter uma ferramenta prova de algumas dessas propriedades (tal

como um Sat solver para a lógica proposicional), e ter humanos escrever provas onde o computador pode Não faça (mas o computador irá verificar a prova do humano). Os assistentes de prova, como CoQ e Isabelle, vêm para este último passo.

Provando formalmente um programa do mundo real é um enorme esforço, exigindo uma quantidade muito maior de tempo e expertise do que o projeto de software típico. Raramente é feito fora dos ambientes de alta garantia, principalmente ambientes com altos requentamentos de segurança, como transporte (aviões, trens, não tanto carros), às vezes ambientes com altos custos, como espaço ou (muito raramente), com altos requisitos de segurança, como inteligência cartões.

.

Se quisermos apenas um algoritmo de classificação em listas de comprimento

Isso não seria uma prova formal, a menos que o programa tenha um limite de n itens para sua entrada. Eu não conheço este livro, mas eu suspeito que você tenha entrado errado alguma coisa. Formalmente, verificar um programa de classificação envolveria provando sua correção para todos n.