Prototypal Verification Language

This page discusses the language features of PVL, the Prototypal Verification Language of VerCors. The language is similar to Java, so it has classes, methods, etc. It doesn't have modifiers like public and private. This language is used for research too, so some special constructs like the par-block have been added to it. This section elaborates on the basic language features of PVL. The more advanced features are described in later sections. A complete reference overview of the PVL language and specification syntax can be found here.

Basic types and expressions

Currently, VerCors supports the types int, boolean, and void (for return types of methods). Identifiers, e.g. variables and method names, can consist of the characters a-z, A-Z, 0-9 and _. However, they must start with a letter (a-z, A-Z). The following words are reserved and can therefore not be used as identifiers:

inline, assert, package, class, kernel, barrier, invariant, constructor, run, if, else, while, for, goto, return, vec, par, and, parallel, sequential, block, lock, unlock, wait, notify, fork, join, this, null, true, false, current_thread, global, local, static, unfolding, in, new, id, boolean, void, int, string, resource, process, frac, zfrac, bool, ref, rational, seq, set, bag, pointer, map, option, either, tuple, type, any, nothing, pure, thread_local, with, then, given, yields, axiom, model, adt, modifies, accessible, requires, ensures, context_everywhere, context, loop_invariant, kernel_invariant, lock_invariant, signals, decreases, apply, fold, unfold, open, close, assume, inhale, exhale, label, refute, witness, ghost, send, to, recv, from, transfer, csl_subject, spec_ignore, action, atomic, Reducible, AddsTo, APerm, ArrayPerm, Contribution, held, HPerm, idle, perm, Perm, PointsTo, running, Some, Left, Right, Value, none, None, write, read, empty.

Standard operators can be used to form expressions from values and variables of type int or boolean:

• boolean operators: &&, ||, !, ==>, ==, !=, <, <=, >, >=
• arithmetic operators: +, -, *, /, ++, --
• if-then-else expression: b ? e1 : e2 where b is a boolean expressions, and e1 and e2 are expressions of the same type

Other expressions:

• Create new object: new T(...) where T(...) is defined by the constructor of class T
• Create an array: new T[i] where T is a type (so int, boolean, or a class T) and i a non-negative integer.

Classes, fields, methods

A program consists of one of more classes. Classes have a name, zero or more fields, zero or more constructors, and zero or more methods. Below we show a small example class:

class MyForest {
    int nrTrees;
    
    MyForest(int nr) {
        nrTrees = nr;
    }

    void plantTrees(int nr) {
        nrTrees = nrTrees + nr;
    }
}

The keyword this can be used to refer to the current object. Methods and functions may also be declared outside any class, mimicking the behavior of static methods in Java.

Control flow: return, if, while, for

A method body consists of statements. The basic statements of PVL are:

• assignment: x = e; where x is a variable and e an expression.
• return: return e;, where e is an expression of the type of the method
• if-statement: if (b) then { s1 } or if (b) then { s1 } else { s2 }, where b is a boolean expression and s1 and s2 are (sequences of) statements.
• while-loop: while (b) { s1 }, where b is a boolean expression and s1 a (sequence of) statement.
• for-loop: for(int i = e1; b; e2), where i is an identifier e1 is an integer expression, b a boolean about i and e2 an update of i.
• comments: single line comments // put a comment here, or multiline comments /* put a comment here */.

Below we show a method using these constructs:

int myExampleMethod(int nr) {
    nr = nr + 3;
    if(nr > 10) { /* here is a multi-line comment
                     in the if-branch */
        nr = nr-3;
        for(int i = 0; i < 2 && nr > 5; i++) {
            nr = nr/2;
        }
    } else { //we subtract a bit
        while (nr > 2) {
            nr--;
        }
    }
    return nr + 5;
}

Proof helpers: frame, if(*)

Proof helpers do not have an equivalent in regular programming languages, but can be used to instruct the solver to take a certain path.

You can use if(*) to encode a non-deterministic branch. Exactly one branch of the if is chosen, but it is not known to the solver which one. The syntax is as a normal if, but with the condition *:

void test() {
    if(*) {
        x[0] = 3;
    } else if(*) {
        x[1] = 8;
    } else {
        return;
    }
}