Abraçando o poder dos métodos formais em minha jornada de codificação: Como me tornei um evangelista Dafny
NewsDevelopersEnterpriseBlockchain ExplainedEvents and ConferencesPressboletins informativos
Assine a nossa newsletter.
Endereço de email
Nós respeitamos sua privacidade
HomeBlogDevelopers
Abraçando o poder dos métodos formais em minha jornada de codificação: Como me tornei um evangelista Dafny
por ConsenSys 22 de dezembro de 2020 Postado em 22 de dezembro de 2020
Por Joanne Fuller
Quero começar dizendo que estou escrevendo esta postagem do blog na esperança de que outras pessoas possam vivenciar o momento de epifania que tive enquanto aprendia Dafny como parte da minha exploração em métodos formais. Além disso, espero que esta postagem funcione como um catalisador para que outros considerem os métodos formais uma habilidade crítica e necessária dentro do arsenal de qualquer um que escreve código. Como parte do Equipe de verificação automatizada dentro de R&D na ConsenSys, Estou usando o Dafny na verificação formal da especificação Ethereum 2 Fase 0 e quero compartilhar por que considero isso útil.
Minha experiência
Devo deixar claro que não sou um desenvolvedor de software, mas sim um programador matemático com algum conhecimento de desenvolvimento de software. Aprendi a escrever programas como parte de minha aula de matemática durante meu último ano do ensino médio e provavelmente deveria mencionar que embora gostasse bastante de usar computadores naquela época, a perspectiva de aprender a programar me assustou a ponto de quase abandonou aquela aula particular de matemática. Tendo decidido enfrentar meu medo de falhar (com relação a aprender a programar e potencialmente arruinar meu resultado nesta aula), passei a experimentar meu primeiro momento de epifania no contexto da programação. Ainda me lembro vividamente de estar sentado na aula e perceber que escrever um programa para resolver um problema de matemática não era um processo mágico e misterioso, era quase como escrever como eu resolveria um problema na minha cabeça. Não havia como voltar atrás depois disso!
A programação tem sido um aspecto importante de tudo que fiz desde então. Meu PhD em criptografia dependia muito da capacidade de desenvolver algoritmos e programar implementações otimizadas. Meus programas foram escritos para experimentação e, embora eu não tenha empreendido o que agora chamaríamos de teste formal, eu verificaria informalmente os limites e os casos de teste usando o raciocínio lógico sobre a saída pretendida. Também trabalhei por muitos anos como pesquisador de empreendimentos acadêmicos na área de finanças e economia. Novamente, isso incluiu escrever programas e, novamente, usei minhas próprias técnicas para testar informalmente e raciocinar sobre sua correção.
É justo dizer que, embora eu apreciasse o fato de que o teste sempre seria incompleto, no sentido de que era impossível testar todos os casos; que eu estava razoavelmente confiante de que minha maneira matemática de pensar era muito boa quando se tratava de testes informais de maneira rigorosa. Como tal, eu definitivamente não tinha uma avaliação completa da diferença entre testar e provar a correção, nem as consequências de tal! Durante minha carreira, antes de ingressar na ConsenSys, fiquei contente em confiar em minhas próprias técnicas informais para determinar o que eu pensava ser correção por meio de testes.
Minha formação é, portanto, parte da história, já que estou um tanto surpreso por não ter descoberto métodos formais antes. Eu me considero um matemático; Eu amo matemática, algoritmos e lógica. Agora parece loucura simplesmente confiar em testes incompletos, mas também parece loucura para qualquer um que programa não ter pelo menos uma avaliação do que os métodos formais podem oferecer e as possíveis consequências de perder um bug, dadas as muitas maneiras em que os programas de computador são integrado em nossas vidas. Os métodos formais nos permitem ir além dos testes, para provar que um programa está correto em relação a uma especificação que inclui pré e pós-condições.
Um primeiro exemplo Dafny
Como um exemplo simples, considere a divisão inteira de um dividendo não negativo n por um divisor positivo d;
WL
mostrado abaixo:
Embora em uma linguagem de programação digitada possamos restringir um pouco os parâmetros de entrada, nem sempre é suficiente. Neste exemplo, a especificação de n e d como números naturais significa que ambas as entradas devem ser números inteiros não negativos, mas não fornece a restrição de d para ser um número inteiro positivo. O uso de uma pré-condição por meio da instrução requer prevê tal restrição e significa que este método só pode ser chamado se d > 0. Portanto, se qualquer outra parte do programa fizer com que div seja chamado sem que tal pré-condição seja satisfeita, o programa não será verificado. A declaração garante, então, fornece a pós-condição e fornece uma especificação formal do que a saída do método deve satisfazer.
Este exemplo foi escrito usando o Dafny: “Um verificador de linguagem e programa para correção funcional” e me leva ao meu próximo ponto, ou seja, por que sou tão fã de Dafny. Acho que é justo dizer que, para muitos programadores, a idéia de usar “métodos formais” para verificar a exatidão do programa é um tanto assustadora e muitas vezes considerada “muito” difícil. Seja pela falta de exposição às técnicas, pela falta de valorização dos benefícios, ou mesmo pela falta de treinamento nesta área; quaisquer que sejam as razões, acredito que Dafny tem a capacidade de permitir que qualquer programador alcance rapidamente o sucesso na aplicação de métodos formais em seu trabalho. Olhando para o trecho de código acima, eu esperaria que qualquer pessoa com algum conhecimento de programação fosse capaz de ler este código Dafny; Dafny é uma linguagem amigável para o programador. Depois de aprender um pouco sobre Dafny, é muito fácil começar a experimentar e, basicamente, aprender à medida que avança. E se você estiver interessado em aprender Dafny, um ótimo lugar para começar é série de tutoriais pela Microsoft. O site também inclui um editor online, por isso é muito fácil experimentar os exemplos do tutorial. O Canal da esquina da verificação no YouTube é outra fonte de referências úteis.
Meu momento de epifania
Finalmente, eu queria compartilhar meu momento de epifania de quando estava aprendendo Dafny. Certamente já ouvi histórias sobre trechos curtos e simples de código, de grandes empresas respeitáveis, com bugs que foram perdidos e custaram muitos milhões de dólares; mas acho que só quando você se dá conta de como seria fácil criar um bug sem querer em uma função simples é que tudo faz sentido! O momento em que você diz a si mesmo “Oh, seria tão fácil cometer esse erro!”
Meu momento chegou enquanto assistia a um dos Vídeos do canto de verificação.
Neste tutorial, Rustan Leino passa por um método SumMax que pega dois inteiros, xey, e retorna a soma e max, s e m, respectivamente. Este exemplo é relativamente simples e o código Dafny é mostrado abaixo.
As entradas xey são especificadas como inteiros por meio de digitação e nenhuma outra pré-condição é necessária. As três pós-condições fornecem verificações de que a saída realmente atende às especificações, ou seja, que s é igual a x + y, e que m é igual a x ou y e que m não excede x e y. O método SumMaxBackwards é então apresentado como um exercício e é aqui que fica mais interessante. A especificação é o inverso de SumMax, ou seja, dados a soma e o máximo retornam os inteiros x e y. Ok, então uma primeira tentativa pode ser com as mesmas pós-condições; como as relações entre as entradas e saídas ainda se mantêm. Se deixarmos x ser o máximo, um pouco de álgebra nos dirá que y deve ser igual à soma menos o máximo. Colocar isso no editor online dá o seguinte.
Não verifica. Então, o que deu errado? Somos informados de que uma pós-condição não se manteve e, especificamente, a pós-condição na linha 3 (garante x<= m && y <= m) pode não se manter. Olhando mais de perto, vemos que esta condição de postagem especifica que x <= m e y <= m. Bem, sabemos que x é menor ou igual am, pois definimos x igual am, então isso significa que y <= parte m não verifica. Como isso pode acontecer? Nossa álgebra nos disse que y: = s – m. Digamos que s é 5 e m é 3, então y = 5 – 3 = 2, o que garante y <= m; mas digamos que chamemos este método com s igual a 5 e m igual a 1. Nada nos impedirá de chamar o método com esses parâmetros de entrada, mas fazer isso causará um problema, pois y = 5 – 1 = 4 e então y > m. Basicamente, o que estamos vendo aqui é que, embora o parâmetro de entrada deva ser o máximo de dois inteiros que criam a soma s, não há nada que nos impeça de tentar chamar o método com uma entrada inválida. A menos que uma pré-condição seja incluída para restringir as entradas de s e m a inteiros válidos que resultarão em saídas xey que atendam à especificação, nosso método pode produzir resultados incorretos. Que relação precisamos entre s e m para fornecer entradas válidas? Um pouco mais de álgebra nos mostra que s <= m * 2 para que haja uma solução válida de xe y. Se adicionarmos isso como uma pré-condição, Dafny agora pode verificar o código conforme mostrado abaixo.
Este foi o exemplo em que pude ver como é fácil introduzir um bug no código. Só porque chamamos os parâmetros de entrada de ‘s’ para soma e ‘m’ para máximo, não significa que o método será chamado apropriadamente e como parte de algum programa maior, pode haver muitas consequências indesejadas que decorrem disso tipo de bug. Espero que seja útil para qualquer pessoa que esteja aprendendo sobre Dafny ou métodos formais de forma mais geral.
No que estou trabalhando agora
Bem, isso me leva ao final da minha postagem. Se você gostaria de ver no que estou trabalhando atualmente com Dafny, dê uma olhada Repositório GitHub. Faço parte da equipe de verificação automatizada dentro de R&D na ConsenSys e estamos usando Dafny na verificação formal da especificação Ethereum 2 Fase 0. O uso de métodos formais no espaço do blockchain é uma área nova e estimulante de pesquisa que foi adotada pela ConsenSys e eu encorajaria qualquer pessoa interessada em aprender mais sobre a Eth 2.0 a olhar para os recursos disponíveis em nosso repositório de projetos.
Boletim informativo Assine nosso boletim informativo para obter as últimas notícias da Ethereum, soluções empresariais, recursos para desenvolvedores e muito mais. Endereço de e-mail