Especificación de Vyper en Maude

Abstract

En este trabajo se ha utilizado el lenguaje Maude para especificar la sintaxis de Vyper y desarrollar un sistema de entrada/salida, en el que el usuario elige los contratos y las funciones a ejecutar con el objetivo de devolverle la salida de cada ejecución y el estado del contrato en ese momento. El desarrollo del proyecto se puede dividir en tres partes. En la primera parte se ha desarrollado una primera forma de la gramática de Vyper que comprueba que cada línea de código tenga una forma correcta. Para poder desarrollar esta primera gramática, se ha utilizado la documentación de Vyper y se han tomado varios contratos de ejemplo donde se han podido ver distintas casuísticas que no se deducían de la documentación. Tras recibir un contrato se ejecuta un preprocesamiento encargado de transformar distintas partes del código de Vyper con el objetivo de facilitar el diseño de la representación interna, que por la forma de programar en Maude daba lugar a distintos problemas. A continuación, el contrato se pasa por una función propia de Maude para darle forma uniforme y por otra función de implementación propia que corrige su forma y lo dispone para la fase siguiente. En la segunda parte, se ha definido una segunda gramática de Vyper y se han desarrollado distintas estructuras de datos para almacenar variables y representarlas como se verían en Vyper. Para mantener una imagen del contrato durante la ejecución se ha desarrollado los conceptos de pila de memorias y memoria de funciones: el primero guarda una imagen del programa y almacena todas las variables simples y estructuras complejas, y la segunda guarda la definición de todas las funciones ejecutables dentro del contrato. En la tercera parte se han definido reglas de reescritura para especificar la semántica del lenguaje. Asimismo, se ha definido un módulo funcional para conectar las reglas con las estructuras de datos y conseguir inicializar, introducir, extraer y comprobar condiciones útiles para la correcta ejecución del contrato. Por último, se ha definido un módulo de sistema para especificar la entrada/salida para que el usuario interactúe con el programa e indicar qué contrato se quiere cargar, las funciones a ejecutar y los parámetros de estas. Por cada función ejecutada se muestra al usuario si la salida es correcta y la imagen del programa en ese momento.

In this work, the Maude language has been used to specify the syntax of Vyper and to develop an input/output system, in which the user chooses the contracts and the functions to be executed with the aim of returning the output of each execution and the state of the contract at that moment. The development of the project can be divided into three parts. In the first part, a first form of the Vyper grammar was developed, which checks that each line of code has a correct form. In order to develop this first grammar, the Vyper documentation has been used, and several example contracts have been taken where different cases that could not be deduced from the documentation could be seen. After receiving a contract, preprocessing is carried out to transform different parts of the Vyper code in order to facilitate the design of the internal representation, which, due to the way Maude was programmed, gave rise to various problems. The contract is then passed through Maude’s own function to give it a uniform form and through another implementation function that corrects its form and prepares it for the next phase. In the second part, a second Vyper grammar has been defined and different data structures have been developed to store variables and represent them as they would be seen in Vyper. To maintain an image of the contract during execution, the concepts of memory stack and function memory have been developed: the former stores an image of the program and stores all simple variables and complex structures, and the latter stores the definition of all executable functions within the contract. In the third part, rewrite rules have been defined to specify the semantics of the language. A functional module has also been defined to connect the rules with the data structures and to initialize, introduce, extract and check conditions useful for the correct execution of the contract. Finally, a system module has been defined to specify the input/output for the user to interact with the program and to indicate which contract is to be loaded, the functions to be executed and their parameters. For each function executed, the user is shown whether the output is correct and the image of the program at that moment.