­č笭čçŞ Tutoriales de Marlowe: 11. An├ílisis est├ítico

Análisis estático

Una caracter├şstica distintiva de Marlowe -probablemente la m├ís distintiva- es que podemos analizar los contratos, y deducir sus propiedades, sin ejecutarlos.

Podemos comprobar, antes de ejecutar un contrato, estas propiedades:

  • Pagos parciales: es decir, pagos cuando no hab├şa suficiente dinero en la cuenta.
  • Dep├│sitos no positivos: en los que el contrato pide un valor negativo o cero.
  • Pagos no positivos: pagos de 0 o un importe negativo.
  • Sombreado de Lets , donde dos Lets fijan el mismo identificador en la misma ruta de ejecuci├│n.

En el resto de este tutorial nos centraremos en el primero de ellos, que es el peor tipo de error. Es en este caso que un pago falla, porque no hay suficiente dinero en el contrato (o más estrictamente en la cuenta) para hacer un pago completo.

Un ejemplo

Veamos este ejemplo, en Blockly

MT-11-1

Y en puro Marlowe

MT-11-2

El contrato exige en primer lugar un depósito de Alice de 1 Lovelace, y luego le pide a Bob que haga una elección (llamada bool) de 0 o 1. El contrato paga entonces esta elección más uno a Bob con cargo a la cuenta de Alice.

As├ş, podemos ver que mientras el contrato funciona bien cuando Bob elige 0, no habr├í suficiente en el contrato para pagarle si elige 1. Nuestro an├ílisis, que est├í integrado en la pesta├▒a SIMULATION del Marlowe Playground, puede diagnosticar esto:

MT-11-3

Esto muestra que el error se produce cuando

  • Alice ha hecho el dep├│sito, y
  • Bob ha elegido el valor 1.

y que el error generado es un TransactionPartialPay: en este caso Bob s├│lo recibe un pago de 1 en lugar de 2.

Si modificamos el contrato para que Alice haga un dep├│sito inicial de 2, entonces el an├ílisis tendr├í ├ęxito:

MT-11-4

Bajo el cap├│

S├│lo para reiterar: el efecto de este an├ílisis es comprobar cada posible ruta de ejecuci├│n a trav├ęs del contrato, utilizando una versi├│n simb├│lica del mismo. Esto se pasa al solucionador Z3 SMT, que es un sistema automatizado de ├║ltima generaci├│n para decidir si las f├│rmulas l├│gicas son satisfechas.

Si el an├ílisis no tiene ├ęxito, es decir, si hay una forma de hacer que el contrato falle un pago, entonces el sistema tambi├ęn dar├í un ejemplo de c├│mo puede salir mal, y lo presentar├í al usuario. El usuario puede entonces arreglar el problema y volver a comprobarlo.

Pr├│ximos pasos

En los pr├│ximos meses estudiaremos c├│mo presentar los resultados de nuestro an├ílisis de una manera m├ís ÔÇťamigableÔÇŁ, as├ş como ampliar el alcance de nuestro trabajo.

Utiliza el bot├│n de an├ílisis en el Marlowe Playground para analizar algunos de los contratos que ya has escrito. Si el an├ílisis falla, ┬┐puedes ver por qu├ę y corregir los contratos para que no fallen?

┬ę Copyright 2020, IOHK Revision 614a0b3a.

Encuentra una copia oficial de este documento aqu├ş:

https://alpha.marlowe.iohkdev.io/doc/marlowe/tutorials/static-analysis.html

https://docs.cardano.org/projects/plutus/en/latest/marlowe/tutorials/static-analysis.html

Más traducciones de Cardano en: Cardano For The World