Translation and Verification Methods

[RU|EN]

This is the set of hands-on excercises to support the lecture course of Translation and Verification Methods taught on FIT NSU as a part of the 09.03.01 education program.

Introduction

This set of excercises aims at building the verifying translator from a toy language Funny into WASM. The code of these excercises is based on the following technologies:

• Implementation language: Typescript
• Execution environment: Node.js
• Compilation target: Wasm
• Theorem prover: Z3 via the z3-solver package
• Package manager: pnpm
• Parser library: Ohm
• Autotests: Jest (may be replaced)
• IDE: VS Code (optional)

Excercise Evaluation

There are a set of goals for each lab. Every goal is tagged with a mark. In order to get a C mark (3) for the whole practice, one must achieve all the goals tagged with C. To get a B, one needs to achive all the B and all the C goals, and so on. To verify the solutions, one should use the built-in test framework: specify the desired mark in the file desiredMark.json, and run the auto-tests. The tests for the goals above the requested mark would be automatically skipped.

Contents and Solution Order

The recommended order of implementation is starting from Lab 01 and proceeding sequentially through Lab 11:

• Lab 01: Addition and Multiplication
• Lab 02: Reverse Polish Notation
• Lab 03: Arithmetic Expressions
• Lab 04: Parsing Arithmetics to AST
• Lab 05: Compiling to Wasm
• Lab 06: Symbolic Derivation
• Lab 07: Algebraic Simplification
• Lab 08: Parsing Funny
• Lab 09: Compiling Funny
• Lab 10: Parsing Funny Annotations
• Lab 11: Verifying Funny

Some of the labs can be done out-of-order, but many do depend on each other. Here is the complete dependency map:

flowchart LR
    Lab01[<a href="./lab01/README.md">Lab01</a>]
    Lab02[<a href="./lab02/README.md">Lab02</a>]
    Lab03[<a href="./lab03/README.md">Lab03</a>]
    Lab04[<a href="./lab04/README.md">Lab04</a>]
    Lab05[<a href="./lab05/README.md">Lab05</a>]
    Lab06[<a href="./lab06/README.md">Lab06</a>]
    Lab07[<a href="./lab07/README.md">Lab07</a>]
    Lab08[<a href="./lab08/README.md">Lab08</a>]
    Lab09[<a href="./lab09/README.md">Lab09</a>]
    Lab10[<a href="./lab10/README.md">Lab10</a>]
    Lab11[<a href="./lab11/README.md">Lab11</a>]

    
    Lab03 --> Lab04
    Lab04 --> Lab05
    Lab04 --> Lab06
    Lab03 --> Lab07
    Lab04 --> Lab07
    Lab03 --> Lab08
    Lab04 --> Lab08
    Lab08 --> Lab09
    Lab08 --> Lab10
    Lab09 --> Lab10
    Lab04 --> Lab11
    Lab09 --> Lab11
    Lab10 --> Lab11

Loading

Note: getting the passing mark requires breadth, i.e. completing all the excercises on the desired level. The recommended approach to this course is to focus on getting all the labs done with the basic goals (setting the desired mark to 3 and making sure all the tests are passed). Then try to improve the depth by changing the desired mark to 4, and fixing the failed tests if any. This approach ensures smart resource allocation - if one doesn't have enough time to complete all the excercises, they would better get a passing mark than risking to get half the labs solved at a perfect level.

Prerequisites and Installation

1. Download and install Node.js with pnpm for your platform: https://nodejs.org/en/download

2. Checkout this project.

3. Run a terminal at the project root location and execute

   pnpm install -r

   This will download and install the dependencies for all the labs

4. (Optional) download and install VS Code: https://code.visualstudio.com/Download

   • Install recommended extensions. Support for JavaScript and TypeScript is included in VS Code out of the box. Two extra tools would be handy
     • Jest extension helps you running the unit tests (that are going to be the basis of the excercise acceptance)
     • Ohm-JS Language extension helps you to write the PEG grammars extensively used throughout this course

5. Build the labs

   • VS Code: press Shift-Ctrl-B.

   • CLI: run terminal at the root folder of any lab; execute pnpm build

     Running pnpm -r build will build all labs at once.

6. Run tests Note: don't forget to set the desired mark via the desiredMark.json!

   • VS Code: switch to the Testing tab, hover the project root, click "Run Tests" icon
   • CLI: run the jest command at the project root