Veja todos os tutoriais em https://educacaocardano.wordpress.com/
12. Análise estática
Uma característica distintiva de Marlowe – provavelmente sua característica mais distinta – é que podemos analisar contratos e deduzir propriedades deles, sem executá-los.
Podemos verificar, antes da execução de um contrato, estas propriedades:
-
Pagamentos parciais: ou seja, pagamentos quando não havia dinheiro suficiente na conta.
-
Depósitos não positivos: sob os quais o contrato pede um valor negativo ou nulo.
-
Pagamentos não positivos: pagamentos de 0 ou um valor negativo.
-
Shadowing de Lets, quando dois Lets definem o mesmo identificador no mesmo caminho de execução.
No restante deste tutorial, focaremos no primeiro deles, que é o pior tipo de erro. É nesse caso que um pagamento falha, porque não há dinheiro suficiente no contrato (ou mais estritamente na conta) para efetuar um pagamento completo.
12.1 Um exemplo
Vejamos este exemplo, em Blockly
e em puro Marlowe:
O primeiro exige um depósito de Alice de 1 Lovelace e, em seguida, solicita que Bob faça uma escolha (chamada bool) de 0 ou 1. O contrato paga essa opção mais um para Bob da conta de Alice.
Portanto, podemos ver que, enquanto o contrato funciona bem quando Bob escolhe 0, não haverá contrato suficiente para pagá-lo se ele escolher 1. Nossa análise, que está embutida na guia SIMULATION no Marlowe Playground, pode diagnosticar isto:
Isso mostra que o erro ocorre quando
-
Alice fez o depósito e
-
Bob escolheu o valor 1.
e que o erro gerado é um TransactionPartialPay: nesse caso, Bob recebe apenas um pagamento de 1 em vez de 2.
Se modificarmos o contrato para que Alice faça um depósito inicial de 2, a análise será bem-sucedida:
12.2 Sob o capô
Apenas para reiterar: o efeito dessa análise é verificar todos os caminhos de execução possíveis através do contrato, usando uma versão simbólica do contrato. Isso é passado para o resolvedor Z3 SMT, que é um sistema automatizado de última geração para decidir se as fórmulas lógicas são satisfatórias.
Se a análise não for bem-sucedida, ou seja, se houver uma maneira de fazer com que o contrato falhe em um pagamento, o sistema também fornecerá um exemplo de como pode dar errado e apresentará isso ao usuário. Os usuários podem corrigir o problema e verificá-lo novamente.
12.3 Próximos passos
Nos próximos meses, veremos como apresentar os resultados de nossa análise de uma maneira mais “amigável”, além de ampliar o escopo de nosso trabalho.
Exercício
Use o botão de análise no Marlowe Playground para analisar alguns dos contratos que você já escreveu. Se a análise falhar, você pode ver o motivo e corrigir os contratos para que eles não falhem.