Via Sintética e Via Analítica
A maioria de nós, incluindo outros pesquisadores de projetos de verificação formal, confiamos na forma “analítica” de verificação do programa. Ou seja, programa primeiro, verificação depois. Porém, usar esta forma significa escrever um programa em uma determinada linguagem e depois verificar se o programa atende à especificação que desejamos; a linguagem de programação não tem restrições quanto aos seus programas que podem ocorrer em relação à especificação. Por outro lado, ao usar linguagens “sintéticas” como Coq, especificamos a especificação com precisão e primeiro. Agradecendo que haja generalização da correspondência Curry-Howard, o programa pode ser gerado se e somente se provarmos que a especificação do programa está correta.
Aqui vimos duas formas opostas de verificação do programa, analítica versus sintética.
Eu não mencionaria o que é melhor porque ambas as formas têm pontos fracos.
por exemplo, a maneira sintética sempre pode ter um programa trivial. (Mesmo se escrevermos especificações S_1, … S_n e se esquecermos de adicionar uma especificação S_{n+1} de que necessitamos, podemos sempre ter o programa sintético trivial. E a técnica de prova em linguagem sintética como Coq às vezes é muito mais difícil do que a verificação formal da análise do programa usando aproximação. )
Condição de guarda
Em relação ao Pen Compiler, atualmente definimos a Árvore de Sintaxe, seu Gráfico de Programa e a matriz de representação, ou seja, estamos desenvolvendo a parte analítica.
Particularmente, no que diz respeito ao Program Graph, não decidimos como lidar com loops no gráfico.
Uma das formas analíticas de verificação de loop é a “análise invariante”, que é estudada na teoria da Lógica de Hoare. No entanto, a análise invariante exige que especifiquemos qual é o invariante e pode ser difícil encontrá-lo em alguns casos. Então, como lidar com loops? Para a pergunta, gostaríamos de aplicar uma forma sintética ao compilador de caneta. É a chamada “condição de guarda”.
A condição de guarda afirma que a condição de ramificação do loop tem estrutura de dados indutiva e cada vez que atingimos a condição, temos que encolher a estrutura, e ela deve encolher para apenas uma “estrutura pontual”, quebrando o loop.
Por exemplo, o compilador Coq usa a condição de guarda para garantir que os programas em Coq parem e sejam analisados estaticamente.
Muitos compiladores, como o Solidity, usam Integer, mas talvez não precisemos dele.
Em vez disso, temos números naturais (números positivos e inteiros como no estilo Coq).
Os números negativos podem ser representados por números naturais na contabilidade por partidas dobradas.
Talvez não precisemos de números inteiros de maneira formal.
Às vezes dizemos que a condição de ramificação do loop é “noetheriana” se satisfizer a condição de guarda, uma vez que a sequência de condições é descendente e tem o fim, assim como as sequências descendentes na geometria algébrica são noetherianas se tiverem o ponto final nomeado por um grande matemático “Emmy Noether”.
Códigos de operação formais
Nessas suposições, não podemos usar os dados da EVM ADD Diretório Opcode na adição de dois números desde ADD funciona exatamente como definido no EVM.
Temos estruturas de dados indutivas e precisamos incorporá-las ao EVM. Como o código EVM incorporado funciona e é chamado no EVM, a verificação estática não significa, mesmo que verifiquemos o código cuidadosamente em tempo de compilação. Portanto, ao incorporar a estrutura de dados, temos que definir a adição formal FADD ser adição com verificação de condição de contorno, FMUL ser multiplicação com verificação de condição de contorno e assim por diante. É claro que os preços do gás dos Opcodes Formais deveriam ser baratos.
Fontesethresear
