Introduction

Welcome to the VerCors tutorial! In this tutorial, we will look at what VerCors is, what it can do, and how you can use it.

VerCors is a toolset for software verification. It can be used to reason about programs written in Java, C, OpenCL and PVL, which is a Prototypal Verification Language that is developed alongside VerCors and often used to demonstrate and test the capabilities of VerCors.

In this tutorial, we will first take a brief look at where VerCors fits into the bigger picture of software verification. As this is only a brief look, we recommend users that are unfamiliar with software verification to take a look at the chapter "Background" that gives more information on software verification and some of the terms used below. Then, we will discuss the syntax of PVL and Specifications in VerCors. Once we have a basic idea of how things work, we look at several more advanced concepts, either of VerCors (e.g. resources) or of the input languages (e.g. inheritance). You can find an overview of the chapters on the right.

VerCors

VerCors is a verification tool that uses static analysis to prove partial correctness of a given piece of code. It requires users (e.g. software developers) to add annotations in the code, which specify the expected behaviour. The chapter "Specification Syntax" of this tutorial describes the syntax for these annotations. VerCors particularly targets parallel and concurrent programs, using the permission-based Concurrent Separation Logic (CSL) as its logical foundation. CSL is a program logic that has a very strong notion of ownership in the form of (fractional) permissions: A thread can only read from, or write to, shared memory if it owns enough permission to do so. An advantage of concurrent separation logic is that, due to the explicit handling of ownership, we get properties like data-race freedom and memory safety for free; these properties are consequences of the soundness argument of the logic. A disadvange is that it causes significant overhead to always deal with permissions explicitly. Therefore, if you only wish to verify sequential algorithms, it may be worthwhile to look at alternative tools such as OpenJML and KeY, which do not use CSL as their logical foundation. For more info on CSL, ownership and permissions, see the chapter "Permissions".

VerCors' analysis is modular, proving each method in isolation: Each method has a contract specifying the pre-conditions that must be met before calling the method, and the post-conditions that are certain when the method call finishes. Analysis of a method body happens solely based on the contract, not considering any actual calling environments.

While VerCors currently supports Java, C (incl. OpenMP), OpenCL and PVL, it is designed to be extensible, in the sense that support for other input languages with parallel and concurrent language constructs (for example C#) can be added without much difficulty. For that, the aim for VerCors is to allow reasoning over many different general concurrency structures, like statically-scoped concurrency (e.g. GPU kernels), dynamically-scoped concurrency (e.g. fork/join parallelism), and automated parallelism (e.g. programs that are automatically parallelised using OpenMP).

Note that VerCors checks for partial correctness, meaning that if the program terminates, then it satisfies its post-conditions. No proof is attempted to check whether the program actually terminates.

It is worth noting that VerCors is not the only tool that can perform static verification on annotated programs; there are actually many tools that can do a very similar job. Examples of such tools are: Dafny, OpenJML, KeY, VeriFast, and VCC. However, VerCors distinguishes itself by focussing on different parallel and concurrent language constructs (e.g. Dafny, OpenJML, and KeY only allow verifying sequential programs) of various high-level programming languages (e.g. VCC only allows to verify C programs). Moreover, VerCors is not designed to be language-dependent, and instead focusses on verification techniques for general concurrency patterns.

Internally, VerCors uses the Viper backend, which in turn uses the SMT solver Z3.

Background

In this chapter, we explain some of the terms related to VerCors, for example static analysis. If you are already an experienced user of software verification tools, feel free to skip it. If you are new to the topic, we recommend reading this chapter to better understand the other chapters.

Software Verification

Nowadays, we as a society rely heavily on software, and software errors can have a major impact, even causing deaths. Thus, software developers strive to reduce the number of software errors as much as possible. Software verification is the task of reasoning about the behaviour of the software, in order to ensure that it behaves correctly. The most basic case could be considered to be the compiler, which checks that the program e.g. does not misspell a name. Only if the compiler does not find any errors, then the program can be executed. However, many errors that are more intricate can slip past the compiler. To catch these, there are two possibilities: Static analysis and dynamic analysis. Dynamic analysis runs the program and watches its behaviour. One example is testing, where you provide the software with a concrete input, let it compute an output and check that it is the expected one. While this can show errors, it cannot guarantee the absence of errors: Maybe it only works for this specific input, and even that only in non-leap years. Static analysis looks at the source code itself, and can thus reason in more general terms. The compiler is part of this category, and so is VerCors.

Different tools provide different levels of analysis. As an example, let's take a division by zero, which is not allowed in mathematics and would cause the software to misbehave. In the most simple case, we could search for expressions like 1/0, which we recognise as bad immediately. But what about 1/x? Maybe x is zero, maybe not. Some tools will check the program to find all possible values that x can take. But this is often difficult to decide, and the tools often approximate (e.g. instead of saying "-1, 1 or 2", they say "the interval [-1,2]", thereby also including the value 0 even though it cannot occur in reality). This can lead to false results, e.g. complaining about programs that are actually correct. Other tools require the user (meaning the software developer) to specify which values x can take. This requires much more effort by the user, who has to annotate the code, i.e. provide additional information inside the program that is not needed to run the program, but only for analysing it. As a reward for the additional effort, the user can get more accurate results. VerCors follows this approach, requiring the user to provide specifications as annotations. The chapter "Specification Syntax" of this tutorial describes the syntax for these annotations.

Annotations can have different purposes, and two are particularly relevant: Assertions or proof obligations are properties the user wants to be proven, for instance that a function computes the correct value. Assumptions provide the tool with additional knowledge to help its proof; the tool takes them as given facts and does not prove them. A common example are method pre-conditions, where the user specifies the context in which the method is called. That way, when analysing the method itself, the tool can reason more accurately e.g. about the values of input parameters. However, that means that the analysis results is only applicable if the respective assumptions are met. So users (particularly new users) should pay attention what facts were actually proven, and what was assumed, and be aware under which conditions the analysis result holds.

As an example, consider the following code:

int foo(int arg) {
  return 10/arg;
}

If we assume that the method is only invoked with arguments arg>0, then we can assert (or prove) that no division by zero occurs, and even that the result is between 0 and 10. Note that if the assumption is unsatisfiable (e.g. two contradictory conditions, or a simple false), then we can derive any boolean statement, because the implication "if assumption then statement" is trivially true. Thus, users must be careful in their choice of assumptions.

Separation Logic

VerCors particularly targets parallel and concurrent programs, as they are more difficult to understand intuitively and thus are more error-prone than sequential programs. One typical example is two parts of the program accessing the same memory location at the same time. This can lead to the unintuitive fact that, right after one thread wrote a value to a variable, that variable might already have an entirely different value due to the other thread jumping in between and changing it. To avoid one thread invalidating the properties and invariants maintained and observed by the other threads, VerCors uses Permission-Based Separation Logic (PBSL) as its logical foundation. PBSL is a program logic that has a very strong notion of ownership in the form of (fractional) permissions: A thread can only read from, or write to, shared memory if it owns enough permission to do so. So just because a variable is on the heap, shared and technically accessible by everyone, that does not mean that just anyone can go ahead and use it; they need to coordinate with the others by getting permission first. The specification language of VerCors has constructs to deal with ownership and permissions (see the chapter "Permissions"). An advantage of this approach is that, due to the explicit handling of ownership, we get properties like data-race freedom and memory safety for free; these properties are consequences of the soundness argument of the logic. You will notice that the handling of permissions makes up a significant part of the verification effort, and "Insufficient Permissions" is a frequent complaint by VerCors in the beginning. And while VerCors can be used to analyse sequential programs, it always requires this overhead of managing permissions. Therefore, if you only wish to verify sequential algorithms, it may be worthwhile to look at alternative tools such as OpenJML and KeY, which do not use PBSL as their logical foundation.

Installing and Running VerCors

The installation and running instructions can be found on the Github homepage of this project.

Syntax highlighting

When writing a program in PVL, the Prototypal Verification Language of VerCors, syntax highlighting can be obtained in the following way:

VerCors provides syntax highlighting support for PVL in TextMate 2 (MacOS X) and Sublime Text (Linux and Windows) as a TextMate Bundle. The bundle is located at ./util/VercorsPVL.tmbundle. On MacOS X for TextMate 2 you can simply double click the .tmbundle file to install it. Sublime Text requires you to copy the bundle content to some directory:

1. In Sublime Text, click on the Preferences > Browse Packages… menu.
2. Create a new directory and name it VercorsPVL.
3. Move the contents of VercorsPVL.tmbundle (that is, the ./Syntaxes directory) into the directory you just created.
4. Restart Sublime Text.

Visual Studio Code (VS Code) also has support for TextMate bundles to do syntax highlighting (VS Code runs on Windows, Linux and OSX). Click here for instructions on how to install this (this has not been tested however).

Prototypical 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;
    }
}

Specification Syntax

This section describes the syntax of the specification language, which is independent of the target language. Thus, unless otherwise stated, all features are supported for all input languages.

In this part of the tutorial, we will take a look at how specifications are expressed in VerCors. While this tutorial provides more detailed explanations of the various constructs, a concise list can be found in the PVL Syntax Reference in the annex. The specification language is similar to JML.

Depending on the input language, specification are embedded into the target code in two different ways: In most languages, such as Java and C, the specifications are provided in special comments. These special comments are either line comments starting with //@, or block comments wrapped in /*@ and @*/. Since these are simply a kind of comment, regular compilers ignore them and can still compile the program. However, the @ signals VerCors to interpret them as annotations. Note that this style of comment comes from JML, so VerCors is not the only tool using them. However, the exact interpretation of the comments may vary between tools, so a valid specification in VerCors may not be recognised by another tool and vice versa.

As an example, a method pre-condition (see following section) can look like this:

//@ requires x>0;
public int increment(int x) { /* ... */ }

/*@
requires x>0;
requires y>0;
@*/
public int add(int x, int y) { /* ... */ }

Tip Always remember to place the @! It can be aggravating to spend significant time debugging, just to realise that parts of the specification were put in regular comments and ignored by the tool.

For PVL, the specifications are inserted directly into the code, without the special comments around them:

requires x>0;
int increment(int x) { /* ... */ }

requires x>0;
requires y>0;
int add(int x, int y) { /* ... */ }

Given that the syntax is otherwise identical, we will use the commented version in the rest of the tutorial, to make the separation between specifications and target code more obvious. The examples in this chapter are in Java, but you can find the respective examples in other languages on the website (as well as a Java file of all the examples below).

Most annotation constructs have to end with a semicolon.

In principle, we can distinguish two kinds of annotations: Specifications in the form of method contracts that specify the observable behaviour of the respective method; and auxiliary annotations that guide the prover towards its goal and are for example used inside a method's body, or to define helper functions. We will first look at the former, then at the latter, and conclude with a description of the kind of expressions that VerCors supports (e.g. boolean connectives). For the earlier parts, it suffices to know that expressions in VerCors specifications are an extension of whatever expressions the target language supports.

Method Contracts

Method contracts specify the behaviour of the method that is visible to the calling environment, by means of pre-conditions and post-conditions. Pre-conditions use the keyword requires and restrict the situations in which the method can be invoked, e.g. restricting parameters to be non-null. Post-conditions use the keyword ensures and describe the behaviour of the method by defining the program state after the call finishes. The method contract is placed above the method header, and these keywords can only be used in combination with a method header.

Two useful keywords to define the post-state (i.e. the state after the method finishes) are \result to refer to the return value of the (non-void) method, and \old(expr) to refer to the value of expr before the method's execution.

class Test {
  /*@
  requires x >= 0;
  requires y >= 0;
  ensures \result == x+y;
  ensures \result >= 0;
  @*/
  public int add(int x, int y) {
    return x+y;
  }

  /*@
  requires xs != null;
  ensures \result != null;
  ensures \result.length == \old(xs.length)+1;
  ensures \result.length > 0;
  @*/
  public int[] append(int[] xs, int y) {
    int[] xsCopy = new int[xs.length + 1];
    /* ... */
    return xsCopy;
  }
}

Recall that VerCors analyses methods in isolation, purely based on their contract and independent from any actual calling contexts. It tries to prove that if the pre-condition is satisfied before the method body is executed, then the post-condition holds afterwards. In the example of the add method above, if the input parameters are non-negative, then the result is, too. Note that the pre-condition x>=0 is not actually required for executing the method body, but it is necessary to prove the post-condition. In contrast, in the example of append, the pre-condition xs!=null is actually needed for \old(xs.length) to be well-defined, and potentially to prove absence of null-pointer dereferences in the method body. Note that, to fully specify the correct behaviour of append, one would have to compare the values inside of xs and \result. Since these values are stored on the heap (and not on the stack like the reference xs itself), this would require access permissions, which will be introduced in the next chapter "Permissions".

Note Method contracts must not have side effects, so for example calls to (non-pure) methods are forbidden inside contracts. Pre- and post-conditions are processed in-order, so for example swapping the order of two pre-conditions could result in a failed verification (e.g. you need to specify that an integer variable is within range before you can use it as an array index in another pre-condition). Note that unsatisfiable pre-conditions (e.g. contradictory conditions, or simply false) can lead to unexpected results, because the implication "if pre-condition before, then post-condition after" becomes trivially true for any post-condition, and VerCors is able to prove any arbitrary statement.

Sometimes, the same expression is needed as a pre- and as a post-condition, for example the fact that a global variable is not null. In that case, the keyword context can be used as a short-hand notation: context xs != null; stands for requires xs!=null; ensures xs!=null;. An even further reaching short-hand is context_everywhere expr;, which adds expr as a pre- and as a post-condition, as well as a loop invariant for all loops inside the method body (see below).

Auxiliary Annotations

When method bodies become more complicated than the toy examples above, it becomes more difficult for VerCors to prove by itself that the post-conditions hold after executing the method, and additional annotations are needed inside the method body to guide the verification. These can take the form of loop invariants, assumptions and assertions, or ghost code. Ghost code can also occur outside of methods, for instance to define helper functions.

Loop Invariants

Loop invariants are similar to the context in a method contracts, but for loops: They specify expressions that must hold before entering the loop (like a pre-condition), as well as after each loop iteration, incl. the last iteration (like a post-condition). Loop invariants use the keyword loop_invariant and are placed above the loop header:

//@ requires a>0 && b>0;
//@ ensures \result == a*b;
public int mult(int a, int b) {
  int res = 0;
  //@ loop_invariant res == i*a;
  //@ loop_invariant i <= b;
  for (int i=0; i<b; i++) {
    res = res + a;
  }
  return res;
}

Let us examine why this program verifies (you can skip this paragraph if you are familiar with software verification and loop invariants): The first loop invariant holds before we start the loop, because we initialise both i and res to zero, and 0 == 0*a is true. Then in each iteration, we increase i by one and res by a, so if res == i*a held before the iteration, then it will also hold afterwards. Looking at the second invariant, we see that it holds before the loop execution because i is initialised to zero and b is required to be greater than zero. To understand why the invariant holds after each iteration, we also have to consider the loop condition, i<b. This condition has to be true at the beginning of the iteration, otherwise the loop would have stopped iterating. Since i and b are integers and i<b at the beginning of the iteration, an increment of i by one during the iteration will ensure that at the end of the iteration, i<=b still holds. Note that if i or b were floating point numbers, i might have gone from b-0.5 to b+0.5, and we would not have been able to assert the loop invariant. Likewise, any increment by more than one could step over b. Only the combination of all these factors lets us assert the invariant at the end of the loop iteration. When the loop stops iterating, we know three things: Each of the two loop invariants holds, and the loop condition does no longer hold (otherwise we would still be iterating). Note that the combination of the second loop invariant and the negated loop condition, i<=b && !(i<b), ensures that i==b. Combining that with the first invariant ensures the post-condition of the method.

Remember that VerCors checks for partial correctness, so there is no check whether the loop actually stops iterating at some point. It just asserts that if the loop stops, then the post-condition holds.

As mentioned above, context_everywhere expr; in the method contract will implicitly add expr as a loop invariant to all loops in the method body. This can be useful for expressions that hold for the entirety of the method, e.g. in the case of xs!=null; but it can also be a subtle cause for errors if it adds invariants to a loop that were not intended there (especially in the case of multiple loops). For example, a method to insert an element into a sorted array may add the new value at the end, and then step by step restore the ordering of the array; in that case, adding a sortedness property as context_everywhere would not verify.

Assumptions and Assertions

Sometimes, VerCors has trouble deriving a post-condition from the given code and established facts (like pre-conditions), and it requires explicitly specifying an intermediate step to guide the verification. VerCors first proves these intermediate steps, and then can use them to derive the desired facts. This can be done with the keyword assert:

//@ ensures a==0 ? \result == 0 : \result >= 10;
public int mult10(int a) {
  int res = a;
  if (res < 0) {
    res = 0-res;
  }
  //@ assert res >= 0;
  return 10*res;
}

(Note that VerCors would be able to verify this example even without the assertion, but this demonstrates how to use assert.)

Tip Assertions can also be useful for debugging: If VerCors fails to prove the post-condition, adding assert statements throughout the method body can help to pinpoint where the verification fails, either because of a shortcoming of VerCors or because of an actual error in the code. Additionally, assert false; should always fail, so if the verification does not seem to terminate, adding such statements throughout the method can show where VerCors gets stuck. Finally, remember that a contradiction e.g. in the pre-conditions can imply anything; even false. So assert false; can be used to check that no such contradiction occurred: If it verifies, something went seriously wrong.

While assertions add additional proof obligations, assumptions introduce additional facts that VerCors just takes for granted afterwards, similar to pre-conditions. This is done via the keyword assume. This can be dangerous if the assumptions contradict the actual state of the program:

int x = 2;
//@ assume x == 1;
int y = x + 3;
//@ assert y == 4;

This snippet verifies, even though the actual value of y at the end is 5. However, based on the (wrong) assumptions that x==1 on Line 2, the assertion holds. Therefore, assumptions should be used with caution!

Nevertheless, assumptions can be useful, e.g. for debugging purposes. Also, while still being in the process of verifying the code, it can be useful to assume certain basic facts to prove the bigger picture, and then drill deeper and prove that the assumed facts actually hold.

VerCors also supports a refute statement, which is the opposite of assert. Internally, refute expr; is transformed into assert !(expr);, i.e. asserting the negation. Note that a failing assert expr; is not equivalent to a successful refute expr;. For example, if we know nothing about the value of a variable a, then both assert a>0; and refute a>0; will fail, as a could be greater than zero, but it also could be less.

Ghost Code

Recall that annotations must never have side-effects on the program state, otherwise the results of methods would be different between VerCors (which takes the annotations into account) and the compiler (which treats them as comments). However, it can be useful to extend the program state, for example introducing additional helper variables to keep track of intermediate results. This helper code, which only exists for the purpose of verification, is called ghost code, and the respective variables form the ghost state.

Ghost code can occur inside method bodies, but also outside, for instance as global ghost variables. In principle, ghost code can be any construct that the target language supports; for example when verifying Java programs, you could define ghost classes, and in C programs, you may use pointers in ghost code. Additionally, the ghost code can use the extensions that the specification language adds to the target language, such as the new type seq<T> (see section "Expressions" below).

Keep in mind that ghost code does not exist for the compiler, so it cannot have side effects on the program state, and "real" code cannot refer e.g. to ghost variables. However, it is possible to read from "regular" variables (e.g. to create a ghost variable with the same value).

When using constructs from the target language (such as variable declarations), the keyword ghost is required before the use of the construct.

Here is an example for ghost code inside a method:

/*@
  requires x>=0 && y>=0;
  ensures \result == (x<y ? 5*x : 5*y);
@*/
public int minTimes5(int x, int y) {
  //@ ghost int min = (x<y ? x : y);
  int res = 0;
  //@ loop_invariant i<=5;
  //@ loop_invariant res == i*min;
  //@ loop_invariant min<=x && min<=y && (min==x || min==y); 
  for (int i=0; i<5; i++) {
    if (x<y) {
      res = res + x;
    } else {
      res = res + y;
    }
  }
  /*@ 
  ghost if (x<y) {
    assert res == 5*x;
  } else {
    assert res == 5*y;
  }
  @*/
  return res;
}

Note the definition of a ghost variable min at the beginning of the method, and the ghost if statement at its end.

Ghost Methods and Functions

You can use ghost code not only within methods but also to declare entire ghost methods:

/*@
ghost
requires x > 0;
ensures \result == (cond ? x+y : x);
static int cond_add(bool cond, int x, int y) {
  if (cond) {
    return x+y;
  } else {
    return x;
  }
}
@*/

//@ requires val1 > 0 && val2>0 && z==val1+val2;
void some_method(int val1, int val2, int z) {
  //@ ghost int z2 = cond_add(val2>0, val1, val2);
  //@ assert z == z2;
}

The conditional addition cond_add is defined as a ghost method. Otherwise, it looks like any normal method, including having a method contract (in this case, just a single precondition). Note that the precondition is not wrapped in the special comment //@, like the precondition of some_method is, because the entire ghost method already is inside a special comment /*@. We then use this ghost method in the body of some_method (but only inside annotations!).

Functions and Pure Methods

Functions are, in a way, a special kind of ghost methods. They look like any method, but they are pure by design (as signified by the keyword pure) and their body is a single expression following an =, rather than a block of statements:

/*@
requires x > 0;
static pure int cond_add(bool cond, int x, int y) 
  = cond ? x+y : x;
@*/

Note that the ghost keyword is not used: It is only required when using a construct from the target language (e.g. if, variable declarations, etc), not for specification-internal constructs like defining a function. However, using a stand-alone call statement to call the function (e.g. invoke a lemma directly and not in an assert) still needs the ghost keyword, as method calls are constructs from the target language: //@ ghost myLemma();. The important distinction to normal methods, apart from the fact that they have just one expression, is that functions must be pure, i.e. must be without side-effects, even on the ghost state. Thus, the body cannot contain for instance calls to non-pure methods.

Remember that in VerCors, only the contract of a method is used to reason about the behaviour of a method call, the actual behaviour of the method body is not taken into account at this point. For functions, this restriction is not as strict: For simple functions like the one above, VerCors actually uses the "real" behaviour of the function to analyse the behaviour of a call to that function. Thus, the behaviour does not need to be specified explicitly in a post-condition, like it does for other methods. However, this only works for simple functions, and for example a recursive function may still need a post-condition specifying its behaviour.

You can also add the pure keyword to a "real" method. This indicates that the method does not have side-effects, and can therefore be used e.g. in method contracts, while still being accessible by the "real" code. However, for a method to be pure, it has to be actually without side-effects, therefore only a limited number of constructs are allowed in methods that are designated pure: if statements, return statements and variable declarations.

/*@
requires x > 0;
@*/
static /*@ pure @*/ int cond_add(boolean cond, int x, int y) {
  if (cond) {
    return x+y;
  } else {
    return x;
  }
}

Abstract Methods and Functions

Ghost functions and methods do not require a body. Sometimes, you are only interested in the assertions that a function or method gives in its post-condition, and do not care about the actual implementation. In such a case, you can omit the body, turning the method or function abstract. Given that method calls are usually reasoned about only based on the contract, the call site does not see a difference between an abstract method and a "real" method. However, this removes the assurance that it is actually possible to derive the post-condition from the pre-condition by some computation. Consider a post-condition false: The call site will simply assume that the method establishes its post-condition, and treat it as a known fact. Normally, verifying the method body will check that the post-condition is actually fulfilled; but for an abstract method, this check is missing. Since false implies everything, this can easily lead to unsoundness. Therefore, from the perspective of correctness, it is always better to have a body proving that the post-condition can actually be established based on the pre-condition.

However, making a method abstract relieves VerCors from the effort to check that the method body actually adheres to the contract. Therefore, it can be an interesting option to speed up the re-run of an analysis: Once you proved that a method can indeed derive its post-condition, you can turn the method abstract and focus on other parts of the code without checking this method every time you re-run the analysis.

Syntactically, an abstract method or function has a semicolon in place of its body:

//@ requires a>0 && b>0;
//@ ensures \result == a*b;
public int mult(int a, int b);
// commented out body for the sake of speeding up the analysis:
//{
//  int res = 0;
//  // loop_invariant res == i*a;
//  // loop_invariant i <= b;
//  for (int i=0; i<b; i++) {
//    res += a;
//  }
//  return res;
//}

/*@
requires a>0 && b>0;
ensures \result == a+b;
public pure int add(int a, int b);
@*/

Note that VerCors can also work with abstract methods that are not ghost methods (like mult in the example above), but your compiler may complain about missing method definitions.

Inline Functions

Inline functions are like macros in C: You can write an expression that occurs frequently in your code as a macro and then use it as if it were a function; but before verifying the program, VerCors replaces every call to the inline function with the function's body as if you had written out the body in place of the function call. Therefore, during the analysis, the "real" behaviour of the function is taken into account, rather than just the specification of the function's contract. However, inline functions are only possible if the body of the function is simple enough; for example a recursive function cannot be used in that way, otherwise there would be an infinite loop of replacing a function call with the body, which again contains a call. Inline functions are declared using the inline keyword.

//@ pure inline int min(int x, int y) = (x<y ? x : y);

Note that the inline keyword is also used for inline predicates (see chapter "Predicates"), which are a similar concept.

Ghost Parameters and Results

You can extend the header of an existing method, by adding additional parameters and return values to a method. This is done by using the given and yields keywords in the method contract, respectively. To assign and retrieve the values when calling the method, use given and yields symmetrically:

/*@
given int x;
given int y;
yields int modified_x;
requires x > 0;
ensures modified_x > 0;
@*/
int some_method(boolean real_arg) {
  int res = 0;
  /* ... */
  //@ ghost modified_x = x + 1;
  /* ... */
  return res;
}

void other_method() {
  //@ ghost int some_ghost;
  int some_result = some_method(true) /*@ given {y=3, x=2} @*/ /*@ yields {some_ghost=modified_x} @*/;
}

There are several points of interest in this example: Note that the pre- and post-condition of some_method can reference the ghost parameter and result just like normal parameters. If the ghost parameters and results are not just primitive integers, but heap objects, then permissions are needed to access them, just like with normal parameters and results (see following chapter). There is no explicit return statement for the ghost result; instead, the ghost result is whatever value the variable has when the method returns. Therefore, make sure when your method returns that you always have a defined value assigned to your ghost result variable! In other_method, the given keyword is followed by a list of bindings to the ghost parameters. The parameters are named, so the assignment can be in any order, and need not adhere to the order in which the ghost parameters are defined. Make sure to assign a value to each ghost parameter! Otherwise, the method will be missing a parameter, just as if you called a method void foo(int x) as foo();. Similarly, the yields keyword is followed by a block of bindings that retrieve the yielded values. The yielded values may only be immediately assigned to a local variable. The respective local variable, some_ghost, must be a ghost variable, otherwise you would affect the "real" program state from inside an annotation. Note that it is not required to have an output for every yielded value. Both the given and the yields are placed in a specification comment between the method call and the respective semicolon.

Expressions

As mentioned above, expressions in specifications are an extension of the expressions available in the target language. So if you analyse a Java program, you can use expressions like a&&b or x==y+1 in the specifications just like in Java. However, specifications must be free of side-effects (on the program state) and for example calls to non-pure methods are not allowed.

VerCors extends the expressions of the target language by a few more features that you can use in specifications. One of them is the implication operator ==>, which works like you would expect from a logical implication. A common usage is requires x!=null ==> <some statement about fields of x>. Note that the implication binds less than equality or conjunction, so a==>b&&c is equivalent to a==>(b&&c). You need to explicitly use parentheses if the operators shall associate differently.

A related new operator is the null-coalescing operator ?.. It can be used as expr?.fun(args), which is a shorthand for expr!=null ==> expr.fun(args). One use-case, where this comes in handy, is when using predicates in the place of the function fun (see chapter "Predicates").

Two other new operators are ** and -* from separation logic. ** is the separating conjunct, while -* is the separating implication (or "magic wand"). For more on this, see the chapters on Permissions and Magic Wands.

The target language is also extended to include new data types. A simple case is the boolean type bool, which can be useful in specifications if the target language has no boolean type (e.g. old C). If the target language does support boolean (e.g. Java), this is not needed (but can be used nonetheless). More interestingly, the new types include generic axiomatic data types such as set<T> and option<T> (with T being a type). For more information on them and their supported operations (such as getting the size, and indexing elements), see the respective chapter.

An important new type are fractions, frac. VerCors uses concurrent separation logic (CSL) to manage the ownership and permissions to access heap locations. A permission is a value from the interval (0,1], and the type frac represents such a value. To give a value to a variable of type frac, the new operator of fractional division can be used: While 2/3 indicates the classical integer division, which in this example gives 0, using the backslash instead gives a fraction: 2\3. For more on this topic, including some additional keywords for short-hand notations, see the chapter "Permissions".

Sometimes, you might create complicated expressions and want to use helper variables to simplify them. However, certain constructs only allow for expressions, and not for statements such as variable declarations. To alleviate that, there is the \let construct, which defines a variable just for a single expression: ( \let type name = expr1 ; expr2 ), where type is the type of the helper variable, name its name, expr1 defines its value, and expr2 the complicated expression that you can now simplify by using the helper variable. Example:

//@ assert (\let int abs_x = (x<0 ? -x : x); y==(z==null ? abs_x : 5*abs_x));

Quantifiers

Note that most target languages, such as Java and C, support array types, such as int[]. Sometimes, you might want to reason about all elements of the array. To do that, VerCors supports using quantifiers in the specifications: (\forall varDecl, varDecl...; cond; expr). The syntax is similar to the header of a for loop: varDecl declares a variable (e.g. int i); cond is a boolean expression describing a boundary condition, restricting the declared variable to the applicable cases (e.g. defining the range of the integer 0<=i && i<arr.length); and expr is the boolean expression you are interested in, such as a statement you want to assert. Note that the parentheses are mandatory. Here is an example to specify that all elements in the given array are positive:

//@ requires arr != null;
//@ requires (\forall int i ; 0<=i && i<arr.length ; arr[i]>0);
void foo(int[] arr) { /* ... */ }

Note that in practice, you would also have to specify permissions to access the values in the array. More on that in the next chapter.

Tip If you want to quantify over more than one variable (e.g. saying arr1[i] != arr2[j] for all i and j), do not use nesting, this commonly hurts proof performance. Instead, use a list of bindings: (\forall int i, int j; 0<=i && i<arr1.length && 0<=j && j<arr2.length; arr1[i]!=arr2[j]).

If your boundary condition is an interval (like in the examples above), you can use the shorter notation (\forall type name = e1 .. e2 ; expr), where type must be an integral type (e.g. int), name is the name of the quantified variable, e1 and e2 are expressions defining the interval bounds (lower bound inclusive, upper bound exclusive) and expr is the expression you are interested in: (\forall int i = 0 .. arr.length ; arr[i]>0). Note that, depending on the circumstances, spaces are necessary around the ...

You may freely mix normal bindings and range bindings, and omit the condition as you like. For example, all these quantifiers are equivalent:

• (\forall int i, int j; 0 <= i && i < n && i < j && j < n ==> xs[i] < xs[j])
• (\forall int i=0..n, int j; i < j && j < n; xs[i] < xs[j])
• (\forall int i=0..n, int j=i+1..n; xs[i] < xs[j])

There also is an \exists quantifier analogous to the forall quantifier: (\exists varDecl, ...; cond; expr). For instance, we could use a similar example as above, but requiring that at least one array element is positive:

//@ requires arr != null;
//@ requires (\exists int i ; 0<=i && i<arr.length ; arr[i]>0);
void foo(int[] arr) { /* ... */ }

Again, note that in practice, you would also have to specify permissions to access the values in the array.

Note \forall quantifiers are easier to reason about than \exists, because they can be applied indiscriminately whenever an element is encountered, while \exists needs to find the element to which it can be applied. Therefore, \exists quantifiers are more likely to cause problems with VerCors (e.g. non-termination of the analysis), and they should be used with care!

Note: Further sections explain advanced concepts: new users may want to skip those.

Alternative quantifier syntax

In case brevity is needed for readability, you can use the appropriate unicode symbols instead of \forall and \exists:

• (∀varDecl+; (cond ;)? expr)
• (∀*varDecl+; (cond ;)? expr)
• (∃varDecl+; (cond ;)? expr)

The IntelliJ plugin Spec & Math Symbols may be useful to type these symbols.

Triggers

A quantifier (\forall int i = 0 .. arr.length ; arr[i]>0) is a rather generic piece of knowledge; to apply it to a concrete case, for example when encountering arr[1], the quantifier must be instantiated. This basically replaces the quantified variable(s), in this case i, with concrete values. But this is only done when necessary, so when the concrete case arr[1] is actually encountered. Recognising that the quantifier must be instantiated was fairly easy in this case, but for more complex expression it can become rather difficult. In those cases, VerCors might use heuristics, and even randomisation. This can lead to VerCors verifying a program successfully, and when you call it again with the exact same program, the analysis takes forever. So if you experience such behaviour, quantified expressions are a likely cause.

To avoid that, you can explicitly tell VerCors what kind of expression should cause instantiating the quantifier, disabling the internal heuristics. This is called a trigger (or pattern, e.g. by Z3); for more information see the Viper tutorial on triggers. In VerCors, to mark a part of an expression as a trigger, it is enclosed in {: and :}:

//@ requires arr!=null && arr.length>3;
//@ requires (\forall int i ; 0<=i && i<arr.length ; {: arr[i] :} > 0);
void foo(int[] arr) {
  assert arr[3]>0;   // the trigger recognises "arr[3]" and instantiates the quantifier, setting i to 3
}

(Again, Permissions were omitted.)

Note that the trigger must involve all quantified variables. So if you have a quantifier with multiple bindings (\forall int i, int j; ... ; expr), a trigger in expr must be about both i and j. Also note that you cannot use arithmetic expressions or relations as triggers. Most other operators e.g. about sequences and sets may appear in triggers. For instance in the example above, {: arr[i]>0 :} would not be a valid trigger.

Warning A wrong choice of triggers can lead to failed verifications of true statements:

/*@ pure @*/ int f(int a, int b);
    
//@ requires x>0;
//@ requires (\forall int k ; 0<=k && k<=x ; {: f(k, y) :} == 0);
//@ requires (\forall int k ; 0<=k && k<=x ; {: f(k, y) :} == 0 ==> f(k, z) == 0);
void bar(int x, int y, int z) {
    //@ assert f(x, y) == 0;     // this assertion verifies, because "f(x,y)" triggers the first quantifier
    //@ assert f(x/2, z) == 0;   // this assertion fails, even though the quantifiers includes this knowledge
}

In this example, the first quantifier asserts that f(x/2, y) == 0. From that, the second quantifier could derive f(x/2, z) == 0, so the second assertion should hold. However, the second quantifier has no trigger for f(k,z), so the quantifier does not get instantiated and the knowledge remains hidden. Removing the trigger around f(k,y) in the second quantifier leads to a successful verification, because without explicit triggers, VerCors' heuristics finds the correct trigger f(k,z) automatically.

Advanced trigger syntax

It is possible to specify multiple triggers for a single quantifier. In this case, the solver requires all triggers to be present before instantiating the quantifier. This also relaxes the requirement that all bindings must occur in a trigger: instead they must collectively occur in the set of all triggers. For example, a quantifier might state a pairwise equality:

(forall int i, int j; 0 <= i && i < |xs| && 0 <= j && j < |ys|; {:xs[i]:} + {:ys[j]:} == i + j)

This quantifier is only instantiated when both a term of the shape xs[?] and a term of the shape ys[?] is encountered by the solver. {xs[i], ys[i]} is also referred to as a trigger set.

In some cases it is useful to specify multiple trigger sets. In that case, all terms must be matched of any of the trigger sets. By default, a trigger is part of trigger set 0. For example:

(∀`seq`<T> xs, int i, T t;
    0 <= i && i < seq_length(xs) ==> {:1:seq_length({:2:seq_update(xs, i, t):}):} == {:2:seq_length(xs):})

This quantifier is instantiated when a term of the shape seq_length(seq_update(xs, i, t)) is encountered, or both a term of the shape seq_update(xs, i, t) and seq_length(xs). In such a case, it is required that the xs appearing in both patterns are equal before the quantifier is instantiated.

Finally, nested quantifiers are essentially instantiated separately: in principle the inner quantifier is never instantiated, unless the outer quantifier is instantiated. When specifying a trigger that is not meant for the innermost quantifier, you can use some number of < symbols to indicate the trigger belongs to the quantifier that many levels up. For example:

(∀int i; (∀int j; {:<:xs[i]:} == {:xs[j]:}))

Other trigger sources

We recommend the following sources for more examples and explanations of how triggers work.

• Dafny FAQ: How does Dafny handle quantifiers? I've heard about "triggers", what are those?
• Viper tutorial on triggers
• Stack Overflow: quantifiers - What are triggers in Dafny/Boogie?
• Extending Support for Axiomatic Datatypes in VerCors, Section 2.3. Masters thesis by Ömer Şakar. Includes a visual explanation of the workings of triggers using Axiom Profiler, a quantifier instantiation debugging tool.

Permissions

This feature is supported for all languages.

This section discusses the basics of handling ownership using a simple toy example. Ownership is used to express whether a thread (or synchronization object) has access to a specific element on the heap. This access can be shared among multiple threads (or synchronization objects), which allows the threads to read the value of this element, or it can be unique to one, in which case the value can written to or read from. Permission annotations are used to express ownership. We start by considering the following simple example program, written in Java:

class Counter {
  public int val;

  void incr(int n) {
    this.val = this.val + n;
  }
}

If you wish, you can store this file as, say, counter.java, and try to run VerCors on this file by running vct --silicon counter.java in a console (assuming you have VerCors installed). This program currently does not contain any annotations, but we will eventually annotate the program to verify the following simple property: after calling the incr function, the value of val has been increased by an amount n. This can be expressed as a postcondition for the incr method: ensures this.val == \old(this.val) + n. The \old(_) expression is used to evaluate an expression in an earlier state. By default this is in the state as it was just after the precondition. This is explained further later on.

However, if you run VerCors on this example, as it is now, you will see that VerCors fails to verify the correctness of the program and reports an 'AssignmentFailed: InsufficientPermission' error, since the caller of the method has insufficient permission to access this.val. First observe that this.val is shared-memory; there may be other threads that also access the val field, since the field is public. In order to prevent other threads from accessing this.val while the calling thread is executing incr, we need to specify that threads may only call c.incr (on any object c that is an instance of Counter) when they have write permission for c.val:

class Counter {
  public int val;

  /*@
    requires Perm(this.val, 1);
    ensures Perm(this.val, 1);
    ensures this.val == \old(this.val) + n;
  */
  void incr(int n) {
    this.val = this.val + n;
  }
}

We added three things to the counter program. The first is a requires clause, which is a precondition expressing that incr can only be called when the calling thread has permission to write to val. The second is an ensures clause, which is a postcondition expressing that, given that the incr function terminates (which is trivial in the above example), the function returns write permission for val to the thread that made the call to incr. The third is a postcondition that states that after incr has terminated, the value of this.val has indeed been increased by n. If you run this annotated program with VerCors, you will see that it now passes. The remainder of this section mostly focuses on how to use the Perm ownership predicates.

Observe that the clause Perm(this.val, 1) expresses write permission for this.val. Recall that VerCors has a very explicit notion of ownership, and that ownership is expressed via fractional permissions. The second argument to the Perm predicate is a fractional permission; a rational number q in the range 0 < q <= 1. The ownership system in VerCors enforces that all permissions for a shared memory location together cannot exceed 1. This implies that, if some thread has permission 1 for a shared-memory location at some point, then no other thread can have any permission predicate for that location at that point, for otherwise the total amount of permissions for that location exceeds 1 (since fractional permissions are strictly larger than 0). For this reason, we refer to permission predicates of the form Perm(o.f, 1) as write permissions, and Perm(o.f, q) with q < 1 as read permissions. Threads are only allowed to read from shared memory if they have read permission for that shared memory, and may only write to shared memory if they have write permission. In the above example, the function incr both reads and writes this.val, which is fine: having write permission for a field implies having read permission for that field.

Let us now go a bit deeper into the ownership system of VerCors. If one has a permission predicate Perm(o.f, q), then this predicate can be split into Perm(o.f, q\2) ** Perm(o.f, q\2). Moreover, a formula of the form Perm(o.f, q1) ** Perm(o.f, q2) can be merged back into Perm(o.f, q1 + q2). For example, if we change the program annotations as shown below, the program still verifies successfully:

/*@
  requires Perm(this.val, 1\2) ** Perm(this.val, 1\2);
  ensures Perm(this.val, 1\2) ** Perm(this.val, 1\2);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}

For splitting and merging we use the ** operator, which is known as the separating conjunction, a connective from separation logic. A formula of the form P ** Q can be read as: "P, and separately Q", and comes somewhat close to the standard logical conjunction. In essence, P ** Q expresses that the subformulas P and Q both hold, and in addition, that all ownership resources in P and Q are together disjoint, meaning that all the permission components together do not exceed 1 for any field. Consider the formula Perm(x.f, 1) ** Perm(y.f, 1). The permissions for a field f cannot exceed 1, therefore we can deduce that x != y.

One may also try to verify the following alteration, which obviously does not pass, since write permission for this.val is needed, but only read permission is obtained via the precondition. VerCors will again give an 'InsufficientPermission' failure on this example.

/*@
  requires Perm(this.val, 1\2);
  ensures Perm(this.val, 1\2);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}

If you replace both ownership predicates for Perm(this.val, 3/2), then the tool will report a 'MethodPreConditionUnsound: MethodPreConditionFalse' error because the precondition can then never by satisfied by any caller, since no thread can have permission greater than 1 for any shared-memory location. VerCors is a verification tool for partial correctness; if the precondition of a method cannot be satisfied because it is absurd, then the program trivially verifies. To illustrate this, try to change the precondition into requires false and see what happens when running VerCors. Note that VerCors does try to help the user identify these cases by showing a 'MethodPreConditionUnsound' if it can derive that the precondition is unsatisfiable. But one has to be a bit careful about the assumptions made on the program as preconditions.

Self-framing

Consider the following variant on our program. Would this verify?

/*@
  requires Perm(this.val, 1);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}

This program does not verify and gives an 'InsufficientPermission' failure when given to VerCors. The reason is that, also in the specifications one cannot read from shared-memory without the required permissions. In this program, the ensures clause accesses this.val, however no ownership for this.val is ensured by the incr method. Note that, without a notion of ownership, one cannot establish the postcondition: perhaps some other thread changed the contents of this.val while evaluating the postcondition. By having a notion of ownership, no other thread can change the contents of this.val while we evaluate the postcondition of the call, since no other threads can have resources to do so.

Moreover, the order of specifying permissions and functional properties does matter. For example, the following program also does not verify, even though it ensures enough permissions to establish the postcondition:

/*@
  requires Perm(this.val, 1);
  ensures this.val == \old(this.val) + n;
  ensures Perm(this.val, 1);
*/
void incr(int n) {
  this.val = this.val + n;
}

VerCors enforces that shared-memory accesses are framed by ownership resources. Before accessing this.val in the first ensures clause, the permissions for this.val must already be known! In the program given above, the access to this.val in the postcondition is not framed by the ownership predicate: it comes too late.

Permission leaks

So what about the following change? Can VerCors successfully verify the following program?

/*@
  requires Perm(this.val, 1);
  ensures Perm(this.val, 1\2);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}

VerCors is able to verify the example program given above. However, less permission for this.val is ensured then is required, meaning that any thread that calls c.incr will need to give up write permission for c.val, but only receives read permission back in return, after incr has terminated. So this example has a permission leak. Recall that threads need full permission in order to write to shared heap locations, so essentially, calling c.incr has the effect of losing the ability to ever write to c.val again. In some cases this can be problematic, while in other cases this can be helpful, as losing permissions in such a way causes shared-memory to become read-only, specification-wise. However, in the scenario given below the permission leak will prevent successful verification:

/*@
  requires Perm(this.val, 1);
  ensures Perm(this.val, 1\2);
  ensures this.val == \old(this.val) + n;
*/
void incr(int n) {
  this.val = this.val + n;
}
  
/*@
  requires Perm(this.val, 1);
*/
void incr2(int n) {
  incr(n);
  incr(n);
}

In the incr2 method, the first call incr(n) will consume write permission for this.val, but only produce read permission in return. Therefore, the requirements of the second call incr(n) cannot be satisfied, which causes the verification to be unsuccessful.

Some extra notation

We end the section by mentioning some notational enhancements for handling permissions. Instead of writing Perm(o.f, 1), one may also write Perm(o.f, write), which is perhaps a more readable way to express write permission for o.f.

Similarly, one can write Perm(o.f, read) to express a non-zero read permission. Note that if this is used in a pre- and postcondition, it is not guaranteed to be the same amount of permissions. The underlying amount of permissions is an unspecified fraction and can therefore not be merged back into a write permission. This can be observed in the following program where the assert fails:

class Counter {
    int val;

    /*@
    requires Perm(this.val, write);
    ensures Perm(this.val, write);
    ensures this.val == \old(this.val) + n;
    */
    void incr(int n) {
        int oldValue = getValue();
        //@ assert Perm(this.val, write);
        this.val = oldValue + n;
    }
    
    /*@
    requires Perm(this.val, read);
    ensures Perm(this.val, read);
    ensures \result == this.val;
    */
    int getValue() {
        return this.val;
    }
}

read is mostly useful for specifying immutable data structures. One can also write Value(o.f) to express read permission to o.f, where the value of the fractional permission does not matter. Consequently, Value ownership predicates can be split indefinitely.

If you instead want to express that you require some non-zero amount of read permission and that the same amount of permission is returned you an either add a ghost parameter of type frac which must be provided at every call site to specify the amount of available read permission, or you can use AutoValue(o.f). Similarly to Value, AutoValue expresses that some amount of read permission is required. However, unlike Value no amount of read permission is removed when AutoValue is exhaled, it merely checks that there exists some amount of read permission. When the AutoValue in a precondition is inhaled you gain a symbolic non-zero, non-write amount of read permission which must be exhaled at the end of the context again. If the same AutoValue expression does not appear in the postcondition an automatic leak check is added. Usage looks like this (unlike the previous example the assert now passes):

class Counter {
    int val;

    /*@
    requires Perm(this.val, write);
    ensures Perm(this.val, write);
    ensures this.val == \old(this.val) + n;
    */
    void incr(int n) {
        int oldValue = getValue();
        //@ assert Perm(this.val, write);
        this.val = oldValue + n;
    }
    
    /*@
    requires AutoValue(this.val);
    ensures AutoValue(this.val);
    ensures \result == this.val;
    */
    int getValue() {
        return this.val;
    }
}

[!NOTE] Note that AutoValue may only be used in combination with **, ==>, \let .. in .., and .. ? .. : ... For the implication, let, and ternary expressions the AutoValue may only appear on the right-hand side and in the postcondition the left-hand side will automatically be wrapped in \old(_) because the leak check must always occur at the end of the scope to prevent unsoundness.

If you want to express that a thread has no ownership over a certain heap element, then one can use the keyword none, e.g. Perm(o.f, none). This is equivalent to writing true. It can be useful in situations where the amount of permission is conditional, e.g. Perm(o.f, cond ? 1\2 : none).

If you want to express permissions to multiple locations, one may use \forall* vars; range; expr. For example, (\forall* int j; j >= 0 && j < array.length; Perm(array[j], write) denotes that the thread has write access to all elements in array. It is equivalent to writing Perm(array[0], write) ** Perm(array[1], write) ** … ** Perm(array[array.length-1], write). Another way to specify permissions of all array elements is to use Perm(array[*], write) which is equivalent to the previous expression.

If you want to reason about the value that the variable refers to as well then you can use PointsTo(var, p, val) which denotes that you have permission pfor variable var which has value val. It is similar to saying Perm(var, p) and var == val.

Old Heap State

As mentioned earlier, you can use \old(_) to evaluate an expression in an older state. By state here we mean strictly the heap, and not any local variables. By default, the \old predicate uses the heap just after the precondition as the heap to evaluate the expression in. You can specify a different heap with \old[l](_), where l is either a ghost label (//@ ghost label l) or a regular label in your input language.

As an example, consider the following method:

class Obj { int f; }

context Perm(x.f, write) ** Perm(y.f, write);
void test(Obj x, Obj y) {
    Obj z = x;
    
    y.f = 2;
    label a;
    
    z.f = 30;
    label b;
    
    z.f = 400;
    label c;
    
    z = y;
    z.f = 3000;
    label d;
    
    assert
        z.f + // (1)
        \old[a](
            z.f + // (2) 
            \old[b](
                z.f + // (3) 
                \old[c](
                    z.f + // (4)
                    \old[d](
                        z.f // (5)
                    )
                )
            )
        ) == 6006;
}

Any time that an expression uses the heap to evaluate itself, we look where the nearest \old expression is. For us, that is:

• (1) has no \old above it, so it is simply the current heap.
• (2) has \old[a] as its closest parent \old, so it is evaluated in the heap at label a
• (3) is evaluated in the heap at label b
• (4) is evaluated at label c
• (5) is evaluated at label d, which is the same heap that (1) is evaluated with

Now, why is the answer 6006? This is because the expression z.f is evaluated with an old heap, but not with an older value of the variable z. Thus: it only counts that z aliases the same object as y when we enter the assertion. The value for y.f at all our heaps are, repspectively:

• (1) y.f == 2, since we just assigned it
• (2) y.f == 2, since an assignment to x has no effect on y
• (3) y.f == 2, idem
• (4) y.f == 3000, since we just assigned it
• (5) y.f == 3000 still, since the heap at (1) is the same heap as at label d

[!NOTE] This is just an illustrative example, and as a matter of style you should try to keep the expression you evaluate in an \old as small as possible. Certainly it should not be necessary to nest them.

Another important detail is how \old interacts with \unfolding. (In case you are reading this tutorial in order, you can come back to this section after reading about predicates). The intuition is that \unfolding takes the current heap, and temporarily unfolds a predicate while its body is evaluated, whereas \old discards the current heap and replaces it with a different one. The consequence of this is that nesting them can lead to unexpected effects:

• An \unfolding nested in an \old: first the \old has replaced the current heap, after which the \unfolding unfolds a predicate in the old heap
• An \old nested in an \unfolding: first the \unfolding unfolds a predicate in the current heap, but this action is thrown away by \old, since it replaces the entire heap.

An example of the second situation is a program like this:

class Problem {  
  int x;
  resource state() = Perm(x, 1);

  requires state();
  //                                                   [-
  ensures state() ** (\unfolding state() \in (x == \old(x) + 1));
  //                                                    -]
  // ERROR: There may be insufficient permission to access this field here
  void inc() {
    unfold state();
    x++;
    fold state();
  }
}

It is clear what the intended behaviour is: we simply want to relate the value of x between the pre- and postcondition, so we temporarily unfold it and compare the values. This does not work, because the \old nested under \unfolding replaces the whole heap with a heap as it was just past the precondition. In this heap, we can derive from the precondition that it just contains state(), so we do not have permission to x.

The solution is to unfold twice: once in the current heap, and once in the old heap. We first have to enter the old heap before we unfold its state.

class Solution {  
  int x;
  resource state() = Perm(x, 1);

  requires state();
  ensures state() ** (\unfolding state() \in x) == \old((\unfolding state() \in x)) + 1;
  // Verified
  void inc() {
    unfold state();
    x++;
    fold state();
  }
}

GPGPU Verification

This section explains how to verify GPGPU programs in VerCors. The tool supports both OpenCL and CUDA languages. The synchronization feature (i.e., barrier) in these languages is also supported by VerCors. To demonstrate GPGPU verification, we show two examples in both OpenCl and CUDA, one without barrier and the other one with barrier.

OpenCL/CUDA without Barrier

This simple method shows an OpenCL program that adds two arrays and stores the result in another array:

#include <opencl.h>
/* 1  */ /*@
         context \pointer_index(a, get_global_id(0), read);
         context \pointer_index(b, get_global_id(0), read);
         context \pointer_index(c, get_global_id(0), write);
         ensures c[get_global_id(0)] == a[get_global_id(0)] + b[get_global_id(0)];
         @*/
/* 7  */ __kernel void openCLAdd(int a[], int b[], int c[]) {
/* 8  */    int tid = get_global_id(0);
/* 9  */    c[tid] = a[tid] + b[tid];
/* 10 */ }  

and this method shows the same example in CUDA:

#include <cuda.h>
/* 1  */  /*@
          context \pointer_index(a, threadIdx.x, read);
          context \pointer_index(b, threadIdx.x, read);
          context \pointer_index(c, threadIdx.x, write);
          ensures c[threadIdx.x] == a[threadIdx.x] + b[threadIdx.x];
          @*/
/* 7  */  __global__ void CUDAAdd(int a[], int b[], int c[]) {
/* 8  */     int tid = threadIdx.x;
/* 9  */     c[tid] = a[tid] + b[tid];
/* 10 */  }  

In both examples, first we should include the header files (i.g., opencl.h and cuda.h). Next we obtain thread identifiers and then each thread does the computation (lines 8-9 of OpenCL and 8-9 of CUDA examples). As we can see obtaining the global thread identifiers are different in OpenCL and CUDA.

In the specification of the methods, we specify read permission for each thread in arrays "a" and "b" and write permission in array "c" as pre- and postcondition. The keyword "\pointer_index" is used with three arguments, array name, index and permission to indicate which thread has what permission to which location. Finally in the last postcondition we specify the result of the methods that each location in array "c" contains the sum of the values in the corresponding locations in arrays "a" and "b". Note that in the specification we can use the shorthand keyword "\gid" instead of "get_global_id(0)" and "threadIdx.x" in the tool.

Note: In CUDA, to compute the global id, normally threadIdx is combined with blockDim. Unfortunately, blockDim is not yet supported in VerCors, so the examples in this chapter only use threadIdx.

OpenCL/CUDA with Barrier

In GPU programming, when there is only one thread block, there is a mechanism to sunchronize threads. This example shows an OpenCL program that uses barrier to synchronize threads:

#include <opencl.h>
/* 1  */ 
/* 2  */
/* 3  */ /*@
         context_everywhere opencl_gcount == 1;
         context_everywhere array != null && array.length == size;
         requires get_local_id(0) != size-1 ==> \pointer_index(array, get_local_id(0)+1, 1\2);
         requires get_local_id(0) == size-1 ==> \pointer_index(array, 0, 1\2);
         ensures \pointer_index(array, get_local_id(0), 1);
         ensures get_local_id(0) != size-1 ==> array[get_local_id(0)] == \old(array[get_local_id(0)+1]);
         ensures get_local_id(0) == size-1 ==> array[get_local_id(0)] == \old(array[0]);
         @*/
/* 12 */ __kernel void openCLLeftRotation(int array[], int size) {
/* 13 */    int tid = get_local_id(0);
/* 14 */    int temp;
/* 15 */    if(tid != size-1){
/* 16 */     temp = array[tid+1];
/* 17 */    }else{
/* 18 */     temp = array[0];
/* 19 */    }
/* 20 */
/* 21 */    /*@
            requires get_local_id(0) != size-1 ==> \pointer_index(array, get_local_id(0)+1, 1\2);
            requires get_local_id(0) == size-1 ==> \pointer_index(array, 0, 1\2);
            ensures \pointer_index(array, get_local_id(0), 1);
            @*/
/* 26 */    barrier(CLK_LOCAL_MEM_FENCE);
/* 27 */
/* 28 */    array[tid] = temp;
/* 29 */ }  

And this is the CUDA version of the example:

#include <cuda.h>
/* 1  */ 
/* 2  */
/* 3  */ /*@
         context_everywhere opencl_gcount == 1;
         context_everywhere array.length == size;
         requires threadIdx.x != size-1 ==> \pointer_index(array, threadIdx.x+1, 1\2);
         requires threadIdx.x == size-1 ==> \pointer_index(array, 0, 1\2);
         ensures \pointer_index(array, threadIdx.x, 1);
         ensures threadIdx.x != size-1 ==> array[threadIdx.x] == \old(array[threadIdx.x+1]);
         ensures threadIdx.x == size-1 ==> array[threadIdx.x] == \old(array[0]);
         @*/
/* 12 */ __global__ void CUDALeftRotation(int array[], int size) {
/* 13 */    int tid = threadIdx.x;
/* 14 */    int temp;
/* 15 */    if(tid != size-1){
/* 16 */     temp = array[tid+1];
/* 17 */    }else{
/* 18 */     temp = array[0];
/* 19 */    }
/* 20 */
/* 21 */    /*@
            requires threadIdx.x != size-1 ==> \pointer_index(array, threadIdx.x+1, 1\2);
            requires threadIdx.x == size-1 ==> \pointer_index(array, 0, 1\2);
            ensures \pointer_index(array, threadIdx.x, 1);
            @*/
/* 26 */    __syncthreads();
/* 27 */
/* 28 */    array[tid] = temp;
/* 29 */ }  

The above examples illustrate GPU programs that rotates the elements of an array to the left. Each thread ("tid") stores its right neighbor in a temporary location (i.e., "temp"), except thread "size-1" which stores the first element in the array (lines 15-19). Then each thread synchronizes in a barrier (line 26). After that, each thread writes the value read into its own location at index "tid" in the array (line 28).

We specify that there is only one thread block in the specification of the programs using the keyword "opencl_gcount" (the first precondition). The precondition of the barrier follows from the precondition of the function and the computations before the barrier. If the precondition of the barrier holds, the postcondition can be assumed after the barrier. Then, the postcondition of the method can follow from the postcondition of the barrier. Note that in the specification we can use the shorthand keyword "\lid" instead of "get_local_id(0)" and "threadIdx.x" in the tool.

Axiomatic Data Types

This section discusses axiomatic data types supported by VerCors.

Axiomatic data types are data types that are defined by a set of uninterpreted functions and axioms that define the behavior of these functions. This is in contrast to concrete data types which are defined by their implementation in a programming language such as Java or C++. Axiomatic datatypes are not to be confused with algebraic datatypes.

In the sections below, we are going to go over all ADTs supported by VerCors, give the definition of each, and show examples of common operations defined on them. A reference table can be found at the end showing all the operations defined on the ADTs.

The axiomatizations used by VerCors and its back end Viper can be found here (for sequences sets and bags) and here (for the other ADTs).

Finally, it is also possible to create custom ADTs, though with limited syntax support. This is discussed at the end of this section.

Sequence

Sequences are an ordered/enumerated collection also commonly referred to as lists. Sequences are finite and immutable (i.e. once created they cannot be altered).

There are two ways to construct a sequence: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the sequence to be explicitly defined. For example, s1 is a sequence of integers initialized with the values 1, 2 and 3 and s2 is an empty sequence of integers.

seq<int> s1 = seq<int> { 1, 2, 3 };
seq<int> s2 = seq<int> { };

The implicit syntax is a shorter syntax. If the sequence is initialized with at least one value (using the implicit syntax), VerCors infers the type of the sequence. An empty sequence can be constructed by providing the type of the sequence. For example, s3 is equivalent to s1 and s4 is equivalent to s2. Notice how there is no space between [ and t, this is mandated by the VerCors grammar.

seq<int> s3 = [ 1, 2, 3 ];
seq<int> s4 = [t: int ];

Once we have a sequence, we can query different properties of that sequence. The syntax s5[i] can be used to retrieve the element at index i from sequence s5. The notation s5.head is shorthand for s5[0]. The length of a sequence s5 can be obtained by using the notation |s5|. Two sequences can be compared using the == operator where they are equal iff they are of the same length and the elements at the same indices are equal.

seq<int> s5 = [ 1, 2, 4, 8, 16 ];
assert s5[3] == 8;
assert |s5| == 5;
assert s5 == seq<int> { 1, 2, 4, 8, 16 };

Constructing sequences from existing sequences

As mentioned above sequences are immutable, however it is possible to construct a new sequence from an existing sequence.

Elements can be added to a sequence in two ways. The first way is by concatenating two sequences s6 + s7. This expression represents a new sequence with the elements of s6 followed by the elements of s7. The second way is to add a single value to the front of a sequence. The syntax e::s6 is used to prepend e at the front of s6.

seq<int> s6 = [ 1, 2, 4, 8, 16 ];
assert 0::s6 == [ 0, 1, 2, 4, 8, 16 ];

seq<int> s7 = [ 32, 64, 128 ];
assert s6 + s7 == [ 1, 2, 4, 8, 16, 32, 64, 128 ];

It is also possible to take a subsequence from an existing sequence. The syntax s8[i..j] is used to take the elements from s8 from index i to index j (exclusive). By omitting either the lower bound or upper bound, one can take or drop from a sequence. The notation s8.tail can be used as a shorthand for s8[1..].

seq<int> s8 = [ 1, 2, 4, 8, 16 ];
assert s8[1..4] == [ 2, 4, 8 ];
assert s8[..2] == [ 1, 2 ];
assert s8.tail == s8[1..]; 

Examples

Sortedness

Sortedness is a property that is often used in the verification of sorting algorithms. The sortedness property for a sequence of integers could be defined as follows:

pure boolean sorted(seq<int> xs) = (\forall int i ; 0 <= i && i < |xs|-1; xs[i] <= xs[i+1]);

Distinct Element

Another property on sequences is the uniqueness of the elements. This property could be expressed for a sequence of integers as follows:

pure boolean distinct(seq<int> s) =
    (\forall int i; 0 <= i && i < s.length; 
        (\forall int j; 0 <= j && j < s.length && s[i] == s[j]; i == j)
    );

Maximum element

Recursive functions are often used to transform or reduce a sequence. The example below goes over a sequence to get its maximum value. This function could be defined for a sequence of integers as follows:

requires |xs| > 0;
ensures (\forall int i; 0 <= i && i < |xs|; xs[i] <= \result);
pure static int max(seq<int> xs) =
    1 == |xs| ?
        xs[0]:
        (xs[0] > max(xs[1..]) ?
            xs[0]:
            max(xs[1..]
        )
);

Set

Sets are an unordered collection with unique values. Sets are finite and immutable (i.e. once created they cannot be altered).

Similar to sequences, there are two ways to construct a set: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the set explicitly defined. For example, s1 is a set of integers initialized with the values 1, 2 and 3 and s2 is an empty set of integers.

set<int> s1 = set<int> { 1, 2, 3, 2 };
set<int> s2 = set<int> { };

The implicit syntax is a shorter syntax. If the set is initialized with at least one value (using the implicit syntax), VerCors infers the type of the set. An empty set can be constructed by providing the type of the set. For example, s3 is equivalent to s1 and s4 is equivalent to s2. Notice how there is no space between { and t, this is mandated by the VerCors grammar.

set<int> s3 = { 1, 2, 2, 3 };
set<int> s4 = {t: int };

Once we have a set, we can query different properties of that set. The length of a set s5 can be obtained by using the notation |s5|. Two set s6 and s7 can be compared using the == operator where they are equal iff all elements of s6 are in s7 and all elements of s7 are in s6. The syntax e1 \in s8 is used to check if set s8 contains the element e1. The < and <= operators denote the strict subset and subset operators respectively.

set<int> s5 = { 1, 2, 2, 3 };
set<int> s6 = { 3, 4, 5, 6 };
set<int> s7 = { 1, 2 };
set<int> s8 = { 2, 3 };
int e1 = 3;

assert |s5| == 3;
assert s6 != s7;
assert e1 \in s8;
assert s8 < s5;

Constructing sets from existing sets

As mentioned above sets are immutable, however it is possible to construct a new set from an existing set.

There are several operations defined on sets that are part of set theory. The union of two sets is denoted by s5 + s6, the difference between two sets is denoted by s5 - s6 and the intersection of two sets is denoted by s5 * s6.

set<int> s5 = { 1, 2, 2, 3 };
set<int> s6 = { 3, 4, 5, 6 };

assert s5 + s6 == { 1, 2, 3, 4, 5, 6 };
assert s5 - s6 == { 1, 2 };
assert s6 - s5 == { 4, 5, 6};
assert s5 * s6 == { 3 };

Set comprehension

Please note that set comprehensions are currently not supported.

An advanced way to create a set is using set comprehension. The syntax is set<T> { main | variables; selector } and consists of three parts: the main, the variables and the selector.

The variables are the variables that are quantified over and these variables can be bound or unbound. From the quantified variables, we can select specific values by using the selector expression. This is a Boolean expression that selects (a part of) the quantified variables. With the selected set of variables to quantify over, we express the value that is going to be part of the resulting set using the main expression.

For example, we can construct the set of all even integers from 0 to 9 as follows:

set<int> {x | int x <- {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; x % 2 == 0};

To use more complex main expressions (i.e. non-identity functions), it is recommended to wrap the expression in a function and use that function in the main expression. For example, suppose we have a set of integers from 0 to 5 (inclusive) and we want to construct the set of integers where each element is doubled, we could use set comprehension as follows:

class SetComp {
    requires 0 <= j && j < 5;
    void myMethod(int j) {
       set<int> a = set<int> {SetComp.plus(x, x) | int x; x >= 0 && x <= 5 };
       assert plus(1, 1) in a; 
       assert plus(j, j) in a; 
    }

    pure static int plus(int a, int b) = a+b;
}

Here we define a function plus to wrap the expression a+b and use an invokation of the plus function as the main of our set comprehension.

Bag

A bag (also called a multiset) is an unordered collection. They are equivalent to sequences without order, or sets with duplicates. Bags are finite and immutable (i.e. once created they cannot be altered).

Similar to sequences and sets, there are two ways to construct a bag: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the bag explicitly defined. For example, b1 is a bag of integers initialized with the values 1, 2, 2 and 3 and b2 is an empty bag of integers.

bag<int> b1 = bag<int> { 1, 2, 3, 2 };
bag<int> b2 = bag<int> { };

The implicit syntax is a shorter syntax. If the bag is initialized with at least one value (using the implicit syntax), VerCors infers the type of the bag. An empty bag can be constructed by providing the type of the bag. For example, b3 is equivalent to b1 and b4 is equivalent to b2. Notice how there is no space between b{ and t, this is mandated by the VerCors grammar.

bag<int> b3 = b{ 1, 2, 2, 3 };
bag<int> b4 = b{t: int };

Once we have a bag, we can query different properties of that bag. The length of a bag b5 can be obtained by using the notation |b5|. The syntax e1 \in b6 is used to get the multiplicity (or number of occurrences) of an element e1 in the bag b6. Two bags b7 and b8 can be compared using the == operator where they are equal iff for all elements e2, the multiplicity of e2 in b7 and b8 are equal. The < and <= operators denote the strict subset and subset operators respectively.

bag<int> b5 = b{ 1, 2, 2, 3 };
bag<int> b6 = b{ 3, 4, 5, 6, 5 };
bag<int> b7 = b{ 1, 2, 3, 2, 2, 6 };
bag<int> b8 = b{ 6, 1, 2, 2, 2, 3 };
int e1 = 5;


assert |b5| == 4;
assert (e1 \in b6) == 2;
assert b5 <= b7 && b5 < b8;
assert b7 == b8;

Constructing bags from existing bags

As mentioned above bags are immutable, however it is possible to construct a new bag from an existing bag.

The union of two bags is denoted by b9 + b10, the difference between two bags is denoted by b11 - b12 and the intersection of two bags is denoted by b13 * b14.

bag<int> b9 = bag<int> { 3 };
bag<int> b10 = bag<int> { 3, 4 };
bag<int> b11 = bag<int> { 1, 2, 2, 3 };
bag<int> b12 = bag<int> { 2, 3, 3, 4 };
bag<int> b13 = bag<int> { 1, 1, 2, 3 };
bag<int> b14 = bag<int> { 2, 3, 3, 4 };

assert b9 + b10 == bag<int> { 3, 3, 4 };
assert b12 - b11 == bag<int> { 3, 4 };
assert b11 - b12 == bag<int> { 1, 2 };
assert b13 * b14 == bag<int> { 2, 3 };

Examples

TODO

Map

Maps are an unordered, collection of key/value pairs with unique keys. Maps are finite and immutable (i.e. once created they cannot be altered).

A map can be constructed using the syntax map<K,V> { k1 -> v1, k2 -> v2, ...}. This syntax constructs a map with keys/value pairs (k1, v1) and (k2, v2) (of type K and type V respectively). An empty map can be constructed by declaring no key/value pair.

map<int, boolean> m1 = map<int,boolean>{1 -> true, 2 -> true, 0 -> false};
map<int, boolean> m2 = map<int,boolean>{1 -> true, 2 -> true, 0 -> false, 1 -> false, 1 -> true};
assert m1 == m2;

Once we have a map, we can query different properties of that map. Given a key k1, we can get its associated value in map m1 using the syntax m1[k1] or m1.get(k1). The cardinality/size of the map can be queried using the syntax |m1| or m1.size. The size of a map is equivalent to the size of its key set. The key, value and key/value pair sets can be obtained using the notations m1.keys, m1.values and m1.items respectively.

map<int, boolean> m1 = map<int,boolean>{1 -> true, 2 -> true, 0 -> false};

assert |m1| == 3;
assert m1[0] == false;
assert m1[1] == true;
assert m1[2] == true;

assert m1.keys == { 1, 2, 0 };
assert m1.values == { true, false };
assert tuple<int, boolean> { 0, false } \in m1.items;
assert tuple<int, boolean> { 1, true } \in m1.items;
assert tuple<int, boolean> { 2, true } \in m1.items;

We can add a key/value pair (k4, v4) to the map m4 using the syntax m4.add(k4, v4). If the key was already present in m4, its value gets updated. We can also remove a key k5 from a map m5 using the function m5.remove(k5).

map<int, int> m1 = map<int,int>{};
map<int, int> m2 = m1.add(1, 1).add(2, 4).add(3, 9);
map<int, int> m3 = m2.remove(2);
map<int, int> m4 = m3.remove(3).remove(1);

assert |m1| == 0;
assert m2[1] == 1;
assert m2[2] == 4;
assert m2[3] == 9;

assert !(2 \in m3.keys);
assert m3[1] == 1;
assert m3[3] == 9;

assert |m4| == 0;

Examples

TODO

Tuple

A tuple is an ordered, immutable collection containing exactly two elements.

A tuple can be constructed using the syntax tuple<F,S> { fst, snd }. This syntax constructs a tuple with the first value fst of type F and the second value snd of type S. A tuple can also be deconstructed into its first and second value by using the functions t2.fst and t2.snd respectively. For example, a tuple t1 with values (1, false) is constructed as:

tuple<int, boolean> t1 = tuple<int, boolean> { 1, false };
assert t1.fst == 1;
assert t1.snd == false;

Examples

TODO

Option

The option data type is a container that either represents the presence of an element in the container or the absence of it.

An option type can be constructed with the constructors Some(e) or None. The constructor Some(e) represents the presence of the value e in the option type and the constructor None represents the absence of an element.

option<int> o1 = None;
option<int> o2 = Some(3);

Option types can be compared to each other where two options o3 and o4 are equivalent iff they both contain an element e3 and e4 respectively and e3 equals e4, or both are empty.

option<int> o3 = Some(6);
option<int> o4 = Some(6);
option<int> o5 = Some(1);
option<int> o6 = None;

assert o3 == o4;
assert o4 != o5;
assert o5 != o6;

Examples

TODO

ADT Reference

The tables below are a reference for all the functions/operations that are defined on the different ADTs.

Sequence

Set

Bag

Map

Tuple

Option

Custom ADTs

ADTs can be useful to provide VerCors with domain-specific assumptions. For example, a custom int-tuple ADT can be defined in PVL as follows:

adt MyTuple {
  pure MyTuple cons(int l, int r);
  pure int left(MyTuple t);
  pure int right(MyTuple t);

  axiom (\forall int l, int r; left(cons(l, r)) == l);
  axiom (\forall int l, int r; right(cons(l, r)) == r);
  axiom (\forall int l1, int l2, int r1, int r2; 
    (cons(l1, r1) == cons(l2, r2)) ==> (l1 == l2 && r1 == r2));
}

void testTuple(MyTuple t) {
  assert MyTuple.cons(1, 2) == MyTuple.cons(1, 2);
  assert MyTuple.cons(1, 2) != MyTuple.cons(3, 4);
}

Note however that it is easy to make mistakes and define axioms from which false can be derived. If this happens, and your custom ADT is used in your code or contracts, from that point on VerCors assumes false, which makes every proof obligation after that point trivial to prove. Furthermore, when writing quantifiers in ADTs it is important to also define triggers. VerCors and its backend can often infer some trigger, but these are usually suboptimal.

Custom ADTs are supported in all frontends.

Arrays and Pointers

This tutorial explains how to specify arrays and pointers in vercors. Java and PVL support arrays, whereas C and the GPGPU frontends only support pointers. The tutorial assumes you are familiar with arrays and pointers already.

Array permissions

We have learned already how to specify ownership of variables on the heap. Arrays generalize this concept by treating each element of the array as a separate location on the heap. For example, you might specify:

/*@
requires ar != null && ar.length == 3;
context Perm(ar[0], write) ** Perm(ar[1], write) ** Perm(ar[2], write);
*/
void example1(int[] ar);

This means we require the length to be 3, and require and return permission over each of the elements of the array. Length is treated in a special way here: even though it is a "field", we do not need permission to read it, because the length of an array cannot be changed and it is baked into Vercors.

Of course writing a specific length and manually asserting permission over each location is cumbersome, so we can write a contract that accepts arrays of any length as such:

/*@
requires ar != null;
context (\forall* int i; 0 <= i && i < ar.length; Perm(ar[i], write));
*/
void example2(int[] ar);

As mentioned in the permissions tutorial, the permissions are combined with ** to Perm(ar[0], write) ** Perm(ar[1], write) ** … ** Perm(ar[ar.length-1], write). Please note the * after forall, which denotes that the body of the forall is combined with separating conjunction (**) and not boolean conjunction (&&).

As you might expect, we can also use forall to specify properties about the values of the array:

/*@
requires ar != null;
context (\forall* int i; 0 <= i && i < ar.length; Perm(ar[i], write));
ensures (\forall int i; 0 <= && i < ar.length; ar[i] == i);
*/
void identity(int[] ar) {
    for(int i = 0; i < ar.length; i++)
    /*@
    loop_invariant (\forall* int i; 0 <= i && i < ar.length; Perm(ar[i], write));
    loop_invariant (\forall int j; 0 <= j && j < i; ar[j] == j); */
    {
        ar[i] = i;
    }
}

Syntactic sugar

Specifying arrays quickly leads to prefix a lot of statements with \forall* int i; 0 <= i && i < ar.length;, so there is some syntactic sugar. First, you might want to use context_everywhere for the permission specification of the array, so that it is automatically propagates to loop invariants:

/*@
context_everywhere (\forall* int i; 0 <= i && i < ar.length; Perm(ar[i], write));
ensures (\forall int i; 0 <= && i < ar.length; ar[i] == i);
*/
void identity(int[] ar) {
    for(int i = 0; i < ar.length; i++)
    /*@
    loop_invariant (\forall int j; 0 <= j && j < i; ar[j] == j); */
    {
        ar[i] = i;
    }
}

This whole forall* can also be written as Perm(ar[*], write), which still means write permission over all the elements of the array:

/*@
requires ar != null;
context_everywhere Perm(ar[*], write);
ensures (\forall int i; 0 <= && i < ar.length; ar[i] == i);
*/
void identity(int[] ar) {
    for(int i = 0; i < ar.length; i++)
    /*@
    loop_invariant (\forall int j; 0 <= j && j < i; ar[j] == j); */
    {
        ar[i] = i;
    }
}

If you want to specify the length of an array, you can write as well: \array(ar, N) which is equivalent to ar != null && ar.length == N. More interestingly, there is also \matrix(mat, M, N), which is equivalent to:

mat != null ** mat.length == M **
(\forall* int i; 0 <= i && i < M; Perm(mat[i], read)) **
(\forall int i; 0 <= i && i < M; mat[i].length == N) **
(\forall int i; 0 <= i && i < M; (\forall int j; 0 <= j && j < M && mat[i] == mat[j]; i == j))

The last line is interesting here. In Java there is no such thing as a true matrix: instead we can make an array of arrays. However, there is nothing preventing you from putting the same row array instance in multiple rows. The last statement says that if we have valid row indices i, j, we know that i != j ==> mat[i] != mat[j] (and the contrapositive).

Pointers

Pointers themselves are quite well-supported, but we don't support casting and structs in C, making the end result quite limited. For the support that we do have, pointers can be specified with two constructs: \pointer and \pointer_index.

We write \pointer(p, size, perm) to express that p != NULL, the pointer p is valid from (at least) 0 to size-1, and we assert perm permission over those locations.

We write \pointer_index(p, index, perm) to express that p != NULL, (p+i) is a valid location, and we have permission perm at that location.

/*@
requires \pointer(a, 10, write);
*/
void test(int *a) {
    //@ assert \pointer(a, 10, write);
    //@ assert \pointer(a, 8, write);
    //@ assert (\forall* int i; 0 <= i && i < 10; \pointer_index(a, i, write));
    int *b = a+5;
    //@ assert a[5] == b[0];
    //@ assert \pointer(b, 5, write);
}

Injectivity, object arrays and efficient verification

This section contains advanced information, and can be skipped on a first read.

Due to a technical limitation in the backend of VerCors, the location denoted by a permission expression in a quantified expression must be unique for each binding of the quantifier. For example, if we write:

class Box {
    int value;

    void test() {
        Box box1 = new Box();
        seq<Box> boxes = seq<Box>{box1, box1};
        exhale (\forall* int i; 0 <= i && i < |boxes|; Perm(boxes[i].value, 1\10));
    }
}

This could be correct: we only exhale 2\10 permission of box1.value. The expression is however not well-formed: i==0 and i==1 cause the expression boxes[i].value to point to the same location. (Please note that it seems that the error from our backend currently is not propagated correctly. Silicon reports "Receiver of boxes[i].value might not be injective." and VerCors translates this into "ExhaleFailed:InsufficientPermission".)

The reason we refer to this as injectivity, is that we should be able to construct a function that assigns bindings for a location, e.g. for a given Box we can either find a unique i that points to the Box, or the Box does not appear in boxes. That function is the inverse of the expression in the Perm. The truth value of a \forall* carries with it this property of injectivity. This means, for example, that in a method definition a requirement assumes that \forall* statements are injective with repsect to locations, whereas we must prove it in ensures statements. This usually follows directly from a requirement. In method invokations then as per usual it's the opposite: we must prove that \forall* statements in the requirements are injective and may assume it for ensures statements.

This limitation is especially important in for example arrays of objects:

class Box {
    int value;

    requires a != null ** (\forall* int i; 0 <= i && i < a.length; Perm(a[i], read));
    requires (\forall* int i; 0 <= i && i < a.length; a[i] != null ** Perm(a[i].value, write));
    void test(Box[] a) {
        
    }

    void foo() {
        Box box = new Box();
        Box[] boxes = new Box[2];
        boxes[0] = box;
        boxes[1] = box;
        test(boxes); // fails
    }
}

In common use however we have to know about duplicate elements anyway. For example, in the example above we require write permission over the boxes, so indirectly we already require all the boxes to be distinct. As for the array elements themselves: we have an internal axiom about arrays that expresses exactly that the locations of an array correspond to only one index and one array.

Parallel Blocks

In this section we explain how to verify parallel algorithms by creating parallel blocks in PVL. First, we give an example of a simple method using parallel block. Then, we discuss a more complex example with a barrier inside the parallel block. A barrier is used to synchronize threads inside a parallel block.

Simple Parallel Blocks

Parallel Block without Barrier

This example shows a simple method that adds two arrays in parallel and stores the result in another array:

/* 1  */ context_everywhere a != null && b != null && c != null;
/* 2  */ context_everywhere a.length == size && b.length == size && c.length == size;
/* 3  */ context (\forall* int i; i >= 0 &&  i < size; Perm(a[i], 1\2));
/* 4  */ context (\forall* int i; i >= 0 &&  i < size; Perm(b[i], 1\2));
/* 5  */ context (\forall* int i; i >= 0 &&  i < size; Perm(c[i], 1));
/* 6  */ ensures (\forall int i; i >= 0 &&  i < size; c[i] == a[i] + b[i]);
/* 7  */ void Add(int[] a, int[] b, int[] c, int size){
/* 8  */
/* 9  */    par threads (int tid = 0 .. size)
/* 10 */     context Perm(a[tid], 1\2) ** Perm(b[tid], 1\2) ** Perm(c[tid], 1);
/* 11 */     ensures c[tid] == a[tid] + b[tid];
/* 12 */    {
/* 13 */       c[tid] = a[tid] + b[tid];
/* 14 */    }
/* 15 */  }

In this method there is a parallel block (lines 9-14) named "threads". The keyword "par" is used to define a parallel block, followed by an arbitrary name after that defines the name of that block. Moreover, we define the number of threads in the parallel block as well as a name for the thread identifier. In this example, we have "size" threads in the range from 0 to "size-1" and "tid" is used as thread identifier to refer to each thread.

In addition to the specification of the method (lines 1-6), we add thread-level specification to the parallel block (lines 10-11). The precondition of the method indicates that we have read permission over all locations in arrays "a" and "b" and write permission for array "c" (lines 3-5). In the parallel block, we specify that each thread ("tid") has read permission to its own location in arrays "a" and "b" and write permission to its own location in array "c" (line 10). After termination of the parallel block as postcondition (1) we have the same permission (line 10) and (2) the result of each location in array "c" is the sum of the two corresponding locations in arrays "a" and "b" (line 11). From the postcondition of the parallel block, we can derive the postcondition of the method using universal quantifier for all locations in the arrays (line 3-6).

Parallel Block with Barrier

Next we show an example of a parallel block which uses a barrier to synchronize threads:

/* 1  */ context_everywhere array != null && array.length == size;
/* 2  */ requires (\forall* int i; i >= 0 &&  i < size; Perm(array[i], write));
/* 3  */ ensures (\forall* int i; i >= 0 &&  i < size; Perm(array[i], write));
/* 4  */ ensures (\forall int i; i >= 0 &&  i < size; (i != size-1 ==> array[i] == \old(array[i+1])) && 
/* 5  */                                              (i == size-1 ==> array[i] == \old(array[0])) );
/* 6  */ void leftRotation(int[] array, int size){
/* 7  */
/* 8  */   par threads (int tid = 0 .. size)
/* 9  */    requires tid != size-1 ==> Perm(array[tid+1], write);
/* 10 */    requires tid == size-1 ==> Perm(array[0], write);
/* 11 */    ensures Perm(array[tid], write);
/* 12 */    ensures tid != size-1 ==> array[tid] == \old(array[tid+1]);
/* 13 */    ensures tid == size-1 ==> array[tid] == \old(array[0]);
/* 14 */   {
/* 15 */      int temp;
/* 16 */      if (tid != size-1) {
/* 17 */        temp = array[tid+1];
/* 18 */      } else {
/* 19 */        temp = array[0];
/* 20 */      }
/* 21 */
/* 22 */      barrier(threads)
/* 23 */      requires tid != size-1 ==> Perm(array[tid+1], write);
/* 24 */      requires tid == size-1 ==> Perm(array[0], write);
/* 25 */      ensures Perm(array[tid], write);
/* 26 */      { /* Automatic proof */ }
/* 27 */
/* 28 */      array[tid] = temp;
/* 29 */   }
/* 30 */ }

This example illustrates a method named "leftRotation" that rotates the elements of an array to the left. In this example, we also have "size" threads in the range from 0 to "size-1" and "tid" is used as thread identifier. Inside the parallel block each thread ("tid") stores its right neighbor in a temporary location (i.e., "temp"), except thread "size-1" which stores the first element in the array (lines 15-20). Then each thread synchronizes at the barrier (line 22). The keyword "barrier" and the name of the parallel block as an argument (e.g., "threads" in the example) are used to define a barrier in PVL. After that, each thread writes the value read into its own location at index "tid" in the array (line 28).

To verify this method in VerCors, we annotate the barrier, in addition to the method and the parallel block. As precondition of the method, we have read permission over all locations in the array (line 2). At the beginning of the parallel block, each thread reads from its right neighbor, except thread "size-1" which reads from location 0 (lines 16-20). Therefore, we specify read permissions as precondition of the parallel block in lines 9-10. Since after the barrier each thread ("tid") writes into its own location at index ("tid"), we change the permissions in the barrier in such that each thread has write permissions to its own location (lines 23-25). When a thread reaches the barrier, it has to fulfill the barrier preconditions, and then it may assume the barrier postconditions. Moreover, the barrier postconditions must follow from the barrier preconditions.

As postcondition of the parallel block (1) first each thread has write permission to its own location (this comes from the postcondition of the barrier) in line 11 and (2) the elements are truly shifted to the left (lines 12-13). From the postcondition of the parallel block, we can establish the same postcondition for the method (lines 3-5).

Caution: barrier syntax

In this chapter syntax is introduced for barriers. There is a caveat to using barriers, which we want to explain first so it is not missed. Barrier syntax in VerCors has two forms. Form 1:

barrier(barrierName) {
  requires P;
  ensures Q;
}

Form 2:

barrier(barrierName)
  requires P;
  ensures Q;
{ }

Notice how in form 1, the contract is inside the curly braces. In form 2, the contract resides between the barrier declaration and the curly braces.

There is a big difference between these two syntaxes. In form 1, the contract of the barrier is not actually checked by VerCors. This means that if you would add ensures false; to your barrier using the syntax of form 1, VerCors will not indicate this is a problematic contract. For form 2, however, the contract is actually checked. Therefore, when using barriers, form 2 should be preferred. Form 1 should only be used if there is a proof external to VerCors.

Complicated Parallel Blocks

Nested Parallel Blocks

In the previous examples, we defined a parallel block of threads to work on one-dimensional arrays. It is also possible to define two-dimensional thread layouts to work on two-dimensional arrays. As an example we define a two-dimensional thread layout to transpose a matrix in parallel:

context_everywhere inp != null && out != null; /// && out == size;
context_everywhere inp.length == size && out.length == size; 
context_everywhere (\forall int i; 0 <= i && i < size; inp[i].length == size && out[i].length == size);
context (\forall* int i; 0 <= i && i < size; 
         (\forall* int j; 0 <= j && j < size; Perm(inp[i][j], read)));
context (\forall* int i; 0 <= i && i < size; 
         (\forall* int j; 0 <= j && j < size; Perm(out[i][j], write)));
ensures (\forall* int i; 0 <= i && i < size; 
         (\forall* int j; 0 <= j && j < size; out[i][j] == inp[j][i]));
void transpose(int[][] inp, int[][] out, int size){

  par threadX (int tidX = 0 .. size)
   context (\forall* int i; i >= 0 && i < size; Perm(inp[i][tidX], read));
   context (\forall* int i; i >= 0 && i < size; Perm(out[tidX][i], write));
   ensures (\forall int i; i >= 0 && i < size; out[tidX][i] == inp[i][tidX]);
  {
    par threadY (int tidY = 0 .. size)
     context Perm(inp[tidY][tidX], read);
     context Perm(out[tidX][tidY], write);
     ensures out[tidX][tidY] == inp[tidY][tidX];
    {
      out[tidX][tidY] = inp[tidY][tidX]; 
    } 
  }
}

As we can see defining nested parallel blocks allow us to define thread layout in different dimensions. We can simplify the above example syntactically into one parallel block:

context_everywhere inp != null && out != null;
context_everywhere inp.length == size && out.length == size; 
context_everywhere (\forall int i; 0 <= i && i < size; inp[i].length == size && out[i].length == size);
context (\forall* int i; 0 <= i && i < size; 
         (\forall* int j; 0 <= j && j < size; Perm(inp[i][j], read)));
context (\forall* int i; 0 <= i && i < size; 
         (\forall* int j; 0 <= j && j < size; Perm(out[i][j], write)));
ensures (\forall int i; 0 <= i && i < size; 
         (\forall int j; 0 <= j && j < size; out[i][j] == inp[j][i]));
void transpose(int[][] inp, int[][] out, int size){

  par threadXY (int tidX = 0 .. size, int tidY = 0 .. size)
   context Perm(inp[tidY][tidX], read);
   context Perm(out[tidX][tidY], write);
   ensures out[tidX][tidY] == inp[tidY][tidX];
  {
    out[tidX][tidY] = inp[tidY][tidX]; 
  } 
}

Simultaneous Parallel Blocks

There might be some scenarios that we have multiple parallel blocks and all threads in each parallel block are working in disjoint memory locations. In this case we can define multiple parallel blocks to run simultaneously. That means, threads in each parallel block run independently of other threads in different parallel blocks. Below is an example of such a scenario:

/* 1  */ context_everywhere a != null && b != null && c != null;
/* 2  */ context_everywhere a.length == size && b.length == size && c.length == size; 
/* 3  */ context (\forall* int i; i >= 0 &&  i < size; Perm(a[i], write));
/* 4  */ context (\forall* int i; i >= 0 &&  i < size; Perm(b[i], write));
/* 5  */ context (\forall* int i; i >= 0 &&  i < size; Perm(c[i], write));
/* 6  */ ensures (\forall int i; i >= 0 &&  i < size; a[i] == \old(a[i]) + 1 && b[i] == \old(b[i]) + 1 && 
/* 7  */                                              c[i] == \old(c[i]) + 1);
/* 8  */ void simPar(int[] a, int[] b, int[] c, int size){
/* 9  */
/* 10 */   par thread1 (int tid1 = 0 .. size)
/* 11 */    context Perm(a[tid1], write);
/* 12 */    ensures a[tid1] == \old(a[tid1]) + 1;
/* 13 */   {
/* 14 */     a[tid1] = a[tid1] + 1; 
/* 15 */   } and
/* 16 */   thread2 (int tid2 = 0 .. size)
/* 17 */    context Perm(b[tid2], write);
/* 18 */    ensures b[tid2] == \old(b[tid2]) + 1;
/* 19 */   {
/* 20 */     b[tid2] = b[tid2] + 1;
/* 21 */   } and
/* 22 */   thread3 (int tid3 = 0 .. size)
/* 23 */    context Perm(c[tid3], write);
/* 24 */    ensures c[tid3] == \old(c[tid3]) + 1;
/* 25 */   {
/* 26 */     c[tid3] = c[tid3] + 1;
/* 27 */   }
/* 28 */ }

As we can see we use "and" between each parallel block (lines 15 and 21) to define simultaneous parallel blocks. This construction can be used in a situation where we decide to run simultaneous instructions. That means, we do not define threads in the parallel blocks, but the par blocks run simultaneously. Below is an example in this situation where "a", "b" and "c" are objects included a field "val":

class HasVal {
    int val;
}

class Main {
    context Perm(a.val, write) ** Perm(b.val, write) ** Perm(c.val, write);
    ensures a.val == \old(a.val) + 1 && b.val == \old(b.val) + 1 && c.val == \old(c.val) + 1;                                            
    void IncPar(HasVal a, HasVal b, HasVal c){
      par 
       context Perm(a.val, write);
       ensures a.val == \old(a.val) + 1;
      {
        a.val = a.val + 1; 
      } and
       context Perm(b.val, write);
       ensures b.val == \old(b.val) + 1;
      {
        b.val = b.val + 1;
      } and
       context Perm(c.val, write);
       ensures c.val == \old(c.val) + 1;
      {
        c.val = c.val + 1;
      }
    }
}

In the above example, for each object we increase its "val" by one in parallel. As we can see, thread blocks are without names and thread identifiers in this case.

Atomics and Locks

VerCors supports three forms of synchronization primitives. Two can only be used in PVL: built-in locks, and atomics. One can only be used in Java: the synchronized block. Each form will be discussed individually in the next sections.

Warning: at the time of writing, VerCors supports only non-reentrant locks. This means locking twice in a row is unsound, which could have implications for code that uses Java's synchronized. See the caveats section at the end of this document for more info.

PVL: Built-in locks

Using built-in locks in PVL consists of the following parts:

• Lock invariant, which describes the resources that the lock guards
• The lock statement
• The unlock statement
• The commit statement and committed(l) expression, which indicate whether or not a lock is initialized.

Lock invariant

A lock invariant can be defined for a class with the following syntax:

lock_invariant true /* or: resource expression involving permissions and boolean assertions */;
class C {

}

Because a lock invariant is defined for a class, it is always related to a specific class instance. Therefore, it is possible to make assertions about instance fields in the lock invariant. For example, a lock invariant could be specified that contains the permissions for a field, and also the fact that that field must have a value greater than 10, using the following syntax:

lock_invariant Perm(f, write) ** f > 10;
class C {
    int f;

    C() {
        f = 11;
        // Lock invariant must hold here!
    }
}

The lock invariant must hold at the end of the constructor. If VerCors cannot prove this, the program will be rejected.

Using Java terminology, in the above example the field f is "guarded" by the built-in lock of the object that has the field f. That is, to write permission for this.f, and hence access to this.f, first the lock on this needs to be acquired. This is done using the lock statement, which is described in the next section.

lock statement

The lock statement has the following syntax:

lock o;

Where o can be an arbitrary expression. The only constraint is that o is not null. The default lock invariant for a class is true, so by default lock o does not give you extra information, until a lock_invariant is specified.

The lock statement ensures that only one thread at a time can lock on an object. Once the lock has been acquired, the lock invariant of the object o may be assumed. For example, after the lock statement, often fields of the object o can be accessed or written to. For example, consider the code snippet below. It is similar to the previous example, with the addition of an increment method:

lock_invariant Perm(f, write);
class C {
    int f;

    void increment() {
        lock this;
        assert Perm(f, write);
        f = f + 1;
    }
}

Notice how the lock is acquired before f is incremented. Because after lock statement the lock invariant may be assumed, this ensures the thread that is executing increment has write permission for f, which in turn allows reading and writing to f. Additionally, this excludes any data races on f, as the thread that has the lock will be the only thread currently incrementing f.

The above example is still incomplete: when f has been incremented, the lock should be unlocked again. This is done with the unlock statement, which we describe next.

unlock statement

The unlock statement has the following syntax:

unlock o;

Similar to the lock statement, o must be non-null.

The unlock statement behaves as the inverse of the lock statement. For the program to progress beyond unlock, the lock invariant must be re-established. If this is not possible, VerCors will reject the program. If the lock invariant can be re-established, the lock is unlocked, and the program proceeds. Because the lock is now unlocked, other threads can lock it, and gain access to the resources protected by the lock.

In the code snippet, the previous code snippet is completed with the missing unlock statement:

lock_invariant Perm(f, write);
class C {
    int f;

    void increment() {
        lock this;
        assert Perm(f, write);
        f = f + 1;
        unlock this;
    }
}

Because the only thing we did between lock and unlock was increment f, the write permission for f is still available, and hence VerCors can trivially prove that the lock invariant can be re-established. Hence, this example verifies.

commit statement

Before a lock can be locked, it must be initialized. In VerCors, a lock is initialized when it is "committed". This is done using the commit e; statement. The lock must be committed before the end of the constructor. After any commit e; statement, the expression committed(e) is guaranteed to be true.

In the following example, the lock invariant of C requires permission for the field f, and that f has value 3. The constructor writes 3 to f, and then commits the invariant. This ensures that the tryLock method can lock on a newly created object of type C. Without the commit statement, an error would occur. In addition, the postcondition contains committed(this), to indicate that after the constructor the new object is lockable.

lock_invariant Perm(f, 1) ** f == 3;
class C {
  int f;

  ensures committed(this);
  constructor() {
    f = 3;
    commit this;
    assert committed(this);
  }
}

void tryLock() {
  C c = new C();
  lock c;
  assert Perm(c.f, 1) ** c.f == 3;
}

Built-in lock: caveats

There are several caveats to look out for when using built-in locks in PVL.

Avoid: locking a lock twice

PVL locks are non-reentrant: locking a lock twice, without unlocking the lock inbetween, will result in a deadlock. VerCors does not warn about this situation if it occurs. Hence, it needs to be checked manually that this situation does not occur.

Avoid: deadlocking interleavings

Deadlocks can occur when using multiple locks. For example, consider a situation with two locks, l1 and l2. Process A first locks l1, and then tries to acquire l2. Process B locks l2, and then tries to acquire l1. Since built-in locks in PVL are blocking, this interleaving will deadlock. VerCors does not warn about this situation if it occurs. Hence, it needs to be checked manually that this situation does not occur, because it can otherwise allow unsoundness to occur.

PVL: Atomics

For this section, we assume you are familiar with the concept of "lock invariant", as introduced int the previous section.

Atomics in PVL are used through two statements: the invariant statement and the atomic statement. We will discuss them separately.

invariant block

The syntax of the invariant block is as follows:

invariant invName(true) {
    // ...
}

An invariant block consists of the keyword invariant, then a name, and finally an expression that is the atomic invariant of the block. The invariant block may only occur in methods or procedures, and may be nested, provided that the names of each invariant block are unique.

The invariant block will ensure that the atomic invariant holds at the beginning of the block. Inside the invariant block, you will not have access to the atomic invariant, as it is removed from the state at the beginning of the invariant block. You can get access to the atomic invariant using the atomic block, which is explained in the next section. After the invariant block, the atomic invariant may be assumed again.

atomic block

The syntax of the atomic block is as follows:

atomic(invName) {
    // ...
}

The atomic block consists of the keyword atomic, followed by the name of the invariant the atomic block synchronizes on. The atomic block may only occur in methods or procedures, may not be nested, and the invariant that is referred to must enclose the atomic block.

The atomic block will ensure only one thread at a time will synchronize on the invariant. At the beginning of the atomic block, the atomic invariant is assumed. At any point in the atomic block, this atomic invariant can be used and broken. Finally, when the program exits the atomic block, the atomic invariant needs to be re-established. If VerCors cannot prove that this is always possible, VerCors will reject the program and verification will fail.

The atomic block is similar to the lock invariant and lock/unlock statements, with two subtle differences:

1. The synchronization done by the atomic block is scoped, so unlocking is done automatically.
2. Declaration of the invariant is done at the method level, instead of at the class level.

Java: synchronized

The synchronized statement allows you to work with lock invariants in Java. It is a combination of built-in locks from PVL, and atomics from PVL, which are both explained in previous sections. Specifically, VerCors supports the lock invariant syntax for Java classes, and synchronized blocks work almost identically to atomic blocks. Both concepts will be discussed in the next sections.

Java: lock invariants

VerCors supports the lock invariant syntax for Java classes. The syntax is as follows:

//@ lock_invariant true;
class C  {
    C() {
        // Lock invariant is established here!
    }
}

Notice how the syntax is identical to the PVL syntax, except that it must now be placed in ghost code, as indicated by the //@ marker. In the above example the trivial lock invariant true is used, but in principle the lock invariant can contain the same things as in PVL: permissions about fields, arrays, and properties about those fields and arrays.

The lock invariant has to hold at the end of a constructor, otherwise verification will fail. The lock invariant is assumed at the beginning of synchronized blocks, and has to be re-established at the end of synchronized blocks. If it cannot be re-established, VerCors will reject the program and verification will fail.

Java: synchronized block

VerCors supports Java's syntax for synchronized blocks. The syntax is as follows:

synchronized(expr) {
    // ...
}

Note the similarity to the atomic block statement. The only requirement is that expr is non-null and of type class. If no lock invariant is specified on the class, the default invariant true will be used.

The only additional behaviour of the synchronized expr is that it accounts for exceptions. That is, when an exception is thrown before the end of the synchronized block, the lock is still closed, and hence the lock invariant still needs to be re-established.

Caveats

There are some caveats to verifying Java locks in VerCors.

Avoid: locking in the constructor

Similar to PVL, VerCors does not allow locking on an object before the lock invariant is established. However, VerCors does not check for this, so the user must manually ensure that this does not occur.

Avoid: locking on an object twice

Similar to PVL, VerCors models Java's locks as single-entrant locks. This is inaccurate, as Java's locks are actually re-entrant. We are working on improving this, but this is currently not yet implemented. Therefore, users have to take care that locking twice on a single object does not occur. If it does occur, it might cause unsoundness.

Avoid: deadlocking interleavings

Some interleaving of synchronized locking sequences might deadlock. VerCors does not warn, nor check for this. Therefore, it is the user's responsibility to ensure that this does not occur.

Process Algebra Models

Process Algebra Models allow users to specify processes in PVL programs. PVL programs must then be annotated to indicate which locations in the program correspond to transitions in the process model. Properties specified in the process model may be assumed by VerCors at the locations in the program, provided that these properties of the process model are proven using an external tool, such as the model checker mCRL2.

Support for checking if a PVL program adheres to a process model is automatic, and implemented in VerCors 1.4.0. Checking if a process model adheres to the specified properties can be automated, but currently is not, and hence has to be done manually.

For the theoretical background on Process Algebra Models, we refer the reader to Wytse Oortwijn's PhD thesis: https://doi.org/10.3990/1.9789036548984.

For more practical sources, we refer the reader to the following urls:

1. https://github.com/wytseoortwijn/SupplementaryMaterialsThesis: The repository of supplementary materials of Wytse Oortwijn's PhD thesis
2. https://github.com/wytseoortwijn/csl-abstractions: Supplementary materials of "An Abstraction Technique for Verifying Shared-Memory Concurrency", which is a generalisation of chapter 5 of Wytse Oortwijn's PhD thesis
3. The VerCors example directory:
   • https://github.com/utwente-fmt/vercors/tree/dev/examples/futures
   • https://github.com/utwente-fmt/vercors/tree/dev/examples/known-problems/futures

For any aspects not covered by the above summary, please contact the VerCors team.

Predicates

This section discusses syntax and semantics of predicates. First a motivating example is given why predicates are needed. Then an overview is given of the syntax and semantics of predicates. The introductory example is then rewritten using predicates. Finally, we discuss some internal and reserved predicates, and finish this part of the tutorial with a brief overview of advanced usages of predicates and known problems.

In this section, the language used for the code examples is Java. However, the concepts presented apply to PVL as well.

Why predicates?

Permissions are useful for indicating access rights and modifications to data. But, adding permissions to private members in the contract leaks implementation details. Consider the following example:

class Counter {
  int count;
  
  //@ context Perm(count, write);
  //@ ensures count == \old(count) + n;
  void increment(int n);
}

class MyProgram {
  //@ requires c != null;
  //@ requires Perm(c.count, write);
  //@ requires c.count == 0;
  void foo(Counter c) {
    //@ assert c.count == 0;
    c.increment(2);
    //@ assert c.count == 2;
  }
}

It is clear from the contract of increment that it modifies the internal state of the Counter object. Therefore, when Counter changes its internal layout, client code will have to be modified as well. For example, if in the previous example Counter adds some internal field, the client code will also have to be changed. This is shown in the next example:

class CounterExtended {
  int count;
  int numIncrements;
  
  //@ context Perm(count, write) ** Perm(numIncrements, write);
  //@ ensures count == \old(count) + n;
  //@ ensures numIncrements == \old(numIncrements) + 1;
  void increment(int n);
}

class MyProgram {
  //@ requires c != null;
  //@ requires Perm(c.count, write) ** Perm(c.numIncrements, write);
  //@ requires c.count == 0;
  void foo(CounterExtended c) {
    //@ assert c.count == 0;
    c.increment(2);
    //@ assert c.count == 2;
  }
}

It is desirable that permissions are managed such that client code does not depend on irrelevant details, to avoid this rippling effect of modifications. Predicates help with this.

Predicate syntax and usage

A predicate is declared as follows:

//@ resource myPredicate(int a, bool b, ...) = body;

A predicate consists of the name of the predicate, zero or more arguments, and a body where arguments can be used. In Java, the declaration must be written as a verification annotation (e.g. using //@). In PVL, it is a plain declaration.

One can think of a predicate as a function returning type resource, similar to how a permission (Perm) is a resource. Except that, predicates are never called, but created and destroyed using unfold and folds. We will explain this next.

To create a predicate instance, the contents of the predicate body must be exchanged for a predicate instance. This is called "folding". Specifically, folding a predicate means any permissions present in the predicate body are removed from the program state. In return, an instance of the predicate is added to the state. In the following example folding is shown. The method foo receives a permission for the field x. At the end of the method, the permission for this field x has been exchanged for an instance of the predicate state. Note how the permission for x and the predicate state are mutually exclusive: both cannot be in the program state simultaneously.

int x;

//@ resource state(int val) = Perm(x, write) ** x == val;

//@ requires Perm(x, write) ** x == n;
//@ ensures state(n);
void foo(int n) {
    // Now we have Perm(x, write).
    //@ fold state(n);
    // Now Perm(x, write) is gone, but state(n) is present.
}

A predicate can also be "unfolded". This exchanges a predicate instance for its body.

int x;

//@ resource state(int val) = Perm(x, write) ** x == val;

//@ requires state(n);
//@ ensures Perm(x, write) ** x == n;
void foo(int n) {
    // Now we have state(n);
    //@ unfold state(n);
    // Now state(n) is gone, but Perm(x, write) is present.
}

The previous two examples also show that fields of the current class can be used in the predicate body. This is because a predicate instance is implicitly bound to an instance of the class it is defined in. The following example verifies, because the this part of the predicate instance is implicit. It also shows how to name predicates on objects other than this.

final class Cell {
    int x;

    //@ resource state(int val) = Perm(x, write) ** x == val;

    // "this" is implicit:
    //@ requires this.state(n);
    //@ ensures state(n);
    void foo(int n) {

    }

    // Predicates can appear on distinct objects too:
    //@ given int n;
    //@ given int m;
    //@ context other.state(m);
    //@ requires state(n);
    //@ ensures state(n+m);
    void combine(Cell other) {
        //@ unfold state(n);
        //@ unfold other.state(m);
        x += other.x;
        //@ fold other.state(m);
        //@ fold state(n+m);
    }
}

Predicates can be used anywhere Perm can be used, and hence must also be composed using the separating conjunction (**) operator.

The Counter example, now with predicates

In the next snippet we redefine the Counter class to use predicates, instead of plain permissions:

class Counter {
  int count;

  //@ resource state(int val) = Perm(count, write) ** count == val;
  
  //@ given int oldCount;
  //@ requires state(oldCount);
  //@ ensures state(oldCount + n);
  void increment(int n);
}

class MyProgram {
  //@ requires c != null ** c.state(0);
  //@ ensures c.state(2);
  void foo(Counter c) {
    //@ assert c.state(0);
    c.increment(2) /*@ with { oldCount = 0; } @*/;
    //@ assert c.state(2);
  }
}

The client only uses the predicate when expressing how it manipulates the counter. Therefore, the counter class is now free to change its internal composition without affecting any of its clients. This is possible because only relevant details are exposed through the predicate. In this case, this is the value of the counter. For example, adding a plain field does not break the client.

If the interface of Counter changes, the client code will have to change too. However, the client code does not have to manage any extra permissions: it only has to specify how it uses the interface from CounterExtended. The next example shows this.

class CounterExtended {
  int count;
  int numIncrements;

  /*@ resource state(int val, int val2) = Perm(count, write) ** count == val 
        ** Perm(numIncrements, write) ** numIncrements == val2;
    @*/
  
  //@ given int oldCount;
  //@ given int oldIncrements;
  //@ requires state(oldCount, oldIncrements);
  //@ ensures state(oldCount + n, oldIncrements + 1);
  void increment(int n);
}

class MyProgram {
  //@ given int oldIncrements;
  //@ requires c != null ** c.state(0, oldIncrements);
  //@ ensures c.state(2, oldIncrements + 1);
  void foo(CounterExtended c) {
    //@ assert c.state(0, oldIncrements);
    c.increment(2) /*@ with { oldCount = 0; oldIncrements = oldIncrements; } @*/;
    //@ assert c.state(2, oldIncrements + 1);
  }
}

To summarise, predicates are very effective at hiding implementation details. They allow encapsulation. However, predicates do not protect the client from breaking changes. If the interface changes, any clients will have to change too.

Reserved/internal predicates

There are a few situations where VerCors attaches special meanings to certain predicate names.

For atomics/locks

For atomics and locks a predicate lock_invariant is defined. This predicate cannot be folded/unfolded, and has to be manipulated through locking and unlocking.

Additionally, it can be checked if a lock is currently held through the held(x) syntax. held is in this case effectively a predicate that cannot be unfolded. Therefore, any semantics and techniques for manipulating predicates discussed in this part of the tutorial can be applied to held, such as splitting and scaling, except for folding and unfolding.

For more information, see the Atomics and Locks section.

Threads

A thread can be in several states, such as idle and running. The syntax for this is idle(thread) and running(thread). idle and running are effectively predicates that cannot be unfolded. Therefore, any semantics and techniques for manipulating predicates discussed in this part of the tutorial can be applied to held (such as splitting and scaling).

See the PVL Syntax Reference section for more details.

Advanced usage of predicates

Unfolding predicates within expressions using \unfolding

Sometimes it is necessary to briefly open a predicate within an expression, for example, to temporarily gain access to a field. This can be achieved using the \unfolding operator. It has the following concrete syntax:

\unfolding myPredicate(arg1, arg2, ...) \in expression

It takes the instance of the predicate that needs unfolding, followed by \in, and then an expression in which the predicate must be unfolded. After evaluating the internal expression, the predicate is folded again, without any changes to the predicate or the program state. For Java, the alternative syntax is \Unfolding (notice the capital U), since \unfolding causes a compiler error.

Below is an example usage of \unfolding in a Cell class where the predicate does not have a parameter for the value inside the Cell. To work around this, \unfolding is used.

class Cell {
  //@ ensures state() ** \unfolding state() \in x == 0;
  Cell() {
    x = 0;
    //@ fold state();
  }

  //@ resource state() = Perm(x, write);
  int x;
}

public static void main() {
  Cell c = new Cell();
  //@ assert \unfolding c.state() \in c.x == 0;
}

Recursive predicates

Predicates can directly and indirectly recurse without problems, provided they are not inline. This can be used to for example model permissions over data structures with a size that cannot be known statically, such as a linked list. In the below code example, an instance of state predicate of the class LinkedListNode contains the permission for one field, as well as permissions for all fields of the tail of the list. Additionally, the argument of the state predicate reflects the numbers stored in the linked list.

class LinkedListNode {
  //@ resource state(seq<int> data) = Perm(v, write) ** Perm(next, write) ** v == data[0] ** (next != null ==> next.state(tail(data)));

  int v;
  LinkedListNode next;
}

Scaling & splitting

VerCors offers syntax to specify fractions of predicates, similar to how permissions can be specified in fractions. This can be useful to, for example, allow one half of a state predicate to be passed to one thread, and one to another. For a predicate state(args) on a variable x, the syntax for specifying a fraction f of the predicate is: [f]x.state(args). The code below shows an example of how scaling can be used.

class Cell {
  //@ ensures state(0);
  Cell() {
    //@ fold state(0);
  }

  //@ resource state(int v) = Perm(x, write) ** v == x;
  int x;
}

//@ requires [1\2]c.state(0);
public void startThread(Cell c);

public static void main() {
  Cell c = new Cell();
  // Constructing a cell yields a state predicate
  //@ assert c.state(0);
  // We can split this into fractions of a predicate
  //@ assert [1\2]c.state(0) ** [1\2]c.state(0);

  // startThread will claim half of the predicate
  startThread(c);

  // The other half can be used for something else
  //@ assert [1\2]c.state(0);
}

Inline predicates

Predicates can be given the inline attribute:

class C {
  //@ inline resource state() = Perm(x, write);
  int x;
}

If the inline attribute is given to a predicate, VerCors will inline the definition of that predicate wherever the predicate occurs. This means that the following code snippet:

//@ requires c.state();
void foo(C c) {
  //@ assert c.state();
}

Is equal to:

//@ requires Perm(c.x, write);
void foo(C c) {
  //@ assert Perm(c.x, write);
}

Because of this inlining semantics, inline predicates cannot be recursive. However, besides that limitation they are equal to regular predicates, and hence support arguments and scaling.

Furthermore, because of this inlining semantics, folding and unfolding inline predicates do not change the program state. However, for the ease of flexibility, VerCors allows them, interpreting them as a check for whether or not the contents of a predicate is present.

Inheritance

Inheritance is not yet supported for predicates.

Thread-local predicates

There is informal & incomplete support for predicates with thread-dependent resources. For this, the predicate must be defined with the thread_local modifier. The \current_thread keyword can be used inside thread_local predicates to get the integer identifier of the current thread. This can be useful to assign e.g. array indices to individual threads in a global manner.

To restrict the number of threads, and hence the possible values of \current_thread, assumptions can be made. This can be done either in preconditions, or in predicate bodies. For example, for some N:

requires 0 <= \current_thread && \current_thread < N;

Known problems

VerCors crashes when predicates are unfolded

When using predicates, VerCors might yield the following error:

Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.util.NoSuchElementException: None.get
  Cause: java.util.concurrent.ExecutionException: java.util.NoSuchElementException: None.get

This is because the current implementation of Java inheritance in VerCors is incomplete. There are two workarounds for this.

First, a predicate declaration can be marked as final. This ensures that the inheritance-related logic in VerCors is not applied to that predicate, which means it can be used as described in this chapter. In the code below we show an example usage of this workaround.

int x;

//@ final resource state(int val) = Perm(x, write) ** x == val;

//@ requires Perm(x, write) ** x == n;
//@ ensures state(n);
void foo(int n) {
    //@ fold state(n);
}

Second, if a class has many predicates, or the first workaround does not seem to work, the whole class can be marked as final. This ensures the inheritance-related logic in VerCors is not applied to the class at all.

Both workarounds do not change the semantics of Java code that does not use inheritance.

Finally, if neither of the workarounds work, please file an issue.

Interaction between loop conditions and predicates

Consider the following example:

//@ resource wrapX(int val) = Perm(x, write) ** x == val;
int x;

//@ requires wrapX(5);
void m() {
  //@ ghost int i = 5;

  //@ loop_invariant wrapX(i);
  //@ loop_invariant \unfolding wrapX(i) \in 5 <= x && x <= 10;
  while (x < 10) {
    //@ unfold wrapX(i);
    x++;
    //@ ghost i++;
    //@ fold wrapX(i);
  } 
}

This will give an error on the while condition, stating that there is no permission for x. This is to be expected, since permission for x is contained in the predicate wrapX(i). Since we did not give instructions to unfold it, the loop condition cannot access x. Intuitively, the following extra syntax should work:

//@ resource wrapX(int val) = Perm(x, write) ** x == val;
int x;

//@ requires wrapX(5);
void m() {
  //@ ghost int i = 5;

  //@ loop_invariant wrapX(i);
  //@ loop_invariant \unfolding wrapX(i) \in 5 <= x && x <= 10;
  while (/*@ \unfolding wrapX(i) \in @*/ x < 10) {
    //@ unfold wrapX(i);
    x++;
    //@ ghost i++;
    //@ fold wrapX(i);
  } 
}

However, this syntax is currently not supported by VerCors. Instead, it is recommended to use an inline predicate if possible (see the Inline Predicates section for more info). Applying this workaround results in the following program:

//@ inline resource wrapX(int val) = Perm(x, write) ** x == val;
int x;

//@ requires wrapX(5);
void m() {
  //@ ghost int i = 5;

  //@ loop_invariant wrapX(i);
  //@ loop_invariant 5 <= x && x <= 10;
  while (x < 10) {
    x++;
    //@ ghost i++;
  } 
}

Alternatively, the condition can be lifted into its own boolean variable as in the example below. However, this 1) leads to verbose code, and 2) requires modification of non-ghost code. Note that, for presentation reasons, the loop condition p is also more strict than in the previous examples.

//@ resource wrapX(int val) = Perm(x, write) ** x == val;
int x;

//@ requires wrapX(5);
void m() {
  // Put the loop condition in a separate variable. This requires unfolding the predicate temporarily.
  //@ unfold wrapX(5);
  boolean p = 5 <= x && x < 10;
  //@ fold wrapX(5);

  //@ ghost int i = 5;

  //@ loop_invariant wrapX(i);
  //@ loop_invariant \unfolding wrapX(i) \in 5 <= x && x <= 10;
  // Require that loop maintains that p equals the previous loop condition
  //@ loop_invariant p == \unfolding wrapX(i) \in (5 <= x && x < 10);
  while (p) {
    //@ unfold wrapX(i);
    x++;
    //@ ghost i++;

    // Before the while loop ends, check the loop condition manually
    // And put the result in p again.
    p = 5 <= x && x < 10;
    //@ fold wrapX(i);
  }

  //@ assert wrapX(10);
}

Inheritance

Currently, support for inheritance is very limited. Bob Rubbens is working on improving support for inheritance as part of his PhD position. You can read theoretical work on this in his masters thesis: https://essay.utwente.nl/81338/, or contact Bob at r.b.rubbens@utwente.nl. As support improves, this wiki page will improve accordingly.

Exceptions & Goto

This section discusses support for exceptions and goto in VerCors. The following topics are discussed:

• The support that is currently implemented and support that is still being worked on is listed here.
• Then a brief summary of exceptions in Java is given here.
• Then we discuss the signals contract clause here, which models exceptions in VerCors.
• Finally, support for goto is discussed here.

Exceptions

Support

VerCors currently only supports Java exceptions. They are not supported in PVL. We also do not support signal handlers in C. The table below lists which facets of exceptions in Java are currently supported in VerCors.

Support for exceptions is still being worked on currently. Progress on the implementation can be followed here.

Java Exceptions Example

We will now discuss a basic artificial example of exception usage in Java. For a more thorough overview, we refer the reader to the Java tutorial on exceptions: https://docs.oracle.com/javase/tutorial/essential/exceptions/index.html.

In the following code example, the find method determines if an array contains a specific integer value:

class MyFind {
    public static boolean find(int[] xs, int value) throws Exception {
        for (int i = 0; i < xs.length; i++) {
            if (xs[i] == value) {
                return true;
            } else if (xs[i] < 0) {
                throw new Exception();
            }
        }

        return false;
    }

    public static void main(String[] args) {
        int[] myXs = int[3];
        myXs[0] = 1;
        myXs[1] = 10;
        myXs[2] = -3;
       
        try {
            find(myXs, 22);
        } catch (Exception e) {
            System.out.println("An error occurred");
        }
    }
}

If the find method encounters a negative array element while searching, it throws an exception. The fact that the method throws an exception at all is indicated by the throws Exception modifier when the find method is defined. Specifically, the exception is thrown by the throw new Exception() statement in the find method.

The thrown exception is handled in the main method by wrapping the call to find in a try-catch block. Whenever an exception is thrown within a try-catch block, the exception is passed to the catch block of the type of the exception that matches the type of the catch block. This catch block can then handle the exception to allow the program to continue, or perform cleanup such that the program can exit safely. If none of the catch blocks can handle the exception, it is passed further up the call stack, possibly terminating the program if it is not caught and handled.

The signals clause

The signals clause supported in VerCors is very similar to the signals clauses supported in JML (documented here). It is a contract element like requires or ensures, and declares the postcondition in case an exception is thrown. The declared postcondition holds when the thrown type matches the type stated in the signals clause. When an exception is thrown, normal ensures post-conditions never hold, and instead only relevant signals clauses hold.

As an artificial example, we can define a signals clause for a method that sums two numbers. The method throws an exception if one of the numers is equal to five.

//@ signals (Exception e) a == 5 || b == 5;
//@ ensures \result == (a + b);
void sum(int a, int b) throws Exception {
    if (a == 5 || b == 5) {
        throw new Exception();
    } else {
        return a + b;
    }
}

Similar to the throws attribute, the signals clause can name both checked and unchecked exceptions. The only limitation is that the type must extend Throwable.

Signals does not guarantee an exception

A frequently occurring use-case is to guarantee that an exception is thrown, if a certain condition occurs. Furthermore, this is also how the semantics of the signals clause is sometimes misinterpreted. Applying this line of though to the previous example, one might expect the method sum to always throw if one of the arguments equals five. However, this is not the case. The implementation for pickySum below demonstrates this. The implementation for pickySum also satisfies the contract for sum, but clearly pickySum does not always throw an exception if one of the arguments equals 5:

//@ signals (Exception e) a == 5 || b == 5;
//@ ensures \result == (a + b);
void pickySum(int a, int b) {
    if ((a == 5 || b == 5) && dayOfTheWeek() == "tuesday") {
        throw new Exception();
    } else {
        return a + b;
    }
}

Instead, pickySum only throws an exception if one of the arguments equals five, and today is tuesday. Would pickySum be called on a monday with 5 and 10, an exception would not be thrown, and instead 15 would be returned.

This artificial example shows how a signals clause should be interpreted: when an exception of the appropriate type is thrown, the signals clause can be assumed to hold. We call this the "reactive" semantics.

It is not guaranteed that an exception is thrown if a signals condition occurs. We call this the "causal" semantics. VerCors does not implement this currently.

If needed, there is a way to model the causal semantics using an additional ensures clause. To do this, an ensures clause needs to be added that implies false when the signals condition occurs. For example, pickySum can be made consistent as follows:

//@ signals (Exception e) a == 5 || b == 5;
//@ ensures (a == 5 || b == 5) ==> false;
//@ ensures \result == (a + b);
void consistentSum(int a, int b) {
    if (a == 5 || b == 5) {
        throw new Exception();
    } else {
        return a + b;
    }
}

By ensuring that the method cannot terminate normally if one of the arguments equals 5, it is guaranteed that an exception is thrown when one of the arguments equals 5. This encodes the causal semantics using the reactive semantics supported by VerCors.

Exception guarantees

Java guarantees that methods only throw checked exceptions if they are explicitly mentioned in the throws attribute. Unchecked exceptions can always be thrown.

VerCors does not implement this exact semantics. Instead, it assumes that any exception that can be thrown is mentioned in either the throws attribute or in a signals clause. In other words, if a method has no throws clauses, nor signals clauses, it is 100% exception safe according to VerCors. A downside of this is that the VerCors exception semantics does not 100% reflect the Java semantics. The upside is that VerCors can now guarantee that all specified exceptions are caught, as all relevant exceptions are stated explicitly.

For example, if a method does not have a signals clause stating it throws a RuntimeException, VerCors assumes this exception will never be thrown by the method. Another example, if a throw new RuntimeException() statement occurs in method M, VerCors will give an error if M does not have a signals clause for RuntimeException.

In some situations it might be necessary to opt into the more realistic Java semantics of unchecked exceptions. VerCors does not support this directly, but it can be moddeled with an additional signals clause. To do this, an additional signals clause must be added with the condition true. For example, we can modify the contract of the earlier presented sum method to allow throwing a RuntimeException randomly:

//@ signals (ArithmeticException e) a == 5 || b == 5;
//@ signals (RuntimeException e) true;
//@ ensures \result == (a + b);
void sum(int a, int b) {
    if (a == 5 || b == 5) {
        throw new ArithmeticException();
    } else {
        return a + b;
    }
}

void useSum() {
    int result = sum(5, 10);
    System.out.println("Result: " + result);
}

If this example is checked by VerCors, it will yield an error in the useSum method. The error will complain that sum might throw a RuntimeException, but that it is not specified in the contract nor handled in the useSum body.

A way to resolve this would be to catch the RuntimeException by wrapping the call to sum in a try-catch block. However, since catching a RuntimeException is bad practice, it is sometimes better to indicate in the contract of useSum that useSum might also throw a RuntimeException. This propagates the responsibility for handling the unchecked exception to the caller.

The signals_only clause

The signals_only clause from JML (documented here) is not supported by VerCors. It guarantees that the only types that will be thrown by the method are the types listed in the signals_only clause.

To simulate the functionality of signals_only T1, ..., Tn, a signals clause with the condition true can be added for each Ti. For example, the clause signals_only T1, T2; can be simulated by adding two signals clauses to a method contract as follows:

//@ signals (T1 e) true;
//@ signals (T2 e) true;
void m() {
    
}

Alternatively, the abbreviation of signals_only documented in Section 9.9.5 of the JML reference manual can also be used to approximate the semantics of signals_only in VerCors.

Goto and labels

PVL has support for goto and label. They are useful for modeling control flow primitives not yet supported in VerCors. The semantics are standard: when the goto l statement is encountered, control flow is immediately transferred to the location indicated by the label l. For example, the following program verifies:

int x = 3;
goto l;
x = 4;
label l;
assert x == 3;

As PVL does not have a construct like finally in Java, there are no exceptions for the semantics of goto in PVL.

One example where use of goto might lead to confusing results is the following. In the below example, goto is used to exit the while loop. Because goto redirects control flow to the destination label immediately, checking the loop invariant is skipped.

int r = 10;
loop_invariant r == 10;
while (true) {
  r = 20;
  goto lbl2;
}
assert r == 10; // Never executed
label lbl2;
assert r == 20;

If it is desired that the loop invariant is checked at goto as well, this can be modeled by adding asserts at the exit labels of the while loop.

VerCors by Error

Assertion failed: expression may be false

VeyMont

VeyMont is a tool for verification of concurrent message passing programs, also called choreographies. It is implemented as an extension of VerCors. VeyMont generates an implementation from a choreography using the endpoint projection. In this implementation, each endpoint is executed as a thread, and is responsible for a part of the choreography. When these threads are all executed in parallel, the behaviour follows the choreography. Essentially, this projection preserves functional correctness, which is proven with VerCors on the choreography, and guarantees deadlock-freedom. In addition, contracts written in proper form are preserved and projected to the proper endpoint. This allows re-verification of the generated implementation, decreasing the need to trust the implementation of VeyMont, as well as allowing modifications to the generated implementation.

We will introduce the syntax of choreographies through a simple example. Then we will show how to verify it using the permission generation capabilities of VeyMont. Finally, we will introduce the syntax for choreography contracts & permissions, and channel invariants. Using these, we will verify a property of the example. We will assume the reader is familiar with PVL concepts such as permissions, the separating conjunction, contracts and classes. At the end of this section we will give some further directions for reading, as well as an overview of all syntax that VeyMont supports.

Choreography syntax

Choreographies are defined using the choreography keyword. They have a name, arguments, and a body. For example, the next code snippet defines a choreography named Example, and has two parameters, the integers x and y.

choreography Example(int x, int y) {
  // Empty body
}

The body of a choreography consists of endpoint definitions and a single run definition. Endpoint definitions have a name, a class type, and arguments. For example, we can add a Store class with two integer fields. We then define two endpoints using the Store class. We initialize the endpoints with the x and y parameters from the main arguments of the choreography.

class Store {
  int v;
  int temp;

  constructor(int init) {
    v = init;
  }
}

choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);
}

The Store class is a regular PVL class, for more information we refer the reader to the PVL documentation here. It is sometimes omitted in this documentation, but it should be included when verifying the choreography, as otherwise the program cannot be typechecked.

The run definition of a choreography contains the logic of the choreography, and determines the interactions between the endpoints. It is defined using the run keyword and a block of choreographic statements. The next example exchanges the two values using choreographic statements. First, each endpoint sends their v value to the temp field of the other endpoint using the communicate statement. Then, each endpoint copies the value in their temp fields to their v fields using :=, the choreographic assignment operator. The difference between choreographic assignment and regular assignment, is that a choreographic assignment may only read and write to memory that is owned by the endpoint being assigned to.

choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  run {
    communicate alex.v -> bobby.temp;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

Using VeyMont: choreographic verification & permission generation

This example lacks contracts and permissions. However, it can still be verified, and an implementation can also be generated. This can be done using the following command:

$ vercors --veymont example.pvl --generate-permissions --veymont-output example_output.pvl
[INFO] Start: VeyMont (at 10:52:56)
[INFO] Choreography verified successfully (duration: 00:00:10)
[INFO] Writing unknown.pvl to example_output.pvl
[INFO] Implementation generated successfully
[INFO] Implementation verified successfully (duration: 00:00:07)
[INFO] Done: VeyMont (at 10:53:14, duration: 00:00:17

This command executes several steps:

• Permissions are generated according to the single-owner policy. This means that each endpoint owns its own fields, and is not allowed to read or write fields of other endpoints.
• The choreography is verified. This succeeds, as the program is memory safe: each endpoint only reads and writes its own fields.
• An implementation is generated using the endpoint projection. All generated permissions are projected to the endpoint that contains the field referenced in the permissions. As the --veymont-output is also present, the implementation is also written to the path given.
• The generated implementation is verified. This again verifies, as expected for this simple example, because the choreography verified as well. This is not always the case, as we will show in a later section.

If you want to use only one of these steps, you can use the --choreography, --generate, and --implementation flags, respectively, to make veymont skip the other steps.

Choreographic contracts

Channel invariants & choreographic contracts can be used to specify & verify functional correctness and memory safety. Using choreographic contracts, we can manually specify the permissions that VeyMont generated for us with the --generate-permissions flag:

class Store {
  int v;
  int temp;

  ensures Perm(v, 1) ** v == init;
  ensures Perm(temp, 1);
  constructor(int init) {
    v = init;
  }
}

choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  requires (\endpoint alex;
    Perm(alex.v, 1) **
    Perm(alex.temp, 1));
  requires (\endpoint bobby;
    Perm(bobby.v, 1) **
    Perm(bobby.temp, 1));
  run {
    communicate alex.v -> bobby.temp;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

Specifically, we add permissions to the constructor of Store, and permissions to the precondition of run. We use the \endpoint expression to indicate the endpoint for which the expressions is relevant. The endpoint projection uses this information to decide which endpoint to project an expression to. VeyMont knows a very simple inference rule, which allows us to omit the \endpoint expressions in some cases. Essentially, whenever the endpoint context is directly inferrable from the expression, VeyMont tries to do so. In this case, this shortens the contract to the following:

choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  requires Perm(alex.v, 1) ** Perm(alex.temp, 1);
  requires Perm(bobby.v, 1) ** Perm(bobby.temp, 1);
  run {
    communicate alex.v -> bobby.temp;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

VeyMont verifies the above two examples successfully.

Channel invariants & functional correctness

We will now go one step further and specify functional correctness of the above example. Specifically, we will verify that, if x and y are positive and negative respectively, the fields bobby.v and alex.v will also be positive and negative, respectively, after executing the choreography. We do this by adding a contract to the main choreography, to constrain x and y. We also enhance the contract of run by adding this requirement. This results in the following choreography:

requires x > 0 && y < 0;
choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  requires Perm(alex.v, 1) ** Perm(alex.temp, 1) ** alex.v > 0;
  requires Perm(bobby.v, 1) ** Perm(bobby.temp, 1) ** bobby.v < 0;
  ensures Perm(alex.v, 1) ** alex.v < 0;
  ensures Perm(bobby.v, 1) ** bobby.v > 0;
  run {
    communicate alex.v -> bobby.temp;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

This version does not yet verify. VeyMont reports an error on the postcondition of the above choreograpy, reporting that alex.v and bob.v might not be negative and positive, respectively. Note that this error is discovered only after the choreography is verified! This shows an interesting aspect of VeyMont: at the choreography level, properties over the transferred values are included in the reasoning of VeyMont. While this is only matters for primitive values like integers, it is ocasionally useful for verifying choreographies. Note that, while the generated implementation would not verify, it is not because of a bug: there are simply some annotations missing.

In deductive program verification terms, there is a modularity boundary at the communicate statement, in the sense of modular verification. When verifying the choreography, this modularity boundary is transparent. When verifying the implementation, this modularity boundary is opaque. The decision of when and where to draw the modularity boundary is a topic of ongoing research, and might change in future versions of VeyMont.

We will now finish verifying the implementation by adding a property over the message that is sent. This type of property is specified using a channel invariant. Channel invariants are defined using the channel_invariant keyword, followed by an expression. Channel invariants must directly precede the communicate statement they apply to. Within a channel invariant, the special expressions \msg, \sender and \receiver are available. They refer to the message being sent, the sending and the receiving endpoint, respectively. Within a channel invariant, there can be no endpoint ownership expressions, as the owners are implictly determined by the sending and receiving endpoint.

Adding the constraints as channel invariants results in the following choreography:

requires x > 0 && y < 0;
choreography Example(int x, int y) {
  endpoint alex = Store(x);
  endpoint bobby = Store(y);

  requires Perm(alex.v, 1) ** Perm(alex.temp, 1) ** alex.v > 0;
  requires Perm(bobby.v, 1) ** Perm(bobby.temp, 1) ** bobby.v < 0;
  ensures Perm(alex.v, 1) ** alex.v < 0;
  ensures Perm(bobby.v, 1) ** bobby.v > 0;
  run {
    channel_invariant \msg > 0;
    communicate alex.v -> bobby.temp;
    channel_invariant \msg < 0;
    communicate bobby.v -> alex.temp;
    alex.v := alex.temp;
    bobby.v := bobby.temp;
  }
}

The generated implementation of this final version of the choreography verifies.

What next?

More choreographies can be found in the test suite of VeyMont, as well as in the tool papers.

Publications

• The base theory of VeyMont: https://doi.org/10.1007/978-3-030-99336-8_19
• The first tool paper, introducing the base VeyMont implementation: https://doi.org/10.1007/978-3-031-27481-7_19
  • The artefact: https://doi.org/10.5281/zenodo.7410640
• The second tool paper, introducing the contract- and permission-preserving endpoint projection: (published at iFM 2024, DOI pending)
  • The artefact: https://doi.org/10.4121/93f68b2c-5f85-4afd-9679-5e92c634a1b0

VeyMont syntax overview

Choreography declarations

• [contract] choreography Name(parameters...) { choreographic declarations... }

  Defines a choreography named "Name", with zero or more parameters and a body of choreographic declarations. The choreography declaration may be preceded with a contract, which can be used to constrain the arguments.

• endpoint a = ClassType(args...);

  Defines an endpoint named a of type ClassType. When a is initialized, the constructor of ClassType will be called with arguments args....

• [contract] run { choreographic statements... }

  The run declaration defines the interactions between endpoints. It contains zero or more choreographic statements.

Choreographic contract expressions

• (\endpoint a; expr)

  Specifies that expression expr belongs to endpoint a. This means that expression expr will be evaluated in the context of a, using memory only available to a. The endpoint projection also uses this to decide where to project an expression to.

• (\chor expr)

  Specifies that expression expr belongs to no endpoint in particular. It will be included when verifying the choreography, but when generating an implementation this expression is discarded and replaced with true. This means that the generated implementation might not verify. Essentially, \chor is a debugging construct, similar to the assume statement. It is useful to verify properties at the choreographic while they cannot be verified at the generated implementation level yet.

• Perm[a](obj.f, p)

  This is shorthand syntax for (\endpoint a; Perm(obj.f, p)).

Choreographic statements

• channel_invariant expr;

  Specifies a property over a message being sent. Must directly precede a communicate statement.

• communicate a.f -> b.f;

  Indicates that a message is exchanged between endpoint a and b, the value being the f field of a, the destination being the f field of b.

• communicate a: message -> b: target;

  Extended form of the communicate statement, with a and b being endpoints, message being the expression of the message to be sent, and target an assignable memory location for which b has write permission.

• a.f := expr;

  Assigns expr to a.f, in the context of endpoint a. This means VeyMont will report an error if expr tries to read memory that a does not own.

• a: target := expr;

  Assigns expr to target in the context of endpoint a. Used as a fallback when VeyMont cannot infer the endpoint context directly from target.

Channel invariant expressions

• \msg

  Refers to the message being sent.

• \sender, \receiver

  Refer to the sender and receiver of the communicate statement.

Term Rewriting Rules

VerCors allows you to define your own term rewriting rules via pvl files. This chapter shows you how.

Magic Wands

The handling of magic wands is non-trivial, so this chapter takes a closer look at that. For further reading, see e.g. "Witnessing the elimination of magic wands". Blom, S.; and Huisman, M. STTT, 17(6): 757–781. 2015.

Also take a look at the Viper tutorial for wands: http://viper.ethz.ch/tutorial/?page=1&section=#magic-wands

What are Magic Wands?

The "Magic Wand" or separating implication is a connective in separation logic using the symbol -*. It represents a part of a resource (see "Predicates") or "resource with a hole": A -* B means "if you give me an A, I can give you a B in return". Thus, it is similar to a logical implication A ==> B; however, it consumes the A when it is exchanged for a B.

A common use case is if you have a predicate defining a recursive data structure like a linked list or a binary tree, and you take a part of that data structure to reason about explicitly, like a sub-tree. You can use the recursive predicate to reason about the sub-tree, but it is more difficult to reason about the remainder of the original tree: Since you took out the sub-tree and have explicit permission for it, the recursive predicate for the whole tree can no longer have the permission for that part, so it would have to stop recursing at a certain point. With a wand, you can resolve this: For a tree T with left sub-tree L and right sub-tree R, and a recursive predicate Tree(x), you can split Tree(T) into Tree(L) ** (Tree(L)-*Tree(T)). So you have the explicit resource for the left sub-tree, and a wand such that if you join the sub-tree back into it, you get the predicate for the whole tree back. This joining is called applying the wand.

Syntax in VerCors

We will use the following binary tree as example:

final class Tree {
  int value;
  int priority;
  Tree left;
  Tree right;

  /*@
  resource tree() = Perm(value, write) ** Perm(priority, write) ** Perm(left, write) ** Perm(right, write) 
    ** (left != null ==> left.tree()) ** (right != null ==> right.tree());

  requires t.tree();
  static pure boolean sorted(Tree t) 
  = t != null ==> \unfolding t.tree() \in 
    (t.left != null ==> sorted(t.left) && \unfolding t.left.tree() \in t.priority >= t.left.priority) 
    && (t.right!= null ==> sorted(t.right) && \unfolding t.right.tree() \in t.priority >= t.right.priority);
  @*/

So a Tree contains a data item value, a priority and two references to the sub-trees; the tree resource contains write permissions for all those fields, as well as recursive permissions for the sub-trees; and the sorted function ensures that the priority in the root node is the largest in the Tree (like in a priority queue).

Creating a Wand

To create a wand, use the keyword create {...}. Inside the curly braces, you have to provide the necessary information to create the wand:

You need to explicitly specify which resources from the current context should be folded into the wand. The keyword for this is use. Note that, like with folding a normal predicated, any permissions folded into the wand are no longer available in the environment. You can also use boolean facts from the current context, e.g. use a==b;.

When creating a wand A-*B, you need to describe how exactly to merge A with the content of the wand to obtain B. For example, A may contain permissions for the left sub-tree and the wand those for the right sub-tree, and to get the full tree, you need to perform a fold. All necessary permissions and boolean facts for such a merger must be provided via use.

The final statement within the curly braces of create has to be qed A-*B;, with A-*B being replaced by the wand you created.

Note that the wand operator -* has the precedence like an implication, thus it is less binding than the separating conjunct ** and boolean connectives like &&.

/*@
requires t != null;
requires t.tree();
requires \unfolding t.tree() \in t.left != null;
ensures \result != null ** \result.tree();
ensures \result.tree() -* t.tree();
@*/
static Tree get_left(Tree t) {
  //@ unfold t.tree();
  Tree res = t.left;
  /*@
  create {
    use Perm(t.value, write) ** Perm(t.priority, write) ** Perm(t.left, write) ** Perm(t.right, write);
    use t.right != null ==> t.right.tree();
    use res == t.left;
    fold t.tree();
    qed res.tree() -* t.tree();
  }
  @*/
  return res;
}

Notice how in the example, all the permissions necessary for folding tree(t) are provided with use, except the part that is in the premise of the wand, tree(t.left). If we had provided that as well, it would have become part of the wand, rather than being the "missing piece", and the first post-condition ensures tree(\result) would have failed for lack of permission (since this permission is bundled into the wand, and no longer directly available). Additionally, we had to provide the fact that res is the left sub-tree of t, so that fold tree(t) knows that the premise of the wand fits into the missing part of the predicate.

Applying a Wand

To combine the "missing piece" with the wand and obtain the full resource, use the keyword apply. Since we already specified how the merging works when we created the wand, no further logic is needed now:

/*@
context t != null;
context t.tree();
requires \unfolding t.tree() \in t.left != null;
@*/
static boolean check_left_priority(Tree t, int max_priority) {
  Tree left = get_left(t);
  // now we have tree(left) and a wand tree(left) -* tree(t)
  //@ unfold left.tree();
  boolean res = left.priority <= max_priority;
  //@ fold left.tree();
  //@ apply left.tree() -* t.tree();
  // now left.tree() is no longer directly available, but t.tree() is back
  return res;
}

More Complex Expressions

Sometimes, we may want to reason about the things contained in a wand; for example we decompose a sorted tree, and want to say it will be sorted again after the merger. However, as long as tree(t) is split into the sub-tree and the wand, we cannot call sorted(t) as it needs the full predicate tree(t). But simply ignoring the sortedness when splitting and later merging again would mean that we can no longer make any assertions about sortedness afterwards. As a solution, we encode the property into the wand, by adding conjuncts to the premise and antecedence of the wand: A**B -* C**D. We can only apply such a wand if we hold the permissions of A and the properties in B hold. This stricter requirement is rewarded with the fact that we will get both the permissions in C and the properties of D after applying the wand.

Note that VerCors currently only allows method calls as conjuncts in wands, so properties like an equality a==b must be wrapped in a function in order to be used.

/*@
requires t != null ** t.tree();
static boolean wand_helper(Tree t, int max_prio)
  = \unfolding t.tree() \in t.priority <= max_prio;
@*/

/*@
yields int root_prio;
requires t != null;
requires t.tree() ** sorted(t);
requires \unfolding t.tree() \in t.left != null;
ensures \result != null ** \result.tree();
ensures sorted(\result) && wand_helper(\result, root_prio);
ensures \result.tree() ** sorted(\result) ** wand_helper(\result, root_prio) 
        -* 
        t.tree() ** sorted(t);
@*/
static Tree get_left_sorted(Tree t) {
  //@ unfold t.tree();
  //@ ghost root_prio = t.priority;
  Tree res = t.left;
  /*@
  create {
    // necessary parts for t.tree()
    use Perm(t.value, write) ** Perm(t.priority, write) ** Perm(t.left, write) ** Perm(t.right, write);
    use t.right != null ==> t.right.tree();
    use res == t.left;
    // necessary parts for t.sorted()
    use res != null;
    use t.priority == root_prio;
    use t.right != null ==> sorted(t.right) && \unfolding t.right.tree() \in t.priority >= t.right.priority;
    // assemble parts
    fold t.tree();
    qed res.tree() ** sorted(res) ** wand_helper(res, root_prio) 
        -* 
        t.tree() ** sorted(t);
  }
  @*/
  return res;
}

/*@
context t != null;
context t.tree() ** sorted(t);
requires \unfolding t.tree() \in t.left != null;
@*/
static boolean check_left_priority_sorted(Tree t, int max_priority) {
  //@ ghost int root_prio;
  Tree left = get_left_sorted(t) /*@ then { root_prio = root_prio; } @*/;
  // now we have left.tree(), sorted(left) and wand_helper(left, root_prio), as well as the wand
  //@ unfold left.tree();
  boolean res = left.priority <= max_priority;
  //@ fold left.tree();
  //@ apply (left.tree() ** sorted(left) ** wand_helper(left, root_prio)) -* (t.tree() ** sorted(t));
  // now left.tree() is no longer directly available, but t.tree() is back and sorted
  return res;
}

Now, when creating the wand, we need to use additional information in order to be able to ensure sortedness after the merger: The condition for the right side can simply be provided. The condition for the left side is part of the premise of the wand (in particular sorted). The comparison between the priority of the root and the priority of the left node is wrapped into a helper function, wand_helper. Since the premise of the wand contains no permissions for t.priority, we use a ghost variable root_prio to communicate that value.

Applying the wand is nearly as simple as before. However, we again need to use the ghost variable root_prio as an intermediate storage for the priority of t.

You see that adding such additional constraints about the wand's resources is possible, but can carry significant overhead of helper functions, use statements, etc.

Inhale and exhale

// TODO: Explain inhale and exhale statements (add warning!)

What does this VerCors error message mean?

This page is to explain what the different error messages in VerCors mean. We try to keep this page alphabetically ordered by error message (case insensitive sorting. For sentences: spaces come before letters in the alphabet). If you have a question about error messages, please add a question to this wiki page. If you know the answer to a question asked here, please replace the question with the answer (or with a link to the answer elsewhere on the wiki).

AssignmentFailed: insufficient permission

This means you are trying to write to a variable (at the left hand side of an assignment) to which VerCors cannot establish a write-permission. The statement assert(Perm(lhs,1)); in which lhs is the left hand side of this assignment will fail at this point in your code, but should be provable.

Illegal argument count

This is a internal VerCors error, that might be due to a parse-error in your script. We have opened a issue for this here.

Illegal iteration invariant

This seems to happen when you try to specify a loop_invariant in a for-loop, where you're using a resource as invariant. Try using context (short for ensures and requires combined) instead. Are you getting this message in a different situation? Do let us know!

java.lang.*

This is never supposed to happen, but unfortunately, it did. Thank you for finding this bug in VerCors. Try searching our issue tracker to see if you believe this bug is already being addressed. If not, please let us know about it by adding it!

No viable alternative at ...

This is a parsing error, you may have made a typo, or inadvertently used a reserved keyword as a variable. Check your code at the position indicated. If this is the start of a line, make sure there is a semicolon ; at the previous line.

NotWellFormed:InsufficientPermission

This error is shown at a specification. We require rules to be 'self framing', this means that you need read-permission in order to access variables, even inside specifications. Furthermore, checks like array accesses being within bounds need to hold. The order of the specifications makes a difference here: the lines of your specifications are checked from top to bottom, and from left to right. In order to establish permissions and bounds, add a line of specification before the line that gives you trouble, asserting that you have read permission, or that the access is within bounds.

If you see this error in the \old(..) part of an ensures expression, you need permission to that variable before executing the function. For constructors (e.g. foo method of class foo), there is no \old(this.x), as the variable this.x is only created when the constructor is called.

Pre-condition of constructor may not refer to this

When calling the constructor method of a class, the class variables are not yet initialised. Therefore, you should not refer to them. Do you need write-permission? Don't worry, the class constructor already has it by definition (as it implicitly creates the variables)! In particular, use ensures instead of context.

Type of left/right argument is Resource rather than Boolean:

This is a type error. You are using a symbol like && that requires boolean values on both sides. Changing && to **, or breaking up your specification into multiple lines might solve the problem for you.

Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.util.NoSuchElementException: None.get

See VerCors crashes when predicates are unfolded.

"Not injective", or "resource may not be unique with regards to the quantified variables", or similar

Viper requires that all forall with permission expressions (forall* in VerCors) are "injective". That means that different values for the quantified variable(s) must result in different memory locations in the permission expression. For example in (\forall* int k; 0<=k && k<arr.length; Perm(arr[k].myField, 1)), different k must point to different array elements, i.e. arr[i] must be different from arr[j] if i!=j. You need to add a condition like (\forall int i, int j; 0<=i && i<j && j<arr.length; arr[i] != arr[j]) before the quantifier that "may not be unique". And if myField is an object, you might need to do the same for arr[i].myField and arr[j].myField. More info is here.

PVL Syntax Reference

On this page you can find a description of the specification language of VerCors. In general, the specification language extends the language that is verified, like Java. That means that all types, (pure) operators, etc. from the source language can also be used in the specifications, together with the specification-only constructs described below.

Additionally, this page describes PVL, the Prototypal Verification Language. It is a language similar to Java or C and can be verified like them, so the same specification constructs are available. However, it is developed specifically for VerCors, so we also provide the information that is usually found in the language documentation, like the C standard.

General

• Specifications are usually embedded in JML-like comments: /*@ spec @*/ or //@ spec line. Exception: In PVL, specifications are not embedded in comments, instead they are written into the code directly.

• In PVL, identifiers can consist of the characters a-z, A-Z, 0-9 and _. However, they must start with an underscore or letter (a-z, A-Z).

  In specifications, the same rules apply for identifiers as in the language that is specified, e.g. Java identifiers in specifications of Java.

  Note that the following words are reserved and can therefore not be used as identifiers: create, action, destroy, send, recv, use, open, close, atomic, from, merge, split, process, apply, label, \result, write, read, none, empty and current_thread. However, keywords can be wrapped in backticks, to turn them into identifiers, e.g. create cannot be used as an identifier, but `create` is an identifier.

• Most specification constructs are self-contained statements, like preconditions, loop invariants or ghost assignments. Those end with a semicolon ;. However, a few elements, like with side conditions, are parts of another statement, and do not have their own semicolon.

PVL

• At the top level of a program, there can be methods directly (like in C). But more commonly, those are defined within a class:

class ClassName {
    // Here you can add any constructors, class variables and method declarations
}

• The keyword this is used to refer to the current object, null for the null reference ("pointer to nothing").
• You can write single-line or multi-line comments as follows:

// This is a single-line comment
/* 
    This is a 
    multi-line comment 
*/

• Like in C or Java, statements in PVL should end with a semi-colon ;.
• For a more detailed description, see https://github.com/utwente-fmt/vercors/wiki/Prototypal-Verification-Language

Types and Data Structures

The following table lists the basic and composed data types supported in the specification language.

PVL

In PVL, the specification types above can also be used in the regular program. Additionally, the following types are available:

Expressions

Operators

ADTs

Axiomatic Data types have several dedicated operators. Some also have corresponding functions, e.g. s1.subsetOf(s2) for s1 <= s2. There are also functions that do not have an operator equivalence, e.g. xs.removeAt(i). See https://github.com/utwente-fmt/vercors/wiki/Axiomatic-Data-Types for the full list.

PVL

Quantified Expressions

Specification-only Expressions

Resources

Control flow constructs (PVL)

PVL provides similar control flow constructs as other languages, e.g. loops and methods. However, there are also some unique additional control flow constructs that are explained here.

Verification flow constructs

Histories & Futures

Histories and futures, jointly referred to as "Process algebra models" are currently under redesign. Thus, the following parts may not be up to date.

Defining processes

History-related constructs

Future-related constructs

VerCors usage & debugging cheat sheet

Information & questions

https://github.com/utwente-fmt/vercors/wiki

If you're doing a project with VerCors, ask us about the VerCors community chat.

Getting VerCors up and running

Required: at least java 11

Pre-build

• Download latest release (1.3.0 at the time of writing, doesn't work on windows)
• Download the build from the dev branch. Download the .tgz file, it contains a bat script for windows as well. Very likely works, but no guarantee

Should be just unzip and go.

Compile from source

Requires java 11 & sbt. Benefits: allows setting breakpoints in intellij. See VerCors README/Wiki for details.

General usage

vercors inputFile.java --backend

Where backend can be either silicon or carbon.

General flags

Of course, --help

Backends: --carbon (slower, but based on boogie, so sometimes more powerful), --silicon (faster, built by ETH Zurich, sometimes not as smart as Carbon)

Progress printing of individual passes: --progress

Slows down execution but prints more debug info upon crashes: --debug vct.main.Main

Triggers a system notification upon completion: --notify

Advanced verification flags

Detection of unsound preconditions

Flag: --disable-sat

Turns off detection of unsound preconditions. Not needed in general use of VerCors. Might be necessary if you have a lot of foralls in preconditions, and verification is slow.

Java example:

class C {
    //@ requires 1 == 2; // <-- Normally this causes an error, --disable-sat turns this off    
    void m() {

    }
}

Debugging flags

Flags: --show-before passName, --show-after passName

Show textual representation of internal AST before and after a pass. Pass names can be seen by running VerCors with --progress.

VSCode plugin + flags needed

Dump AST given to silicon/carbon into a text file: --encoded temp.sil

This can be opened in VScode with the ETH Zurich Viper plugin/extension installed (see the vscode store for this).

Note:

• The viper version between VerCors and vscode might be out of sync
• The vscode plugin has a 100 second timeout (though it can be turned off)
• The vscode plugin caches results in a wrong way sometimes (this can also be turned off)

Some starter example files

• In the example folder in the repository:
  • basic/BasicAssert-e1.java
  • parallel/block-par.pvl
  • demo/demo1.pvl, demo/demo2.pvl
• All examples in the wiki/tutorial

Case Studies

This page lists all the case studies that have been done with VerCors.

Published case studies

• Automated Verification of the Parallel Bellman-Ford Algorithm. M. Safari, W. Oortwijn and M. Huisman (SAS 2021).
  • Paper: https://doi.org/10.1007/978-3-030-88806-0_17
  • Code: https://github.com/Safari1991/SSSP-Verification
  • Builds on the student project by J. Smits
• Permission-Based Verification of Red-Black Trees and Their Merging. L. Armborst and M. Huisman (FormaliSE 2021).
  • Paper: https://research.utwente.nl/en/publications/permission-based-verification-of-red-black-trees-and-their-mergin
  • Code: https://data.4tu.nl/articles/software/_/13611578
  • This is a continuation of the master project by H.M. Nguyen
• Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms. M. Safari and M. Huisman (ICTAC 2020).
  • Paper: https://doi.org/10.1007/978-3-030-64276-1_10
  • Code: https://github.com/Safari1991/Prefixsum-Applications
• A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms. M. Safari and M. Huisman (IFM 2020).
  • Paper: https://doi.org/10.1007/978-3-030-63461-2_14
  • Code: https://github.com/Safari1991/Permutation
• On the Industrial Application of Critical Software Verification with VerCors. M. Huisman and R.E. Monti (ISoLA 2020).
  • Paper: https://doi.org/10.1007/978-3-030-61467-6_18
  • Code: Not publicly available
  • This was in collaboration with the companies Technolution and Thales.
  • This case study uses a combination of mCRL2 (model checker) and VerCors to prove correctness of the software.
• Formal Verification of Parallel Prefix Sum. M Safari, W. Oortwijn, S. Joosten and M. Huisman (NFM 2020).
  • Paper: https://doi.org/10.1007/978-3-030-55754-6_10
  • Code: https://github.com/Safari1991/Prefixsum
  • Builds on the student project by T. Wiefferink
• Automated Verification of Parallel Nested DFS. W. Oortwijn, M. Huisman, S.J.C. Joosten and J. van de Pol (TACAS 2020).
  • Paper: https://doi.org/10.1007/978-3-030-45190-5_14
  • Code: https://doi.org/10.4121/uuid:36c00955-5574-44d9-9b26-340f7a1ea03b
• Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System. W. Oortwijn and M. Huisman (IFM 2019).
  • Paper: https://doi.org/10.1007/978-3-030-34968-4_23
  • Code: Not publicly available
  • This was in collaboration with the company Technolution.
  • This case study uses a combination of mCRL2 (model checker) and VerCors to prove correctness of the software.

Student projects

Be aware that not all student projects verify complete functional correctness!

Master projects

• Verification of a model checking algorithm in VerCors. H. Hollander (2021).
  • Master thesis: http://purl.utwente.nl/essays/88268
  • Code: https://github.com/HanHollander/SetBasedSCC
• Formal verification of a red-black tree data structure. H.M. Nguyen (2019).
  • Master thesis: http://purl.utwente.nl/essays/77569
  • Code: https://fmt.ewi.utwente.nl/media/rbt.zip
  • This has been continued in Permission-Based Verification of Red-Black Trees and Their Merging (more info in the published case studies list above)

Bachelor projects

• Let's sort this out: GPGPU Verification of Radix Sort. D.H.M.A. van Oorschot (2020).
  • Bachelor thesis: http://purl.utwente.nl/essays/80589
  • Code: Parallel count algorithm, Parallel reorder algorithm, and Parallel radix sort algorithm.
• GPGPU Verification: Correctness of Odd-Even Transposition Sort Algorithm. Y. Kumashev (2020).
  • Bachelor thesis: http://purl.utwente.nl/essays/80585
  • Code: https://doi.org/10.6084/m9.figshare.11725848.v1
• Formal Automated Verification of a Work-Stealing Deque. C.M. van Kampen (2020).
  • Bachelor thesis: http://purl.utwente.nl/essays/80687
  • Code: https://github.com/coenvk/lace-vercors
• Verifying GPGPU Implementation of Breadth-First Search Algorithm. J. Smits (2019).
  • Bachelor thesis: https://fmt.ewi.utwente.nl/media/Bachelor_Thesis_Jan_Smits_BFS_Verification_1.2.pdf
  • Code: In bachelor thesis
• Optimization, Specification and Verification of the Prefix Sum Program in an OpenCL Environment. T. Wiefferink (2015).
  • Bachelor thesis: https://fmt.ewi.utwente.nl/media/147.pdf
  • Code: https://fmt.ewi.utwente.nl/media/147_attachment_1.zip, also available at: https://github.com/NLthijs48/PrefixSumVerification

Developing for VerCors

In Summer 2024, Pieter wrote this developer's guide on the internals of VerCors: https://pieter-bos.github.io/vercors-doc/. It provides some useful background on the setup of the project, and how to do certain tasks.

PR/Branch management

Some general guidelines/notes to take into account when developing for VerCors:

• Draft PRs: while a PR is unfinished, mark it as "draft". Once it is ready for merging, unmark it as draft. Please do this even for short-lived PRs, so there is a definitive signal that work on a PR has finished.
• Branches & PRs: if you do work on a branch, it must have a PR. This way we keep track of what everyone is working on.
• PR size: try to keep your PRs small. If it has been open for longer than a month, consider bringing the PR in a state where it can be merged, even though your work might not be finished yet. This ensures we can still try to do bigger refactorings, while keeping churn in long-standing branches minimal.
• Branch naming: we don't really have a guideline for this, proposals welcome. For now: if it's for a specific subsystem (VeyMont, VeSUV, Pallas), include that. If relevant, feel free to include the issue number.
• VerCors repo or fork: obviously, you may open PRs that propose to merge a branch from a VerCors fork. We try to support this workflow in our CI, as long as it doesn't take too much effort. If you're a UT student, FMT employee, or research collaborator, get in touch with us so you can do your development directly in the VerCors repo, if you prefer.
• Branch cleanup: delete your branch after its PR has been merged, unless you plan on continuing development on it. Don't leave it lying around unused.
• Quality control: on the dev & master branch, all tests (except flaky ones) should pass, and all files should be formatted using the auto formatter. On your own branch you can pretty much do whatever you want.

Example workflow

Below you can find a description of what a typical workflow looks like.

1. Determine what you want to fix.
2. If there is an issue for what you want to fix, assign yourself to the issue. This can be done by navigating to the specific page of the issue. Then on the right-hand side there is an "Assignees" header. Beneath this header click on "assign yourself".
3. Ask for permissions to push to the main VerCors repository. We prefer to keep an eye on evolving development by asking contributors to work in branches of the main repository. Alternatively, you can work in your own fork (but e.g. continuous integration will not work).
4. Navigate to the VerCors project on your computer in your terminal.
5. When you're inside the vercors directory, create a new branch by executing the following command: git branch branch_name. Replace branch_name by the name for your branch. This name can reflect what you will fix. For example if you are going to fix issue 1, then you can name the branch "issue1". Or if you add support for automatic generation of invariants, then you can name the branch "automaticInvariants".
6. Then switch to the new branch using the command git checkout branch_name.
7. You can now start working on your problem!
8. When you are done with your fix, commit and push your changed files to the branch. To push to your new branch you can use the following command:git push origin branch_name.
9. Navigate to the main GitHub page of VerCors (https://github.com/utwente-fmt/vercors/).
10. Create a new pull request (see also: https://help.github.com/articles/creating-a-pull-request-from-a-fork/).
11. GitHub will run the tests, check that there are no unresolved comments on the pull request, and verify the tests have run with the most recent upstream changes.
12. As soon as this pull request has been reviewed by at least one person, and is accepted, then your fix can be merged into the master branch. Congratulations you're done with this PR (Pull Request)!

Project Structure

Functional Overview

VerCors verifies programs by going through four stages:

• The frontend, or parsing: in this step a collection of files is read and parsed into COL, the common object language. This is the internal intermediate representation of programs in VerCors.
• Resolution: here we figure out what names in the AST mean. Every name must point to (part of) a declaration. Afterwards, we forget about the name and only remember a pointer to the relevant declaration.
• The rewrite stage: The COL AST (usually referred to as just the AST) is transformed into a different AST, or it is checked for some property, together called a "pass". Depending on user-supplied options many passes are applied to the AST. They can be divided in several categories:
  • Reducing a feature: The subset of COL used is reduced, by encoding the proof obligations of a language construct in some other way. An example is that we reduce for loops to while loops, by placing the initialization before a new while loop, retaining the condition, and appending the update to the end of the loop body.
  • Checking for consistency: in some places it is useful that the type structure of the AST is not as strict as the set of ASTs we want to allow. Almost all checks are done in the type check, a single pass executed many times.
  • Standardization: many passes expect certain properties to be true about the AST (e.g. "expresions have no side effects"), but on the other hand it is useful not to constrain passes too much in what they can generate. Therefor we standardize the AST between passes, to reduce simple language features.
  • Importing builtins: some features are supported by importing a header of sorts into the AST.
  • Optimization: optimizing passes transform the AST (in particular expressions) such that they are faster to prove, or rely less on heuristics of the backend.
• The backend, or verification: the very much reduced AST is transformed once more, into the language of the selected backend. The backend makes a judgement on the program. This judgement is translated back into useful information about the program.

There are also a few cross-cutting concerns:

• The origin system tracks how the frontend parse tree is transformed via COL into a backend language. This means that if a message from the backend mentions a part of the AST in the backend language, it can be translated all the way back to its origin in the frontend input.

Technical Setup

The VerCors project sources are managed on GitHub, at https://github.com/utwente-fmt/vercors. The unstable development branch is dev, from where we branch to develop new features and bugfixes. Those with access may push feature branches to the main repository, or create a fork if they prefer. A pull request is then made and reviewed by someone appropriate.

Pushed commits as well as pull requests are checked via continuous integration, currently Github Actions. Github builds Vercors and runs the test suite. Once the checks pas and a code review is completed, the PR is merged in dev. In dev is also where we hope to notice bad interactions between new features.

We aim to make a new VerCors release once per month, which is done via a tagged merge commit to the master branch, followed by a GitHub release.

VerCors is written in java and scala. Code is accepted in either language, but we encourage you to take the time to learn some Scala - it is much better suited to manipulating ASTs. The build structure is defined in the mill build tool.

Project Structure

NB: this information quickly becomes out of date as vercors is refactored.

/

• build.sc is the root build definition. It configures global plugin options, wires sub-project dependencies, configures run-time build information, denotes external dependencies, configures metadata about the project and configures compiler options.
• mill/mill.bat bootstrap and run the build tool Mill.