README.md

IMPRESS EDSL

This document still needs reviewing and might not reflect the current state of the project properly!

We want to help students learn about formal program verification. One aspect of this is writing pre and post conditions for their programs. To help the students learn this we developed a tool that can compare two program specifications and can come up with a counter example if the two specifications don't match.

One use case could be to integrate our tool in a submission system like DOMjudge. We then allow students to submit their programs and they get instant feedback on their work.

A proof of concept can be found in src/SimpleFormulaChecker.hs, the "main" function is compareSpec.

Java EDSL

To get started we designed a simple embedded DSL that encapsulates all the expressions taught in the Software Testing & Verification (INFOB3STV) course. This includes:

• Integer expressions (addition, subtraction, multiplication, etc.)
• Boolean expressions (AND, OR, NOT)
• Relational operators (bigger, smaller, equal, etc.)
• Quantifications over integer domains
• Array access

To import the EDSL in a Java project, we use:

//Importing the EDSL like this is required for the parser!
import static nl.uu.impress.EDSL.*;

An example Java project can be found in src/javawlp_edsl, the EDSL implementation is in src/impress.

Example 1

public static void swap_spec1(int[] a, int i, int j) {
    // preconditions
    pre(a != null);
    pre(a.length > 0);
    pre(i >= 0);
    pre(j >= 0);

    // introducing variables to remember old values
    int oldai = a[i], oldaj = a[j];

    // call the actual function implementation
    swap(a, i, j);

    // postconditions
    post(a[j] == oldai);
    post(a[i] == oldaj);
}

This example uses simple arithmetic and shows that multiple pre/post conditions are allowed. Internally they will be appened in a conjunction, but this allows the student to work more easily.

Example 2

public static void getMax_spec1(int[] a) {
    // preconditions
    pre(a != null);
    pre(a.length > 0);
    
    // call the actual function implementation
    int retval = getMax(a);
    
    // postconditions
    post(exists(a, i -> a[i] == retval)); // A
    post(forall(a, i -> a[i] <= retval)); // B
}

This example uses the EDSL quantifier functions exists and forall. In addition to a meaning for the DSL, they also have runtime implementations that allows you to test conditions with concrete values.

Postcondition A will be mapped to:

Postcondition B will be mapped to: