🇧🇷 Tutorial Marlowe 12/14

PortuguĂŞs Geral
1

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.

2 Likes