No Software Engineering Stack Exchange, vi a seguinte pergunta : "O que está impedindo a ampla adoção de métodos formais?" A pergunta foi encerrada como tendenciosa, e a maioria das respostas foram comentários como "Muito caro !!!" ou "Um site não é um avião !!!" De certa forma, isso é verdade, mas não explica muito. Eu escrevi este artigo para fornecer uma imagem histórica mais ampla dos métodos formais (FM), por que eles não são realmente usados e o que estamos fazendo para corrigir a situação.

Antes de começar, você precisa formular algumas condições. De fato, não existem muitos métodos formais: apenas alguns pequenos grupos . Isso significa que grupos diferentes usam os termos de maneira diferente. Em termos gerais, existem dois grupos de métodos formais: a especificação formal estuda a redação de especificações precisas e inequívocas e a verificação formal estuda os métodos de prova. Isso inclui sistemas de código e abstratos. Não apenas usamos termos diferentes para código e sistemas, como também usamos ferramentas diferentes para verificá-los. Para tornar as coisas ainda mais confusas, se alguém diz que está criando uma especificação formal, isso geralmente significa verificação de design. E se alguém disser que está fazendo verificação formal, isso geralmente se refere à verificação de código.

Para maior clareza, dividimos a verificação de verificação de código (CV) e a verificação de design (DV) e da mesma forma dividimos as especificações em CS e DS. Tais termos não são comumente usados na ampla comunidade de FM. Vamos começar com CS e CV, depois passar para DS e DV.

Além disso, a verificação parcial é possível, onde apenas um subconjunto da especificação é verificado ou a verificação completa . Essa pode ser a diferença entre as evidências das alegações de que "o sistema nunca falha e não aceita a senha errada" ou "o sistema nunca falha e bloqueia a conta se você digitar a senha errada três vezes". Basicamente, assumiremos que estamos fazendo uma verificação completa.

Você também deve esclarecer o tipo de software que estamos formalizando. A maioria das pessoas identifica implicitamente programas altamente confiáveis , como dispositivos médicos e aviões. As pessoas assumem que os métodos formais são amplamente utilizados, mas não são necessários para o resto. Isso é otimista demais: o software mais confiável não usa métodos formais. Em vez disso, focaremos no software "regular".

Finalmente, o aviso: não sou um historiador profissional e, embora tenha tentado verificar cuidadosamente as informações, pode haver erros no artigo. Além disso, sou especialista em especificações formais (DS e DV), para que haja mais chances de erro quando falo sobre verificação de código. Se você vir, escreva para mim, vou corrigi-lo (e mais uma coisa: ganho dinheiro com seminários sobre TLA + e Alloy, portanto, sou muito tendencioso em relação a esses idiomas; tento ser o mais objetivo possível, mas você entende: viés é preconceito).

Programação formal

Obtendo especificação

Antes de provar a exatidão do código, você precisa obter o padrão da verdade. Isso significa alguma especificação do que o código deve fazer. Devemos ter certeza de que o resultado corresponde à especificação. Não basta dizer que a lista está "classificada": não sabemos o que estamos classificando, quais critérios usamos e até mesmo o que queremos dizer com "classificação". Em vez disso, podemos dizer: "A lista de números inteiros l classificada em ordem crescente para quaisquer dois índices iej, se i < j , então l[i] <= l[j] ".

As especificações de código são divididas em três tipos principais:

O primeiro é escrever instruções independentes de código. Escrevemos nossa função de classificação e, em um arquivo separado, escrevemos o teorema “isto retorna listas ordenadas”. Essa é a forma mais antiga de especificação, mas Isabelle e ACL2 ainda funcionam dessa maneira (o ML foi inventado especificamente para ajudar a escrever essas especificações).
O segundo implementa especificações no código na forma de pré e pós-condições, instruções e invariantes. Você pode adicionar uma pós-condição à função que "o valor retornado é uma lista classificada". As especificações baseadas em declarações foram formalizadas inicialmente como a lógica de Hoar . Eles apareceram pela primeira vez na linguagem de programação Euclid no início dos anos 1970 (não está claro quem começou a usá-los: Euclid ou SPV , mas, tanto quanto eu sei, o Euclid já havia sido apresentado ao público antes). Esse estilo também é chamado de programação de contratos - a forma mais popular de verificação na indústria moderna (aqui, os contratos são usados como especificações de código).
Finalmente, existem sistemas de tipos. Pela correspondência de Curry-Howard, qualquer teorema ou prova matemática pode ser codificado como um tipo dependente. Definiremos o tipo de lista classificada e declararemos o tipo [Int] -> Sorted [Int] para a função.

No Let's Prove Leftpad, você pode ver como fica. HOL4 e Isabelle são bons exemplos das especificações do "teorema independente", SPARK e Dafny são as especificações da "declaração aninhada" e Coq e Agda são o "tipo dependente".

Se você observar atentamente, essas três formas de especificação de código são comparadas com as três principais áreas de validação automática: testes, contratos e tipos. Isto não é uma coincidência. A correção é uma ampla variedade e a verificação formal é um de seus extremos. À medida que o rigor (e o esforço) da verificação diminui, obtemos verificações mais simples e mais restritas, seja limitando o espaço de estados em estudo, usando tipos mais fracos ou forçando a verificação em tempo de execução. Então, qualquer meio de especificação completa se transforma em meio de especificação parcial e vice-versa: muitos consideram a sala limpa uma técnica de verificação formal, onde uma revisão de código vai muito além das capacidades humanas.

Quais especificações estão corretas?

A verificação verifica se o código está em conformidade com a especificação. Surge a pergunta: como sabemos que temos a especificação correta? Encontrar a especificação certa é um dos maiores problemas nos métodos formais. Essa também é uma das principais objeções a eles. Mas os céticos aqui não significam exatamente o que os especialistas formais têm em mente.

Quando pessoas de fora perguntam: "Como você obtém as especificações corretas?" Eles geralmente pensam em validação , ou seja, especificações que não atendem aos requisitos do cliente. Se você provar formalmente que seu código classifica a lista, e o cliente realmente deseja o Uber para sopas (tm), você gasta muito tempo. Assim, apenas iterações rápidas e curtos loops de feedback podem confirmar seus requisitos.

É verdade que a verificação de código não a valida. Mas há dois problemas com esse argumento. A primeira é que o estágio de aplicação de métodos formais é simplesmente adiado, mas não desaparece completamente. Depois de todas essas iterações rápidas, você provavelmente já tem uma idéia do que o cliente deseja. E então você começa a verificação do código. Em segundo lugar, embora não saibamos exatamente o que o cliente deseja, podemos assumir o que ele definitivamente não quer. Por exemplo, para travar acidentalmente o software. Eles não precisam de brechas de segurança. Todo mundo concorda com isso: no final, ninguém diz que você precisa pular testes de unidade durante as iterações. Portanto, pelo menos, verifique se o seu sistema de controle de versão não exclui dados aleatórios do usuário (nota: não pense que estou amargurado ou algo parecido).

O problema de encontrar a especificação correta é mais fundamental: geralmente não sabemos o que escrever lá . Pensamos em nossos requisitos em termos humanos, não matemáticos. Se eu disser: "O programa deve distinguir árvores de pássaros", então o que é isso? Eu posso explicar para uma pessoa mostrando um monte de fotos de árvores e pássaros, mas esses são apenas exemplos concretos, não uma descrição da idéia . De fato, para traduzir isso em uma especificação formal, é necessário formalizar conceitos humanos, e isso é um problema sério.

Não me interpretem mal. As especificações relevantes podem ser definidas aqui, e especialistas fazem isso o tempo todo. Mas escrever as especificações apropriadas é uma habilidade que precisa ser desenvolvida, bem como habilidades de programação. É por isso que muitos dos sucessos recentes da verificação de código são explicados por um mapeamento claro do que queremos e do que podemos expressar. Por exemplo, CompCert é um compilador formalmente verificado em C. A especificação para isso é: “Evitar erros de compilação”.

Mas tudo isso não tem nada a ver com verificação. Quando você tem uma especificação, ainda precisa provar que o código corresponde a ela.

Prova de especificação

A primeira ferramenta de verificação de código de todos os tempos é o método “pense sobre por que isso é verdade”, no estilo Dijkstra, principalmente para o ALGOL. Por exemplo, eu posso "provar" a correção da classificação pelo método insert da seguinte maneira:

A opção básica : se você adicionar um elemento à lista vazia, ele será o único elemento e, portanto, será classificado.
Se tivermos uma lista classificada com elementos k e adicionarmos um elemento, inseriremos o elemento para que ele fique depois de todos os números menores e antes de todos os números maiores. Isso significa que a lista ainda está classificada.
Por indução, a classificação por inserção classificará a lista inteira.

Obviamente, na realidade, a prova parecerá mais rigorosa, mas essa é uma ideia geral. Dijkstra e outros usaram esse estilo para provar a correção de muitos algoritmos, incluindo muitos dos conceitos básicos de simultaneidade. Este também é o estilo ao qual as palavras de Knuth estão associadas: "Cuidado com os erros neste código; Só provei que estava correto, mas não o iniciei. " Você pode arruinar facilmente uma prova matemática para que ninguém perceba. Segundo algumas estimativas , aproximadamente 20% da evidência matemática publicada contém erros. Peter Guttmann tem um excelente ensaio sobre as evidências da integridade de um programa ridículo, em que toneladas de código "testado" caem imediatamente se você os executar.

Ao mesmo tempo, estudamos maneiras de provar automaticamente teoremas matemáticos. O primeiro programa para provar os teoremas foi publicado em 1967 . No início da década de 1970, esses programas começaram a ser usados para testar o código Pascal e, no meio da década, apareceram linguagens formais especiais. O programador formula algumas propriedades do código e cria uma prova verificável de que o código tem essas propriedades. Os primeiros programas para provar teoremas simplesmente ajudaram as pessoas a verificar as provas, enquanto ferramentas mais sofisticadas poderiam provar independentemente partes do teorema.

O que leva ao seguinte problema.

É difícil obter evidências

A evidência é difícil e é um trabalho muito desagradável. É difícil parar de programar e ir ao circo. Surpreendentemente, as provas formais de código são muitas vezes mais rigorosas que as escritas pela maioria dos matemáticos! A matemática é uma atividade muito criativa, onde a resposta ao teorema é válida apenas se você o mostrar. Criatividade vai mal com formalismo e computadores.

Pegue o mesmo exemplo de classificação de inserção em que aplicamos a indução. Qualquer matemático entenderá imediatamente o que é a indução, como funciona em geral e como funciona neste caso. Mas no programa para provar os teoremas tudo precisa ser estritamente formalizado. O mesmo se aplica à prova por contradição, prova por contraposição, etc. Além disso, todas as suposições devem ser formalizadas, mesmo aquelas em que a maioria dos matemáticos não se preocupa com a prova. Por exemplo, a + (b + c) = (a + b) + c . O programa de verificação de teoremas a priori não sabe que isso é verdade. Você tem que provar isso (difícil) ou declará-lo como verdade de acordo com a lei associativa de adição (perigosa), ou comprar uma biblioteca de teoremas de alguém que já foi capaz de provar isso (caro). Os primeiros programas de prova de teoremas competiam no número de táticas de prova integradas e bibliotecas de teoremas relacionadas. Um dos primeiros programas SPADE difundidos apresentou a biblioteca aritmética completa como a principal vantagem.

Em seguida, você precisa obter a prova em si. Você pode confiar isso ao programa ou escrever você mesmo. Normalmente, a definição automática de evidência não é decidível. Para casos extremamente estreitos, como lógica proposicional ou verificação de tipo HM, é "apenas" NP-completo. De fato, nós mesmos escrevemos a maioria das evidências e o computador verifica sua exatidão. Isso significa que você precisa saber bem:

matemática
ciência da computação;
a área em que você trabalha: compiladores, hardware, etc;
as nuances do seu programa e especialização;
as nuances do programa para provar os teoremas que você usa, o que por si só é uma especialidade inteira.

Pior, paus específicos para computadores são colocados nas rodas. Lembre-se, eu disse que era perigoso assumir uma lei associativa de adição? Alguns idiomas não cumprem. Por exemplo, em C ++ INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. ((-1) + INT_MAX) + 1 é INT_MAX. -1 + (INT_MAX + 1) INT_MAX. -1 + (INT_MAX + 1) , que é indetectável. Assumindo a adição associativa em C ++, sua prova estará incorreta e o código será quebrado. Você deve evitar essa declaração ou provar que nunca haverá transbordamento para seu fragmento específico.

Você pode dizer que a adição indefinida é um erro, mas você precisa usar um idioma com números inteiros não relacionados. Mas a maioria dos idiomas possui recursos específicos que interferem nas evidências. Pegue o seguinte código:

 a = true; b = false; f(a); assert a;

Esse é sempre o caso? Não é um fato. Talvez f mude a . Talvez isso mude o fluxo paralelo. Talvez b atribuído um alias a , portanto, alterá-lo também mudará a (nota: aliases tornam tão difícil escrever evidências de que John C. Reynolds teve que criar uma lógica de separação completamente nova para lidar com esse problema). Se algo assim for possível no seu idioma, você deve provar claramente que isso não acontece aqui. O código limpo ajudará aqui, em outro caso, ele pode destruir a prova, porque força você a usar a recursão e funções de ordem superior. A propósito, ambos são a base para escrever bons programas funcionais. O que é bom para a programação é ruim para a prova! (Nota: nesta palestra, Edmund Clark listou algumas propriedades difíceis de verificar: “pontos flutuantes, seqüências de caracteres, tipos definidos pelo usuário, procedimentos, simultaneidade, modelos universais, armazenamento, bibliotecas ...”).

Os verificadores formais têm um dilema: quanto mais expressiva a linguagem, mais difícil é provar algo. Mas quanto menos expressiva a linguagem, mais difícil é escrever nela. As primeiras linguagens formais de trabalho eram subconjuntos muito limitados de idiomas mais expressivos: ACL2 era um subconjunto do Lisp, Euclid era um subconjunto do Pascal etc. E nada do que discutimos até agora prova programas reais, são apenas tentativas de abordagem. para escrever provas.

A evidência é difícil. Mas está ficando mais fácil. Os pesquisadores desse campo acrescentam novas heurísticas, bibliotecas de teoremas, componentes pré-testados, etc. O progresso técnico também ajuda: quanto mais rápido os computadores, mais rápida a pesquisa.

Revolução SMT

Uma das inovações em meados da década de 2000 foi a inclusão de solucionadores de SMT em programas para provar teoremas. Em termos gerais, um solucionador SMT pode transformar (alguns) teoremas matemáticos em problemas de conformidade com restrições. Isso transforma uma tarefa criativa em uma computacional. Talvez você ainda precise fornecer problemas intermediários (lemas) como etapas no teorema, mas isso é melhor do que provar tudo você mesmo. Os primeiros solucionadores de SMT apareceram por volta de 2004, primeiro como projetos acadêmicos. Alguns anos depois, a Microsoft Research lançou o Z3, um solucionador SMT pronto para uso. A grande vantagem do Z3 foi que ele se tornou muito mais conveniente do que outros SMTs, que, francamente, não disseram quase nada. A Microsoft Research o utilizou internamente para ajudar a provar as propriedades do kernel do Windows, para que não se limitassem ao UX mínimo.

O SMT atingiu a comunidade de FM por baixo do fôlego porque, de repente, fez muitas evidências simples triviais e permitiu que ele abordasse problemas muito complexos. Assim, as pessoas podiam trabalhar em linguagens mais expressivas, já que agora os problemas das declarações expressivas começaram a ser resolvidos. Um progresso incrível é evidente no projeto IronFleet : usando os melhores solucionadores de SMT e uma linguagem de verificação avançada, a Microsoft conseguiu escrever 5.000 linhas de código Dafny comprovado em apenas 3,7 homens-ano! Este é um ritmo incrivelmente rápido: até quatro linhas inteiras por dia (nota: o registro anterior pertencia ao seL4 , cujos desenvolvedores escreviam duas linhas por dia em C.

A evidência é difícil.

Por que isso é necessário?

É hora de dar um passo atrás e perguntar: "Qual é o objetivo?" Estamos tentando provar que algum programa atende a alguma especificação. A correção é um intervalo. Há duas partes na verificação: quão objetivamente "correto" é o seu programa e com que cuidado você verificou a exatidão. Obviamente, quanto mais verificado, melhor, mas a verificação vale tempo e dinheiro. Se tivermos várias restrições (desempenho, tempo de colocação no mercado, custo, etc.), uma validação completa não é necessariamente a melhor opção. Em seguida, surge a pergunta: qual é a verificação mínima de que precisamos e quanto custa. Na maioria dos casos, por exemplo, 90% ou 95% ou 99% de correção é suficiente para você. Talvez você deva gastar algum tempo melhorando a interface, em vez de verificar os 1% restantes?

Em seguida, a pergunta: "Um cheque de 90/95/99% é muito mais barato que 100%?" A resposta é sim. É bastante confortável dizer que a base de código, que testamos e digitamos bem, está basicamente correta, exceto por algumas correções na produção, e até escrevemos mais de quatro linhas de código por dia. De fato, a grande maioria das falhas em sistemas distribuídos poderia ter sido evitada com testes um pouco mais abrangentes. E é apenas uma extensão dos testes, para não mencionar distorções, testes baseados em propriedades ou testes de modelos. Você pode obter um resultado verdadeiramente notável com esses truques simples sem precisar obter a prova completa.

E se a digitação e o teste não fornecerem verificação suficiente? Ainda é muito mais fácil alternar de 90% para 99% do que de 99% para 100%. Como mencionado anteriormente, o Cleanroom é uma prática do desenvolvedor que inclui documentação abrangente, análise completa do fluxo e extensas revisões de código. Nenhuma evidência, nenhuma verificação formal, nem mesmo testes de unidade. Mas uma Sala Limpa adequadamente organizada reduz a densidade de defeitos para menos de 1 bug por 1000 linhas de código na produção (nota: números do estudo Stavley em Toward Zero-Deect Programming > mas sempre seja cético e verifique a fonte ). A programação de salas limpas não diminui o ritmo do desenvolvimento e certamente ultrapassa 4 linhas por dia. E a própria sala limpa é apenas um dos muitos métodos de desenvolvimento de software altamente confiáveis que estão entre o desenvolvimento usual e a verificação de código. Você não precisa de verificação completa para escrever um bom software ou até quase perfeito. Há momentos em que é necessário, mas para a maioria das indústrias é um desperdício de dinheiro.

No entanto, isso não significa que os métodos formais geralmente não sejam econômicos. Muitos dos métodos altamente confiáveis mencionados acima são baseados em especificações de código de escrita que você não prova formalmente. Em termos de verificação, existem duas maneiras comuns pelas quais o setor se beneficia. Primeiro, verifique a verificação em vez do código, que discutiremos mais adiante. Em segundo lugar, uma verificação parcial do código, que consideraremos agora.

Verificação parcial do código

Para tarefas diárias, é muito caro fazer uma verificação completa. Que tal parcial? Afinal, você pode se beneficiar da prova de algumas propriedades de fragmentos de código individuais. Em vez de provar que minha função sempre classifica os números corretamente, posso pelo menos provar que ela não se repete para sempre e nunca sai da faixa. Esta também é uma informação muito útil. Portanto, mesmo a evidência mais simples dos programas C é uma ótima maneira de eliminar uma grande parte do comportamento indefinido .

O problema é a acessibilidade .A maioria dos idiomas é projetada para verificação completa ou não é compatível com isso. No primeiro caso, você perde muitos recursos bons de linguagens mais expressivas e, no segundo caso, precisa de uma maneira de provar as coisas em uma linguagem hostil ao próprio conceito. Por esse motivo, a maioria dos estudos sobre verificação parcial se concentra em várias linguagens de alta prioridade, como C e Java. Muitos trabalham com subconjuntos limitados de idiomas. Por exemplo, SPARK é um subconjunto limitado do Ada, para que você possa escrever um código crítico do SPARK e interagir com um código Ada menos crítico. Mas a maioria desses idiomas é bastante nicho.

Com mais freqüência, certos tipos de verificação são incorporados na estrutura básica dos idiomas. Os sistemas de tipificação usados na produção são uma variante comum: você pode não saber que a cauda sempre retorna a cauda, mas sabe exatamente qual é o seu tipo [a] -> [a]. Existem também exemplos como Rust, com segurança de memória comprovada, e Pony, com prova de segurança, com exceções. Eles são um pouco diferentes de SPARK e Frama-C, na medida em que só podem executar verificações parciais. E eles geralmente são desenvolvidos por especialistas em linguagens de programação, e não especialistas em métodos formais: há muito em comum entre as duas disciplinas, mas não são idênticos. Talvez por isso, linguagens como Rust e Haskell são realmente adequadas para uso prático.

Especificação de projeto

Até agora, falamos apenas sobre a verificação de código. No entanto, os métodos formais têm outro lado, que é mais abstrato e verifica o design em si, a arquitetura do projeto. Essa análise é tão profunda que é sinônimo de uma especificação formal : se alguém diz que está cumprindo uma especificação formal, provavelmente significa que ele define e verifica o design.

Como já dissemos, provar todas as linhas de código é muito, muito difícil. Mas muitos problemas na produção surgem não por causa do código, mas por causa da interação dos componentes do sistema. Se ignorarmos os detalhes da implementação, por exemplo, considerarmos que o sistema é capaz de reconhecer pássaros, será mais fácil analisar como as árvores e os pássaros se encaixam no design geral como módulos de alto nível. Nessa escala, fica muito mais fácil descrever coisas que você não conseguia entender, como um ambiente de tempo de execução, interações humanas ou um fluxo de tempo impiedoso . Nesta escala, formalizamos nossas intenções usando um sistema comum, em vez de linhas de código. Isso é muito mais próximo do nível humano, onde projetos e requisitos podem ser muito mais ambíguos do que no nível do código.

Por exemplo, vamos seguir um procedimento com uma especificação aproximada “se for chamado, ele faz uma chamada do sistema para salvar dados no repositório e processa erros do sistema”. As propriedades são difíceis de verificar, mas é bastante claro como fazer isso. Os dados estão serializados corretamente? Nossas garantias são violadas devido a informações incorretas? Estamos lidando com todas as formas possíveis de uma falha de chamada do sistema? Agora compare o sistema de registro de alto nível com a especificação "todas as mensagens são registradas" e responda às seguintes perguntas:

Todas as mensagens são gravadas ou todas as mensagens que entram no sistema ? As mensagens são gravadas uma vez ou garantidas uma vez?
Como as mensagens são enviadas? Essa é a vez? O canal os entrega apenas uma vez? Está tudo bem com a entrega?
? , ? «» , ?
, ? ?
? « » ?
GDPR?
.

Sem um design formal, é mais difícil expressar os requisitos realmente necessários para o sistema. Se você não pode expressá-los, não tem idéia se o design realmente atende aos requisitos ou se parece com eles, mas pode levar a consequências imprevisíveis. Ao expressar formalmente intenções e design, podemos facilmente verificar se estamos realmente desenvolvendo o que precisamos.

Assim como usamos linguagens de programação para representar código, usamos linguagens de especificação para representar projetos. Os idiomas de especificação geralmente são orientados para especificações de design, e não para especificações de código, embora alguns idiomas possam ser usados nos dois casos (observação: o processo de correspondência das especificações de design com as especificações de código é chamado de refinamentoNo futuro, chamarei linguagens de especificação (DL) para minimizar as confusões (novamente, essa não é uma terminologia comum; a maioria das pessoas usa a "linguagem de especificação", mas quero distinguir claramente entre as especificações de código e as especificações de design).

Provavelmente, o primeiro DL completo foi o VDM por volta de 1972. Desde então, vimos uma enorme variedade de diferentes linguagens de especificação. O espaço DL é muito mais diversificado e fragmentado do que com as linguagens de verificação de código (CVL). Grosso modo, as pessoas inventaram o DL como um meio para atingir um fim, e o CVL como um objetivo em si. Como eles são fortemente influenciados por áreas problemáticas específicas, o DL implementa todos os tipos de idéias e semânticas. Aqui está uma visão geral muito, muito breve de alguns dos primeiros DLs:

Linguagem	Área de modelagem	Meios
Z	requisitos de negócios	álgebra relacional
Promela		CSP
SDL		-

Como as DLs geralmente são criadas para resolver problemas específicos, a maioria delas possui pelo menos dois ou três aplicativos reais. Como regra, os resultados são muito positivos. Os profissionais dizem que o DL fornece uma compreensão dos problemas e facilita a localização de soluções. Por um longo tempo, o principal campeão foi Praxis (agora Altran), que aplicou o “reparo por projeto” - uma combinação de construções em Z e código SPARK - para criar sistemas críticos de segurança. As especificações economizam tempo e dinheiro porque você não encontrará erros de design na fase final do projeto.

Pamela Zave experimentou o Alloy e descobriu um bug fundamental no Chord, uma das principais tabelas de hash distribuídas. AWS começa a encontrar erros críticos de 35 etapasescrevendo especificações TLA +. Na minha experiência, quando as pessoas tentam escrever especificações, elas logo se tornam grandes fãs desse negócio.

Mas os fãs de métodos formais e pessoas de fora avaliam de maneira completamente diferente o valor das especificações de redação. Para os fãs, a maior vantagem é que o próprio processo de design faz você entender o que está escrevendo. Quando você precisa expressar formalmente o que seu sistema está fazendo, muitos erros implícitos se tornam repentinamente óbvios. Pessoas de fora não conseguem entender isso. Se você quiser experimentar alguém com um DL, uma pessoa deve ter uma maneira de verificar se o design realmente possui as propriedades que deseja.

Felizmente, isso também é extremamente importante para muitos especificadores; portanto, a verificação do projeto é uma grande área de pesquisa.

Verificação do modelo

Como no código, podemos verificar o design escrevendo teoremas. Felizmente, temos mais um truque: você pode usar o programa de verificação de modelos. Em vez de compilar evidências de que o design está correto, simplesmente forçamos o espaço dos possíveis estados e vemos se o estado errado existe nele. Se não encontrarmos nada, tudo está bem (nota: os programas de verificação de modelo também são usados para verificar o código, como o JMBC, mas a verificação de modelo é muito mais usada na verificação de design do que na verificação de código).

A validação do modelo tem muitas vantagens. Em primeiro lugar, não há necessidade de escrever evidências, o que economiza muito tempo e esforço. Em segundo lugar, não há necessidade de aprenderescreva evidências, para que a barreira de entrada seja muito menor. Terceiro, se o design for quebrado, a verificação do modelo dará um contra-exemplo explícito. Isso torna muito, muito mais fácil corrigir o erro, especialmente se forem necessárias 35 etapas para reproduzi-lo. Tente encontrar você mesmo.

Existem algumas desvantagens. Primeiro de tudo, essas ferramentas não são tão poderosas. Em particular, você pode encontrar um número ilimitado de(ilimitado) por um modelo que possui um número infinito de estados diferentes. Por exemplo, você define um manipulador de fila de mensagens: ele normalmente funciona com uma lista de dez mensagens. Mas se você precisa acreditar em qualquer lista ... bem, há um número infinito deles, então o modelo tem um número infinito de estados. A maioria das ferramentas de validação de modelo possui truques diferentes para essas situações, como a definição de classes de equivalência ou simetria, mas cada caso é diferente.

Outra grande desvantagem - a explosão no espaço de estados (explosão em espaço de estado). Imagine que você tem três processos, cada um dos quais consiste em quatro etapas consecutivas, e eles podem alternar as etapas de qualquer maneira. Se eles não afetam o comportamento um do outro, acontece que(4*3)! / (4!)^3 = 34 650possíveis execuções (comportamentos). Se cada processo tiver um dos cinco estados iniciais, o número total de comportamentos aumentará para 4.300.000.E a verificação dos modelos deve garantir que todos se comportem bem. E isso é fornecido, pois eles não interagem entre si! Se eles começarem a fazer isso, o espaço de estados crescerá ainda mais rápido. Uma explosão combinatória é considerada o principal problema para testar modelos, e ainda resta muito trabalho para resolver esse problema.

Mas, ao mesmo tempo, há outra maneira de lidar com a explosão do espaço estadual: jogar mais equipamentos nele. O maior problema para verificar o modelo é "apenas" o problema de desempenho, e resolvemos os problemas de desempenho muito bem. A maioria das verificações de modelo (mas não todas) é facilmente paralelizada. Após otimizar o modelo e testá-lo com pequenos parâmetros, você pode implantar o cluster da AWS e executá-lo com grandes parâmetros.

Na prática, muitos qualificadores usam validação de modelo e, quando necessário, mudam para programas para provar teoremas (nota: lembre-se de que “muitos qualificadores” são cerca de dez). Ainda mais compiladores de especificações começam a testar modelos e, quando atingem o limite de seus recursos, eles alternam para formas menos intensivas de verificação.

Problema de especificação de projeto

Portanto, a verificação do projeto é mais simples e rápida que a verificação do código e demonstrou muitos sucessos impressionantes. Então, por que as pessoas não usam? O problema com DV é muito mais insidioso. A verificação de código é um problema técnico e a verificação de design é um problema social: as pessoas simplesmente não entendem o ponto.

Isso se deve em grande parte ao fato de o design não ser um código . Na maioria das DLs, não existe uma maneira automática de criar código, nem existe uma maneira de pegar o código existente e compará-lo com o design (observação: a geração de código a partir das especificações é chamada de síntese ; para orientação, veja o trabalho de Nadya Polikarpova ; prova de que o código atende à especificação (ou especificação corresponde a outra especificação) é chamadoesclarecimento : a pesquisa ativa está sendo realizada nas duas direções).

Os programadores tendem a desconfiar de artefatos de software que não são código ou não são forçados a sincronizar com o código. Pelo mesmo motivo, documentação, comentários, gráficos, wikis e confirmações são frequentemente ignoradas.

Parece que os programadores simplesmente não acreditam que as especificações sejam úteis. Na minha experiência, eles sugerem que as ferramentas atuais (pseudo-código, diagramas, TDD) são mais que suficientes para o design adequado. Não sei o quão difundida é essa opinião e não posso explicá-la com outra coisa senão conservadorismo geral.

Mas exatamente toda comunidade de metodologia tem reclamações que eu conheço: os apoiadores do TDD reclamam que os programadores não querem experimentar o TDD, os fãs de Haskell reclamam que os programadores não pensam em tipagem estática e assim por diante.

Ouvi o argumento de que o Agile não aceita um design pré-projetado; portanto, ninguém deseja fazer uma especificação formal. Talvez. Mas muitas das pessoas que conheci rejeitam o Agile e o FM. Outro argumento é que os métodos historicamente formais eram constantemente reavaliados e não cumpriam o prometido. Isso também é possível, mas a maioria das pessoas nem sequer ouviu falar sobre métodos formais, e mais ainda sobre sua história.

É simplesmente muito difícil fazer as pessoas se preocuparem com o que ainda não estão fazendo, mesmo que reconheçam os benefícios.

Sumário

Verificar o código é uma tarefa difícil. Mais e mais pessoas estão se envolvendo, embora os programas de prova de teoremas e os solucionadores de SMT estejam se tornando mais complexos. Mas ainda assim, no futuro próximo, provavelmente, isso continuará sendo um monte de especialistas.

A verificação do projeto é muito mais simples, mas seu uso requer a superação da barreira cultural. Eu acho que a situação pode ser mudada. Vinte anos atrás, testes automatizados e revisões de código eram tópicos bastante exóticos e de nicho, mas acabaram se tornando populares. Novamente, a programação de contratos era um nicho e continua sendo.

Espero que este artigo explique um pouco melhor por que os métodos formais são tão raramente usados. Pelo menos essa é uma explicação melhor do que o argumento usual "a web não é um avião". Sinta-se à vontade para gritar se vir algum erro óbvio.

Por que as pessoas não usam métodos formais?