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 often used to demonstrate and test the capabilities of VerCors.

In this tutorial, we will first take a brief look at what software verification is, and where VerCors fits in. Then, we will discuss the syntax of PVL and 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.

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 when the sun is shining. 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, 2 or 4", they say "the interval [1,4]", thereby also including the value 3). 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. Chapter 3 of this tutorial describes the syntax for these annotations.

Two important categories of annotations are assumptions and assertions. The tools then try to prove: If before executing a piece of code, the assumptions hold, then afterwards the assertions hold. 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 that no division by zero occurs, and even that the result is between 0 and 10. These specifications are the pre-condition and post-condition of the method, respectively. When analysing the method's body, the pre-condition is assumed, and the tool tries to assert the post-condition. When the method is used, i.e. another part of the code invokes for instance foo(42), then the tool tries to assert the pre-condition before the method invocation (i.e. check that it is allowed to call the method like this), and then assumes the post-condition. This makes the analysis modular. Note that if the pre-condition is unsatisfiable (e.g. two contradictory conditions, or a simple false), then verifying the method will succeed with any post-condition, because the implication "if pre-condition then post-condition" is trivially true. Thus, users must be careful in their choice of assumptions.

VerCors

As mentioned above, VerCors is a static verification tool that relies on annotations in the code specifying its behaviour. It 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 all the other threads, VerCors uses 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. 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. 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. 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. So 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 CSL as their logical foundation. For more info on CSL, ownership and permissions, see Chapter 4.

While VerCors currently supports Java, C (incl. OpenMP), OpenCL and PVL, it is designed to be modular, in the sense that extensions to other input languages (like, for example, C#) with parallel and concurrent language constructs 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 high-level programming languages (e.g. VCC only allows to verify C programs). Moreover, VerCors is not designed to be language-dependent, but instead focusses on verification techniques for general concurrency patterns.

Underneath the Hood

In case that you are interested in the architecture within VerCors, here is a brief introduction: VerCors parses your input file(s), which contain the program in the target language (e.g. Java) as well as the specifications, into an abstract syntax tree (AST). It then traverses the AST multiple times to perform various checks (e.g. type check) and transformations. It then passes the modified AST on to the Viper backend (some of the transformations are for example needed to turn your program into something Viper understands). Viper then performs the actual analysis, using the SMT solver Z3. The results from Z3 / Viper are then related back to your original input file(s) and presented to you in a more human-understandable way.

Installing and Running VerCors

You can install VerCors by either using a release (recommended for beginners), or by building VerCors from its source code.

Using a Release

Installation

VerCors requires a java runtime environment (version 8 or later), as well as clang if you want support for C.

Linux

Currently we support debian-based systems; let us know if you need something else! Install the dependencies:

sudo apt install clang openjdk-8-jre 

Obtain the latest deb release of VerCors here, and install it by running:

sudo dpkg -i Vercors_x.y.z_all.deb

Mac

You can for example obtain the dependencies through homebrew:

brew cask install java

This should install the latest release of OpenJDK. Clang should already be installed through XCode.

Obtain the latest zip release of VerCors here and unzip it. You can find the run script for VerCors in the bin subdirectory.

Windows

You can obtain a java runtime environment e.g. here. Make sure that the environment variable JAVA_HOME points to wherever you unpack the JDK. clang can be obtained as part of the llvm toolchain here. Make sure that clang is added to the path.

Next, download the latest zip release of VerCors here and unzip it. You can find the batch script for VerCors in the bin subdirectory.

Running VerCors

The VerCors toolset can be used by running vercors --silicon <filepath>, with <filepath> the path of the (Java, C, or PVL) file to verify.

Building from source code

Installation

When building VerCors, you additionally need these dependencies:

  1. Clone the VerCors repository using git clone https://github.com/utwente-fmt/vercors.git and move into the cloned directory, cd vercors.
  2. Run sbt compile to compile VerCors.
  3. Test whether the build was successful by running ./bin/vct --test=examples/manual --tool=silicon --lang=pvl,java --progress.

The last command tests the VerCors installation by verifying a large collection of examples (from the ./examples directory). This command should eventually report that all ? tests passed. There are also instructions for importing VerCors into either eclipse or IntelliJ IDEA here.

Running VerCors

The VerCors toolset can be used by running ./bin/vct --silicon <filepath>, with <filepath> the path of the (Java, C, or PVL) file to verify.

Syntax highlighting

When writin 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.

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:

create, action, destroy, send, recv, use, open, close, atomic, from, merge, split, process, apply, label, \result, write, read, none, empty, current_thread

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. The modifier static can be added to methods that do not change any fields or call any non-static methods.

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

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 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.

In VerCors, specifications consist largely of statements, each of which has to end with a semicolon.

Depending on the input language, specification are integrated 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 @*/.

int x = 2;
//@ assert x == 2;
int y = x + 3;
/*@
assert y == 5;
@*/

Since these are simply a type of comment, regular compilers ignore them and can still compile the program. However, VerCors can interpret them. Note that this style of comment matches the JML definition, 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.

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:

int x = 2;
assert x == 2;
int y = x + 3;
assert y == 5;

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).

Expressions

In principle, the specifications extend the language of the program you analyse (such as Java, C or PVL). 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), otherwise the compiler ignoring the specifications would compute something different than the analysis tool that takes the specifications into account. As a result, for example method calls are not allowed. Note that later on, we will discuss so-called ghost code, such as defining additional variables purely for the sake of specification. Depending on the circumstances, side-effects on the state of ghost variables are allowed. But for the beginning, let's only consider specifications without side-effects.

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.

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 the generic axiomatic data types seq<T>, set<T> and bag<T> (with T being a type), which describe sequences, sets and multi-sets, respectively. For more information on them and their supported operations (such as getting the size, and indexing elements), see the respective chapter. Another new container type is option<T>. It can either take the predefined value None, or it is Some(val) with val being an expression of type T. For example, you might use

/*@
ghost option<int> x = (arr==null ? None : Some(arr.length);
@*/

(You can for now ignore the ghost keyword, it will be discussed later in this 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], with 0 meaning no permission, and 1 meaning full write access. A permission in between those values means only read access. To express these permission values, the type frac is used. 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 on 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, or need permission to access all those elements. How do you do that, especially if the size of the array is not known beforehand (e.g. user input)? To do that, VerCors supports using quantifiers in the specifications: (\forall 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. expr is the boolean expression you are interested in, such as a statement you want to assert. Note that the parentheses are mandatory. Such a quantified expression typically relates to an array, or an axiomatic data type like a seq. However, it is not restricted to such cases. Here is an example:

//@ 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), use nesting: (\forall int i; 0<=i && i<arr1.length; (\forall int j; 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 is a type that supports comparison with < (e.g. integer, fraction), 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 ...

A brief glimpse behind the curtain to the inner workings of VerCors: In the method body, VerCors might encounter a statement like x = arr[1], and it now needs to apply the generic knowledge of the quantifier to the concrete case arr[1]. This is done by instantiating the quantifier, which 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. If the instantiation would already happen eagerly when the \forall is encountered, that might generate a lot of unnecessary overhead, instantiating the expression for values that are never actually needed. In fact, depending on the type of the quantified variable and the range expression, there might be infinitely many possible instantiations. 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.

Even worse than \forall is the \exists quantifier: (\exists varDecl; cond; expr), where varDecl declares a variable, e.g. int i, cond is a boolean boundary condition like before, and expr is the expression of interest. For instance, we could use a similar example as above, but requiring that at least one array element is positive:

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

Note Because \exists quantifiers are even more likely to cause issues than \forall, they should be used with care!

Assumptions and Assertions

Two of the most important specification elements are assumptions and assertions. These are expressions that can evaluate to either true or false, depending on the program state. As explained in the introductory chapter, VerCors tries to verify that, if the assumptions hold before executing a piece of code, then the assertions hold afterwards. While other, more complex specification constructs might have a similar meaning to assumptions or assertions in certain contexts, you can explicitly provide them using the assume keyword and the assert keyword, respectively:

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

This example verifies successfully, because under the provided assumption of Line 2, the assertion in Line 4 is indeed true. Note that the assumption of Line 2 is actually contradicting the "real" state at this point. This can easily lead to "wrong" verification results, such as VerCors asserting the statement in the example despite it not actually being true. This is not an error in VerCors, it is how the concept of pre- and post-conditions works. One particularly noteworthy case is when the assumption cannot actually be true, such as two contradictory conditions (e.g. x>0 && x<0) or simply false. From such an unsatisfiable state, anything can be derived, and any assertion verifies successfully. Therefore, users have to be careful in what they specify in assumptions, and explicit assume statements should be avoided. However, they can be helpful e.g. for debugging. assert statements can also help debugging. Additionally, they can actually help in the verification process: Asserting intermediate results of a complex computation can help proving valid results that would otherwise be difficult to prove.

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.

Pre- and Post-Conditions

The concept of pre-conditions and post-conditions of methods is closely related to assumptions and assertions. Pre-conditions specify in what state the program is expected to be whenever the method is called, and post-conditions describe the state in which the method leaves the program when it is done. This leads to a modular approach to verification: To verify the body of a method, we can do localised reasoning and check: Assuming that the method's pre-conditions are true, does the method then behave correctly and generate the expected output, i.e. can the post-condition be asserted? We do not need to concern ourselves with all the different program locations where the method is called, and check all the different states the program can be in. For example we do not need to check all call sites to see what values a method parameter might have, we just assume that its value satisfies the pre-condition and focus our analysis on the method itself. In VerCors, pre-conditions are statements using the requires keyword, and post-conditions use ensures. They are placed above the method header, and these keywords can only be used in combination with a method header:

/*@ 
 requires x == 2;
 ensures y == 5;
@*/
public void foo(int x) {
  y = x + 3;
}

In this example, y is a global variable. Note that in reality, permissions would be required to access global variables (see following chapter). We omitted these here for simplicity.

The example above verifies successfully. Changing the post-condition to y==6 would cause VerCors to raise an error, due to the post-condition not being a consequence of combining the pre-condition and the method body.

Whenever the method is called, VerCors checks that the program state right before the method invocation satisfies the pre-condition, and raises an error if that is not the case. Then, it assumes that the specifications of the post-condition hold after the invocation, without considering what the method body actually does internally:

void bar() {
  int a = 2;
  foo(a);
  a = y + 5;
  //@ assert a == 10;
}

This example verifies successfully, because when the method foo is called, the value of the parameter a fulfils the pre-condition of being 2; and the post-condition implies that in Line 5, a indeed has the value 10. If we changed the initial assignment to a=1, then the pre-condition of foo would not be satisfied, and bar would fail to verify, while foo itself would still pass the checks successfully.

This leads to a modular approach to verification, where each method body can be verified independently, only relying on the pre- and post-conditions of the methods it uses, but not caring what they do internally. The pre- and post-condition of a method together form its contract. The method's behaviour is bound to be as specified in the contract, but no commitment is made regarding things not mentioned in the contract. For example, if a method foo has permission to access a global variable z and the contract does not mention the value of z, then the method is allowed to do whatever it likes to that variable. Consequently, any method bar calling foo must take into account that z could have any arbitrary value after the call to foo returns. Therefore, the author of foo should specify what happens to all the variables it has access to, even if they remain unchanged, in order to allow the developer of bar to make reasonable statements about their own method. While you might now fear that you have to specify huge contracts about all the things your method does not do, rest assured: In practice, the permissions, which a method has, restrict heavily what it can do, and it is simply impossible for foo to do anything bad to most of your precious variables, because it does not have access to them. But let this be a lesson to not be too generous with your permissions, and only give a method access to the variables it actually needs.

If something remains unchanged and you want to add it to both pre- and post-condition, you can use the short-hand notation context expr;. This is an abbreviation for requires expr; ensures expr;:

//@ context y == 5;
int incr(int x) {
  int res = x + 2*y;
  //@ assert res == x + 10;
  return res;
}

This is particularly useful when dealing with permissions, as a method will often require access to a variable, and then return this permission back to the call site.

Pre- and post-conditions are processed in-order, so swapping the order of two pre-conditions could result in a failed verification (e.g. you need to specify the permissions first, before you can use the respective heap variable in a pre-condition).

Two other interesting constructs that are often used in method contracts are \result and \old. When dealing with a non-void method like the example above, \result can be used in the post-condition to refer to the return value of the method. So we could move the assert statement in the example into the method contract as a post condition ensures \result == x+10;. The \old construct can be used to refer to the value of an expression before executing the method. This can be especially useful in post-conditions, when you want to relate the value after the method's execution to the one before, e.g. ensures y == \old(y);. However, it can also be used at any point in the body of the method to refer back to the value that the expression had at the beginning of the method. Note that you can also place more complicated expressions within \old than just a simple variable, for example an in-place algorithm to remove an element from a list might say ensures list.length == \old(list.length - 1). But one important restriction is that the expression has to be free of side effects, even on the ghost state. Obviously, \result cannot occur inside \old, as the return value is not known at the beginning of the method. So we can adapt the previous example:

//@ ensures y == \old(y);
//@ ensures \result == x + 2*y;
int incr(int x) {
  return = x + 2*y;
}

Comparing the post-condition on Line 2 with the method body, you might start to wonder whether you will now have to write everything twice, once "for real" and once for the specification. And indeed, there can be considerable overlap, sometimes to a frustrating extent. This could lead to the problem of doing the same mistakes twice: A program verifies in VerCors, thus you can be sure that it adheres to its specifications, but still it does not do what you want because the specifications contain the same error as the code. However, in many cases the specifications will be simpler than the executable code, avoiding the duplication of code and errors. Nevertheless, it can sometimes be useful to have one person write the specifications (e.g. the developer who wants to use the method), and another person writing the implementation.

Loop Invariants

So far, we have looked at rather straight-forward programs that progress linearly from the top to the bottom. For them, it was rather easy to specify "if this holds at the top, then that holds at the bottom". But what if we use loops? Now we cannot know at the end of the program whether we did the loop once, 100 times or skipped it completely. How can we make assertions about such a program? The answer are loop invariants. A loop invariant is a statement that has to evaluate to true right before the loop is entered and at the end of each loop iteration. Thereby, we can be sure that after the loop, the loop invariant holds, no matter how often it was executed. In VerCors, loop invariants are specified right above the loop header using the keyword loop_invariant:

//@ 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. 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. Note the clear similarity between analysing a method body, where we assume the pre-condition, analyse the body and try to assert the post-condition, and analysing a loop body, where we assume the invariant, analyse the body, and try to assert the invariant again. 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.

Note that, because loop bodies are analysed similarly to method bodies, you need to treat heap variables the same: If you want to use them in the loop body, you have to explicitly allow accessing them by including permissions in the loop invariant. And if a loop invariant does not mention the value of a heap variable, VerCors has to assume that it can have any arbitrary value after executing the loop. Note that this does not apply to stack variables, so the primitive integer variables in our example do not require permissions.

Because it is a common issue that you need to specify the same permissions in the method's pre-condition, post-condition and loop invariants, there is a short-hand notation context_everywhere. It extends the semantics of context, so context_everywhere expr; will add expr to the pre- and post-condition (i.e. requires expr; ensures expr;) and as an invariant to all loops inside the method's body. So if you have multiple loops inside your method's body, be careful what you put inside context_everywhere: You might give a loop permission for a heap variable without realising it, and then wonder why you cannot assert anything about the variable's value after that loop, despite the loop and its explicitly given invariants not touching it. Since context_everywhere also adds the expression to the pre- and post-condition, it can only occur in a method contract (just like requires, ensures and context).

Ghost Code

Sometimes, it is useful to write actual code just for the sake of specifications, for example to declare a helper variable. Such code is called ghost code. It is written in the framework of specifications, so for most languages, that is within the /*@ comments. As a direct consequence of that, the regular compiler is not aware of it, and the "real" code cannot reference e.g. ghost variables. Since the specification language extends the target language, any expression that is possible in the target language is also possible in ghost code, for example method definitions, variable declarations, loops, etc. Additionally, the ghost code can use the extensions that the specification language adds to the target language, so you can for instance declare a variable of type seq<T>, which is defined explicitly for specifications (see above). Like any specification, ghost code must not affect the state of the "real" program. For that reason, it is not possible to change the values of "regular" variables or call "regular" methods, as the latter may have side effects on the program state. However, it is possible to read from "regular" variables (e.g. create a ghost variable with the same value), if you have permission to access that variable. Also, it is allowed to affect the ghost state, i.e. the state of the ghost variables (e.g. change their value). So while calling a "regular" method is forbidden due to potential side effects on the program state, calling a ghost method is allowed, even if it has side effects on ghost variables. Therefore, it is important that you keep in your mind a clear separation between ghost state and "real" program state.

This is all rather abstract, so let's look at an example:

/*@
  requires arr != null ** Perm(arr[*], read);
@*/
public void whatever(int x, int y, int[] arr) {
  x = 2;
  //@ ghost int min = (x<y ? x : y);
  //@ assert (\forall int i; 0<=i && i<arr.length; min<=arr[i] && arr[i] < 2*min);
  if (arr.length > 0) {
    x = 4;
  }
  /*@ ghost 
  if (min < x) {
    assert (\forall int i; 0<=i && i<arr.length; min<=arr[i] && arr[i] < 2*min);
  }
  @*/
}

As you can see, we introduce a ghost variable min, which captures minimum of the values of x and y at a specific point in the computation (after assigning 2 to x). We already know the \old keyword to reference the state at the beginning of a method, but referencing the state in the middle of the execution is more difficult. Thus, a helper variable is an easy solution. Using this helper, the quantified assertion becomes much easier to formulate and to understand. After the first if, we use a ghost if to check our previous assertion again, but only in certain cases. Note that we have changed the value of x inside the first if, but min was not changed and thus is still based on the earlier value of x (just like a regular variable would be). Instead of the ghost if, we could have also used an implication assert boolExpr ==> expr;, but that would not showcase the use of ghost code ;)

Ghost Methods and Functions

You can use ghost code not only within regular methods: As mentioned above, ghost code supports everything the target language supports, so you can declare entire ghost methods. Here is an example of a ghost method:

/*@
requires x > 0;
ghost 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. This is due to the fact that the entire ghost method already is inside a special comment /*@, so no additional comment is needed. We then use this ghost method in the body of some_method. If cond_add were a regular method, this would not be allowed, due to the potential of side effects (even though this particular method does not have any side effects). Note that some_method has as part of its pre-condition val>0. Without this, calling cond_add would result in a failed verification, as its pre-condition might not be fulfilled at the time of the call.

Pure functions are, in a way, a special kind of ghost methods. They have the form modifiers pure return_type name(args) = expr;, where modifiers is a potentially empty set of modifiers like public or static, the return_type and name are exactly what they say, args is a potentially empty list of arguments, and expr is a single expression defining the return value of the function. So it looks like any method, except the additional keyword pure and the fact that the body is a single expression following an =, rather than a block of statements. The important distinction to normal methods, apart from the fact that they have just one expression, is that pure functions must be without side-effects, even on the ghost state. Thus, the body expr cannot contain for instance calls to methods or variable assignments. Another consequence is that, while regular methods must return permissions explicitly in the post-condition, pure functions automatically return all their permissions, and the post-condition must not include permissions (see next chapter on Permissions). Since the example ghost method above actually does not have side-effects, we can turn it into a pure function using a ternary expression:

/*@
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 statement or declaration from the target language (e.g. if, method definitions, etc), not for specification-internal constructs like defining a pure function. However, calling the pure function as a stand-alone statement (e.g. invoking a lemma) is seen as a method call from the target language, and therefore needs the ghost keyword: //@ ghost myLemma();.

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.

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 and not on the body, 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 of 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, if you modified parts of your code and want to re-run the analysis, this can be an interesting option to speed up the repeated analysis: You first check the part of your program that you will not touch with the respective bodies in place. Once that verifies and you are certain that the post-conditions are realistic, you can make the methods abstract while you focus on the rest of your program. Thereby, VerCors does not have to re-analyse those methods every time you change other parts of your code.

Syntactically, an abstract method or function has a semicolon in place of its body (similar to method declarations e.g. in C header files):

//@ 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

Programmers, who are familiar with for example C, know about the existence and the power of #define: You can write an expression that occurs frequently in your code as a define and then use it as if it were a function. However, the pre-processor of the compiler replaces every call to that function with the respective expression, so no real function call occurs, reducing e.g. performance overhead. A similar concept in VerCors are inline functions: Before verifying the program, VerCors also replaces every call to an 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 inlining resources (see chapter on resources), where boolean conditions that often occur together (e.g. permissions for all the fields of an object of a certain type) are grouped together and are treated similarly to inline functions.

Ghost Parameters and Results

So far, we have seen ghost code extending the body of an existing method, and being an entire method. You can also 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 with and then, respectively:

/*@
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) /*@ with {y=3; x=2;} then {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. However, as stated before, the method contract is processed in the order it is given, so the given int x; must appear before the requires that mentions x. 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 with keyword is followed by a block of statements that assign values 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 then keyword is followed by a block of statements that can use the ghost result, in particular storing their value in local variables. The respective local variable, who_cares, must be a ghost variable, otherwise you would affect the state of the "real" program. Both the with and the then are placed in a specification comment between the method call and the respective semicolon.

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.

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 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).

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.

OpenCL/Cuda/GPGPU

TODO @Mohsen

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:

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

and this method shows the same example in CUDA:

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

In both examples, first we should include the header files (i.g., opencl.h and cuda.h) as in line 1. Next we obtain thread identifiers and then each thread does the computation (lines 10-11 of OpenCL and 11-12 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 line 7 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".

OpenCL/CUDA with Barrier

This example shows an OpenCL program that uses barrier to synchronize threads:

1   #include <opencl.h>
2
3   /*@
4   context_everywhere opencl_gcount == 1;
5   context_everywhere array.length == size;
6   requires get_local_id(0) != size-1 ==> \pointer_index(array, get_local_id(0)+1, 1\2);
7   requires get_local_id(0) == size-1 ==> \pointer_index(array, 0, 1\2);
8   ensures \pointer_index(array, get_local_id(0), 1);
9   ensures get_local_id(0) != size-1 ==> array[get_local_id(0)] == \old(array[get_local_id(0)+1]);
10  ensures get_local_id(0) == size-1 ==> array[get_local_id(0)] == \old(array[0]);
11  @*/
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     /*@
22     requires get_local_id(0) != size-1 ==> \pointer_index(array, get_local_id(0)+1, 1\2);
23     requires get_local_id(0) == size-1 ==> \pointer_index(array, 0, 1\2);
24     ensures \pointer_index(array, get_local_id(0), 1);
25     @*/
26     barrier(CLK_LOCAL_MEM_FENCE);
27
28     array[tid] = temp;
29 }  

And this is the CUDA version of the example:

1   #include <cuda.h>
2
3   /*@
4   //context_everywhere opencl_gcount == 1;
5   context_everywhere array.length == size;
6   requires threadIdx.x != size-1 ==> \pointer_index(array, threadIdx.x+1, 1\2);
7   requires threadIdx.x == size-1 ==> \pointer_index(array, 0, 1\2);
8   ensures \pointer_index(array, threadIdx.x, 1);
9   ensures threadIdx.x != size-1 ==> array[threadIdx.x] == \old(array[threadIdx.x+1]);
10  ensures threadIdx.x == size-1 ==> array[threadIdx.x] == \old(array[0]);
11  @*/
12  __kernel void openCLLeftRotation(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     /*@
22     requires threadIdx.x != size-1 ==> \pointer_index(array, threadIdx.x+1, 1\2);
23     requires threadIdx.x == size-1 ==> \pointer_index(array, 0, 1\2);
24     ensures \pointer_index(array, threadIdx.x, 1);
25     @*/
26     __syncthreads();
27
28     array[tid] = temp;
29 }  

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 range 0 to "size-1" and "tid" is used to refer to each thread 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 in a 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 29).

Axiomatic Data Types

This page discusses the axiomatic data types (ADTs) that are supported by VerCors. Some of these ADTs like sequences and sets are natively supported by the Viper toolset, the main back-end of VerCors. ADTs that are not natively supported, like matrices, vectors, and option types, are specified as domains in the config/prelude.sil file (specified in the Silver language). During the translation steps in VerCors, the SilverClassReduction class includes all domains that are needed to verify the input program.

Bags

The notation bag<T> is used by VerCors to denote the type of bags with elements of type T. Bags are immutable and similar to sets; in fact they are multi-sets, meaning that bags permit duplicate elements. For instance, unlike ordinary sets the multi-set {1,1,2,4} is not equal to {1,2,4}. An integer bag can be declared in VerCors using the following syntax:

bag<int> b = bag<int> { 1, 1, 2, 4 };

The notation bag<T> { } is used to denote an empty bag of type T. Given a bag b, the notation |b| is used to denote the size of b, that is, the number of elements in b. For example, one could verify:

bag<int> b = bag<int> { 1, 1, 2, 4 };
assert |b| == 4;
assert |bag<int> { 7, 8 }| == 2;

Please note that in some languages (like Java), |= is an operator. It is therefore recommended to put spaces between the size operator and any subsequent comparison or implication (==>), i.e. |b| == n instead of |b|==n. This avoids ambiguity for the parser.

Bag multiplicity

Given an integer bag b, the notation 2 in b can be used to test whether 2 occurs in b (similar to testing for set membership, see also the section on Sets). However, bags may contain duplicate elements. Therefore, 2 in b does not give a boolean value (like with set membership), but instead yields an integer value denoting the number of occurrences of 2 in b. In other words, 2 in b denotes the multiplicity of 2 in b. For example, one may verify:

bag<int> b = bag<int> { 1, 2, 2, 2, 4 };
assert (2 in b) == 3;
assert (1 in b) == 1;
assert (3 in b) == 0;

Bag union

Given two bags bag<T> b1 and bag<T> b2 of the same type T, the union of b1 and b2 is written b1 + b2 and denotes the bag containing all elements of b1 and b2 (and thereby allowing duplicates). For example:

bag<int> b1 = bag<int> { 1, 2 };
bag<int> b2 = bag<int> { 2, 3 };
assert |b1 + b2| == 4;
assert b1 + b2 == bag<int> { 1, 2, 2, 3 };
assert (1 in b1 + b2) == 1;
assert (2 in b1 + b2) == 2;

Bag difference

Given two bags b1 and b2 of the same type, the bag difference (i.e. the relative complement) of b1 and b2 is written b1 - b2. In other words, b1 - b2 denotes the set b1 with all elements occurring in b2 removed (of course by keeping multiple occurrences of elements into account). For instance:

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

Bag intersection

Given two bags bag<T> b1 and bag<T> b2 of equal type T, the intersection of b1 and b2 is written b1 * b2 and denotes the bag containing all elements that occur both in b1 and b2 and thereby keeping multiplicity into account (unlike ordinary set intersection). As an example, one may verify the following program:

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

Future enhancements

Given a bag b, VerCors currently does not support shorthand notations for adding or removing elements from b, like b += 3 and b -= 2. In essence, the notation b += 3 can be rewritten to b += bag<int> { 3 } (by inferring the bag type, in this case int), which can in turn be defined as shorthand for b = b + bag<int> { 3 }. The same reduction pattern would apply for -=.

We could introduce the notation v member b as a shorthand for (v in b) > 0, thereby returning a boolean result. We may even reuse the notation v in b for this, perhaps depending on the context.

Maps

VerCors does not have support for maps yet. As a future enhancement we may implement support for maps, for example using the notation map<T,U> m, where T denotes the type of all keys of m (i.e. the type of the domain of m) and U denotes the type of the values of m (i.e. the codomain type).

Option Types

The notation option<T> is used to denote the option data type: the type that extends the given type T with an extra element named None. More specifically, elements of type option<T> are either None or Some(e), where e is of type T. For example, the option integer type can be declared in VerCors using the following notation:

option<int> field1 = None;
option<int> field2 = Some(3);

Axioms are provided so that None != Some(e) for every element e, and for every e1 and e2 we have Some(e1) == Some(e1) only if e1 == e2.

Sequences

VerCors uses the notation seq<T> to denote sequence types: the type of sequences with elements of type T. Sequences represent ordered lists and are immutable; once created they cannot be altered.

Construction

Sequences of type T can be constructed using the notation seq<T> { E_0, ..., E_n }, where E_i is of type T for every i. For example, seq<int> { 1, 2, 3 } is the constant sequence of three elements: 1, 2, and 3. In PVL this sequence can be constructed by writing:

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

Naturally, the notation seq<T> { } is used to denote the empty sequence of type T.

Two sequences s1 and s2 are equal if they are: of equal length, of equal type, and if their elements are equal pair-wise. To test for equality the standard operator for equality s1 == s2 can be used. The notation |s| is used to obtain the length of the sequence s. As with bags, it is recommended to put a space between the length operator and any subsequent comparison or implication, to avoid ambiguity with the |= operator when the code is parsed. In PVL one may for example verify:

seq<int> s = seq<int> { 1, 2, 3 };
assert |s| == 3;
assert |seq<int> { 1, 2, 3, 4 }| == 4;

Indexing

A sequence seq<T> xs may be indexed at position i, written xs[i], to retrieve the i-th element of xs. For example, the following should verify:

seq<int> xs = seq<int> { 1, 2, 3 };
assert xs[0] == 1;
assert xs[2] == 3;

However, the current version of VerCors is rather limited in its indexing support. For example, the line assert seq<int> { 1, 2, 3 }[0] == 1 gives a syntax error. This is because the left-hand side E1 of any indexing notation E1[E2] can not be an arbitrary expression of type seq<T>, but most be exactly a sequence of type T. To solve this, one can either declare the sequence explicitly, like in the code example given above, or define an auxiliary get function as given below, and write get(seq<int> { 1, 2, 3 }, i) instead.

static pure int get(seq<int> xs, int n) = xs[n];

Concatenation

Two sequences seq<T> s1 and seq<T> s2 of the same type T can be concatenated by using the plus operator: s1 + s2. For example in PVL one may verify:

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

Axioms are provided to make sequence concatenation associative, s1 + (s2 + s3) == (s1 + s2) + s3, and to make the empty sequence neutral in the sense that s + seq<T> { } == s and seq<T> { } + s == s.

Head-tail notation

VerCors has built-in functions for obtaining the head and tail of a sequence, which are named head and tail. The head(s) function simply gives the first element of s, provided that such an element exists, and tail(s) gives the tail sequence of s. For example:

seq<int> s = seq<int> { 1, 2, 3 };
assert head(s) == 1;
assert tail(s) == seq<int> { 2, 3 };

The head of an empty sequence is undefined. The tail of an empty sequence is empty:

seq<int> s = seq<int> { };
assert tail(s) == seq<int> { };

Future enhancements

There is currently no alternative notation to construct sequences from elements, like [1,2,3], but this would be a nice enhancement.

VerCors does not yet permit slicing notations for sequences. For example, s[2..] should denote the subsequence of s starting from index 2. The Viper toolset currently supports these notations.

Another enhancement would be an append operator ::, so that 2 :: s would be equal to seq<int> { 2 } + s. Then head(2 :: s) == 2 and tail(2 :: s) == s. Providing support for :: does not seem that hard, merely a matter of syntactic transformation.

Like in Dafny we could give support for the membership operators in and !in, so that v in s equals true only if v is contained in s (and likewise v !in s only if !(v in s)).

Sets

The notation set<T> is used by VerCors to denote the type of sets with elements of type T. Sets are immutable, orderless (meaning that the elements are not ordered), and do not allow duplicates (the sets {1,1,2} and {1,2} are equivalent). As an example, a set of integers can be declared as follows:

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

The empty set of type T is denoted set<T> { }, the singleton set is denoted set<T> { e } (with e of type T), et cetera. As said before, sets do not permit duplicate elements and are orderless:

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

Set membership

Given a set set<T> s of type T and an element T e (an element e of type T), we may test whether e is a member of s by writing (e in s). The in operation yields a Boolean result when applied to sets, indicating whether the given element (e.g. e) occurs in the specified set (e.g. s). For example:

set<int> s = set<int> { 1, 2, 3 };
assert (2 in s);
assert !(8 in s);

Set union

The union of two sets set<T> s1 and set<T> s2 of the same type T is written s1 + s2 and denotes the set containing all elements of both s1 and s2 (that is, without duplicates). For example:

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

Set difference

Given two sets set<T> s1 and set<T> s2 of the same type T, the set difference of s1 and s2 is written s1 - s2 and denotes the set of all elements that are in s1 but not in s2. A simple verification example is given below.

set<int> s1 = set<int> { 1, 2, 3, 4 };
set<int> s2 = set<int> { 2, 3, 5 };
assert s1 - s2 == set<int> { 1, 4 };

Set intersection

Given two sets set<T> s1 and set<T> s2 of the same type T, the intersection of s1 and s2 is written s1 * s2 and denotes the set containing all elements that are in both s1 and s2. For example:

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

Future enhancements

We do not have a subset notation yet. For example, given two sets s1 and s2 of equal type, VerCors might be extended with the notation s1 <= s2 to test whether s1 is a subset of s2. In the same way, s1 < s2 might be used as notation for strict subset testing.

Another nice extension would be a notation for set comprehension. For example, the notation set<int> { n | n >= 0 } might denote the set of all non-negative integers.

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 statement 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

Internals

Parallel Blocks

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

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 and an arbitrary name after that defines the name of that block. Moreover, we should define the number of threads in the parallel block and an arbitrary name as thread identifier. In this example, we have "size" threads in range 0 to "size-1" and "tid" is used to refer to each thread as thread identifier.

In addition to the specification of the method (lines 1-6), we should add thread-level specification into 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 in 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). Then, 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 addition of two corresponding locations in arrays "a" and "b" (line 11). From the postcondition of the parallel block, we can specify the postcondition of the method using universal quantifier for all locations in the arrays (line 3-6).

Parallel Block with Barrier

We demonstrate an example of a parallel block which needs barrier to synchronize threads:

1 context_everywhere array != null && array.length == size;
2 requires (\forall* int i; i >= 0 &&  i < size; Perm(array[i], 1\2));
3 ensures (\forall* int i; i >= 0 &&  i < size; Perm(array[i], 1));
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], 1\2);
10    requires tid == size-1 ==> Perm(array[0], 1\2);
11    ensures Perm(array[tid], 1);
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      {
24        requires tid != size-1 ==> Perm(array[tid+1], 1\2);
25    requires tid == size-1 ==> Perm(array[0], 1\2);
26    ensures Perm(array[tid], 1);
27      }
28
29      array[tid] = temp;
30   }
31 }

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 range 0 to "size-1" and "tid" is used to refer to each thread 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 in a 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 29).

To verify this method in VerCors, we should annotate barrier in addition to the 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 into its own location (lines 24-26). When a thread reaches a barrier, it has to fulfill the barrier preconditions, and then it may assume the barrier postconditions. Thus barrier postconditions must follow from barrier preconditions.

As postcondition of the parallel block (1) first each thread has write permission to its own location (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). Note that the keyword "\old" is used for an expression to refer to the value of that expression before entering a method.

Atomics and Locks

TODO @Raul (+invariants)

Models

TODO @Raul (Histories + Futures)

Resources and Predicates

TODO @Bob

Inheritance

TODO @Bob

Exceptions & Goto

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

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.

Feature Supported
throw Yes
throws Yes
try-catch Yes
try-finally Yes
try-catch-finally Yes
try-with-resources No
Multi-catch No
Defining custom exceptions Yes, but only if directly inheriting from one of: Exception, RuntimeException, Throwable, Error. This limitation is temporary.
JML signals Yes
JML signals_only No

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 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 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 post condition in case an exception is thrown. The declared post-condition 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) {
    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 are 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. It is not guaranteed that an exception is thrown if a signals condition occurs.

While VerCors does not support the other signals semantics natively, there is a way to model it 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.

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. A downside of this is that the VerCors exception semantics do 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.

In other words, 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. Conversely, 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. 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() {
    
}

Goto and labels

PVL has support for goto and label. 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.

Term Rewriting Rules

VerCors allows you to define your own term rewriting rules via jspec 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.

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)!

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.

PVL Syntax Reference

On this page you can find a description of the syntax of PVL, Prototypal Verification Language; one of the languages for which VerCors supports verification.

General

  • Identifiers can consist of the characters a-z, A-Z, 0-9 and _. However, they must start with a letter (a-z, A-Z). 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.
  • The keyword this is used to refer to the current object.
  • A program is typically defined within a class:
class ClassName {
    // Here you can add any constructors, class variables and method declarations
}
  • You can write single-line or multi-line comments as follows:
// This is a single-line comment
/* 
    This is a 
    multi-line comment 
*/
  • Lines in PVL should end with a semi-colon ;.
  • Unlike JML, PVL specifications are not written in comments!

Types and Data Structures

Type Description
int Integer
boolean true or false
void Used when a method does not return anything
resource Boolean-like type that also allows reasoning about permissions
frac Fraction
zfrac Fraction that can also be zero.
process Type of actions and defined processes in histories. For more information on histories & futures, have a look at the section on Histories & Futures.
T[] Array which contains elements of type T. T should be replaced by a type. Note that when you initialize a new array, you should always define the length of the array, e.g. new int[3] instead of new int[].
seq<T> var Defines an immutable ordered list (sequence) named var. T should be replaced by a type.
set<T> var Defines an immutable orderless collection (set) that does not allow duplicates. T should be replaced by a type.
bag<T> var Defines an immutable orderless collection (bag) that does allow duplicates. T should be replaced by a type.
option<T> Extends type T with an extra element None. Each element is then either of the type None or of the type Some(e) where e is of type T. T should be replaced by a type. Options cannot be unpacked at the moment.

For more information on sequences, sets, bags and options, have a look at the wiki page on Axiomatic Data Types.

Expressions

Infix Operators

Code Description
==, != Equals and not equals for reasoning about the equality of expressions
&&, ||, ! And, or, and negation respectively for reasoning with boolean variables.
<, <=, >, >= Smaller than, smaller than equals, greater than and greater than equals respectively. They are used to compare integers.
+, -, *, /, \ Addition, subtraction, multiplication, integer division and fractional division respectively.
++, -- Increase by 1 and decrease by 1 respectively. Unlike the other operators, this only requires an variable on the left-hand side.
==> Implication. This statement evaluates to true unless the statement before the arrow evaluates to true and the statement after the arrow evaluates to false.
** Separating conjunction. a ** b denotes that a and bpoint to different variables on the heap and that both expressions mus tevaluate to true. This is used to reason about multiple resources.
-* Magic wand or separating implication. This is used to reason about resources. //TODO: investigate what is supported.
new T() Creates a new object of type T.
new T[length] Creates a new array which contains objects of type T with length number of items.
boolExpr ? exprA : exprB; Evaluates boolExpr, if this is true it will return exprA and otherwise exprB.

Quantified Expressions

Code Description
(\forall vars; range; boolExpr) Construct that allows you to repeat a certain expression for several variables. For example, (\forall int j; j >= 0 && j < n; array[j] >= 0) denotes that all elements in array nonnegative. It is equal to the following statement: array[0] >= 0 && array[1] >= 0 && ... && array[n-1] >= 0. vars should declare the variables over which we will reason. range can be any boolean expression, often used to describe the range of vars. boolExpr is some expression that should evaluate to a boolean for all variables in the given range.
(\forall* vars; range; expr) Similar construct to the \forall except that the expressions are separated by ** instead of &&. One can for example write (\forall* int j; j >= 0 && j < array.length; Perm(array[j], write) which denotes that the thread has writing access to all elements in array.
(\exists Type id; range; expr) Evaluates to true if there exists an element, called id, such that the final expression evaluates to true.
array[*] This is a simplified \forall* expression that ranges over all elements in the array array. Instead of the example mentioned above for \forall*, you can then write Perm(array[*], write). This cannot be used within nested \forall* expressions.

Specification-only Expressions

Code Description
\result Keyword that refers to the object that the method returns
\old(expr) Refers to the value of the specified expression in the pre-state. This can be used in a postcondition (ensures) or loop invariant in which case the pre-state is when the method was called.
held(x) Check whether you are holding a non-reentrant lock. x should refer to the lock invariant. See also: Queue.pvl.
idle(t) Returns true if thread t is idle (before calling t.fork() or after calling t.join()). Overall a thread starts as idle, if the thread is forked, it goes to a 'runnning' state. If join is called on a running thread, then it goes back to an 'idle' state.
running(t) Returns true if thread t is running. Overall a thread can go through the following states: idle --[t.fork()]--> running --[t.join()]--> idle

Resources

Code Description
Perm(var, p) Defines permissions for variable var. If p is 1 or write then it denotes write permission, anything between 0 and 1 or read denotes read permission. Be aware that you cannot use arithmetic when using read such as read/2 or dividing read among multiple threads! Perm() is of the type Resource.
PointsTo(var, p, val) Denotes permissions p for variable var similar to Perm(). Moreover, variable var points to the value val. PointsTo() is of the type Resource.
Value(var) Defines a read-only permission on the given variable. This read-only permission cannot become a write permission and it can duplicate as often as necessary.

Control flow constructs

Control flow construct Example
Function contract returnType functionName(paramType paramName, ...) { ... }. contract should describe the specification of the method. returnType should be replaced by a specific type or void depending on what (if anything) the method returns. functionName should be replaced by the name of the function. paramType paramName, ... is a comma-separated list of parameters, for every parameter you should define its type and its name. It is also possible to have no parameters. For example: ensures \result == a + b; int sum(int a, int b) { return a + b; } is a function which returns an integer that is the sum of the parameters given.
Pure and Abstract Functions: Pure functions are declared by prepending modifiers static and pure in that order. They should be side-effect free and their postconditions must not contain resource assertions such as accessibility predicates. All accessibility constraints for the body of the function and for the postcondition should be ensured by the preconditions. In fact, since pure functions applications are side-effect-free, pre- and post-states of a function application are the same. Example:
requires a != null;
requires 0 <= n && n <= a.length;
requires (\forall* int j; 0 <= j && j < a.length; Perm(a[j],1\2));
ensures (n==a.length)? \result == 0 : \result == a[n] + sumAll(a,n+1);
static pure int sumAll(int []a, int n);
Notice that in the example the function has no body. By doing so we declare an abstract function. When calling this function, its pre-conditions will be checked and its postconditions assumed. No correspondence should be assumed between pure and abstract functions.
Return return can be used to exit the current method. return expr can be used within a method to return a specific object as a result.
If-statement
  • Single-line option: if (boolExpr) ...;
  • Multi-line option: if (boolExpr) { ... }
If-then-else if (boolExpr) { ... } else { ... }
For-loop loop_invariant p; for (...) { ... }
While-loop loop_invariant p; while (boolExpr) { ... }
Parallel block par contract { ... } OR par identifier(iters) contract { ... }. The identifier is optional and iters can be empty. iters specifies what variables are iterated over. Note that you can also extend a parallel block with another parallel block as follows: par contract { ... } and contract { ... } OR par identifier(iters) contract { ... } and identifier(iters) contract { ... }.
Vector block vec (iters) { ... } is a variant of the parallel block where every step is executed in lock step. You do not need to specify a pre- and postcondition. iters should define what variables are iterated over, e.g., int i = 0..10.
Atomic block atomic(inv) { ... } performs the actions within the block atomically. As a result, other threads will not be able to see any intermediate results, only the result before or after executing the atomic block. inv refers to an invariant which stores permissions that are necessary when executing the atomic block.
Barrier barrier(identifier) { contract } waits for all threads to reach this point in the program, then permissions can be redistributed amongst all threads, as specified in the contract, after which the threads are allowed to continue. The barrier needs to know how many threads should reach it before everyone is allowed to continue, this is done by specifying identifier which refers to a parallel block before the barrier.
Fork a thread fork expr starts a new thread.
Join a thread join expr waits for the specified thread to complete.
Wait wait expr will pause the thread until it is notified to continue.
Notify notify expr will notify another thread that it may continue if it is waiting.
Acquire a lock lock expr
Release a lock unlock expr
Label label l indicates a location in the program that can be jumped to with goto l.
Goto goto l indicates control flow must be transferred to the location of the label l.

Note that for-loops and while-loops should be preceded with a contract consisting of one or more loop invariants. Parallel blocks require a contract in the form of requires/ensures clauses.

Verification flow constructs

Code Description
assert expr Defines an assert statement expr which describes a condition that should hold at the program point where this statement is defined.
assume expr Defines a statement that assumes that expr holds. It can be put anywhere within the code.
requires expr Defines the precondition as expr, i.e., expr must hold when calling this method. The precondition should be specified before the method declaration.
ensures expr Defines the postcondition as expr, i.e., expr must hold when completing this method. The postcondition should be specified before the method declaration.
context expr This is an abbreviation that combines the statements requires expr and ensures expr. This statement should be specified before the method declaration.
loop_invariant expr Defines a loop invariant expr which is a condition that must hold when entering the loop and after each loop iteration. A loop invariant should be specified before the corresponding loop.
context_everywhere expr This is an abbreviation that combines the statement requires expr and ensures expr. Moreover, it also adds loop_invariant expr to all loops within the method. This statement should be specified before the method declaration.
given T p Defines that a ghost input parameter (specification-only parameter) of type T with the name p is passed when this method is called. This statement should be specified before the method declaration.
yields x Returns a ghost output parameter (specification-only parameter) to the callee of this method. This statement should be specified before the method declaration.
with ... then ... with is used to pass a parameter to a method (which has a given statement) and then can be used to store a returned value from a yields statement. This statement is specified after the corresponding method call (on the same line) where you want to pass the parameter. All the ... should be replaced by an assignment.
unfolding ... in expr Temporarily unfold definitions in (pure) expressions. The ... should be replaced by a predicate.
refute expr Disproves expr at the given program point. This statement can be put anywhere in the code. Internally it is translated to assert !(expr).
inhale p Take in the specified permissions and properties.
exhale p Discard the specified permissions
fold x Wrap permissions inside the definition
unfold x Unwrap a bundle of permissions
witness x Declares witness names. This feature is deprecated and should no longer be used.

Histories & Futures

Defining processes

Code Description
process Type of actions and defined processes in histories.
process1 + process 2 Do either process1 or process2
process1 * process 2 Sequential composition, do process1 followed by process2
process1 || process 2 Parallel composition, do process1 and process2 at the same time (interleaved)
Code Description
History hist Declare a History object called hist
HPerm(var, p) History-specific permissions where var refers to a variable in the history and p is the amount of permissions (a value between 0 and 1)
Hist(var, p, val) Similar to PointsTo, it denotes permissions p for variable var (which is in a history). Moreover, variable var points to the value val.
AbstractState(h, boolExpr) This can be used to check that the given boolean expression holds in the history (or future) h
action(h, perm, preState, postState) { ... } The action describes how the state of the history (or future) is changed by the code within { ... }. The pre- and post-state describe the state of the history (or future) in terms of processes. perm describes the permissions we have on the history (or future) and h is the name of the history (or future)
create h Create a history. Note that the History class should be instantiated beforehand.
destroy h, val Destroy a history h which has the value val
split h, p1, val1, p2, val2 Split a history (or future) into two such that the first part has permissions p1 and value val1 and the second part has permissions p2 and value val2
merge h, p1, val1, p2, val2 Merge two histories (or futures) such that resulting history h has permissions p1+p2 and consists of combination of the actions described in val1 and val2
modifies vars List of locations that might be modified
accessible vars List of locations that might be accessed
Code Description
Future f Declare a Future object called f
Future(f, p, val) It denotes that we have permissions p on future f of which the state is val
choose f, p1, pre, post //TODO check this support and definition
create f, val Create a future f with the initial state val
destroy f Destroy the future f

Other

  • APerm ??
  • Ls: send p to Lr, d | Release permissions p to the statement labelled Lr with d being the distance of dependence. This statement is labelled Ls.
  • Lr: recv p from Ls, d | Acquire permission p from the statement labelled Ls with the distance of dependence d. This statement is labelled Lr.
  • Iteration contract | An iteration contract specifies the iteration's resources. The precondition of an iteration contract specifies the resources that a particular iteration needs, and the postcondition specifies the resources that become available after the execution of the iteration.
  • \pointer(var, length, perm), \pointer_index(...)?

Developing for VerCors

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. Create a fork of VerCors if you have not done this yet. The installation instructions can be found on the main Github page (https://github.com/utwente-fmt/vercors).
  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. 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)!

Review guidelines

Below you can find a list of things to take into account when reviewing a pull request. Note that these are also things that you can take into account before submitting a pull request.

  • Are all newly added pieces of code/methods documented?
  • Are there no hardcoded Strings/integers/etc.?
  • Are pieces of code not repeated?
  • Can all (correct) examples (in the examples directory) still be verified without errors?

All questions above should typically be answered with "Yes". If not, then you may want to request changes on the pull request before accepting the changes.

Project Structure

Functional Overview

VerCors verifies programs by going through three 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.
  • 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.
  • Logging: we have a bespoke logging system and outputting via stdout or stderr is forbidden programatically. This makes it possible to set verbosity with the granularity we want (e.g. only verdict, progress information, filter debug information by class)

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 Travis + Sonarcloud. Travis builds Vercors and runs the test suite. The (committed) code is linted by Sonarcloud. 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 all things being equal scala is preferred. The build structure is defined in the scala build tool. We use the sbt-native-packager plugin to package the tool as a .deb and a .tar.gz (compiled). The sbt-buildinfo plugin supplies the tool with run-time access to versioning and build time information.

Project Structure

/

  • build.sbt 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.
  • .travis.yml sets up caching and parallelizes the build. The actual build steps are in .travis/build.sh.

/.travis

/bin

Convenience run scripts that targets the last-compiled classes in the vercors directory. This is the least stable method of running Vercors. If bleeding edge features are not needed, use the release version. If possible, run Vercors imported in an IDE instead. Failing that, the run scripts can be useful.

  • run-class.sh and .classpath: run-class obtains the run-time class path from SBT and caches it in .classpath. A supplied main class + arguments is run from this class path. Other scripts in the directory only select a main class and refer to run-class.

/examples

This directory serves the dual purpose of being an archive of past case studies and competition results, as well as the test suite of VerCors. Files in this directory have a header denoting how they are used in the test suite. Names denoted by "case" or "cases" are collected, where overlapping names are joined together as one test case. Files may occur in more than one "case." "tools" denotes the backend used (silicon by default), "verdict" the expected final result (Pass by default).

  • private: this can be created as a subdirectory and is ignored by git. Contributing examples (however small) that reproduce issues are however appreciated.

/parsers

A sub-project of Vercors that implements the parsing infrastructure of Vercors.

  • build.sbt: runs ANTLR 4, the parser generator, prior to compilation if necessary. Grammar source sets are encoded explicitly in the build file.
  • src/main/antlr/*.g4: root grammars from which parsers are generated. These only glue a language grammar to the specification grammar, though the language grammar itself is also modified somewhat.
  • lib/antlr4/*.g4: non-root grammars, defining languages (such as C and Java), embedded languages (such as OpenMP) and specifications.

/project

An artifact of how SBT works. SBT projects are layered, not in the sense that we have sub-project dependencies, but that you can define meta-projects. This directory defines a meta-project, which means it is available in compiled form in the upper build definition. We just use it to add some plugins to the compiler.

/SplitVerify

This tool is not part of VerCors itself, but interacts with VerCors to cache the verification result of parts of a test case. That means that changing part of a test case only requires re-verifying the changed part. Refer to the readme there for further information.

/util

  • VercorsPVL.tmbundle: textmate bundle, defining PVL as a grammar, enabling syntax highlighting for PVL in some editors.

/src

The sources associated with the top-level SBT project, i.e. the main part of VerCors.

/src/universal/res

Here live the resources of VerCors. Normally they would be in a directory res or so in the root, but we have a custom solution to ensure that they remain regular files, even when packed into a jar by the build tool. Universal refers to the native-packager also being called the "Universal" plugin. "res" is the name of the directory in which the resources end up in .tar.gz deployment.

  • config: Include files ("headers") that are put in the AST at some intermediate stage.
    • config/prelude(_C)?.sil: here the standard axiomatic data types that we need are defined
    • *.jspec: simplification rules that we assume to be true, applied at various stages.
  • deps: Software dependencies that we do not refer to in the project structure, but rather by including the binary.
  • include: Include files ("headers") that are available to front-end files, though currently only C.
  • selftest: Ancient test files that are still accessible via the test suite. Unclear if they still work.

/src/main/scala

Please don't use this directory anymore. Scala sources also compile fine when included in the java directory, so this "mirror" of the package structure only serves to confuse where classes are defined. Only a few rewrite passes are defined here.

/src/main/java

  • col/lang: I believe this is an implementation of some verification constructs, to facilitate compiling PVL to Java.
  • puptol, rise4fun: external tool support, now obsolete.

/src/main/java/vct

  • antlr/parser: Takes ANTLR parse trees and converts them to COL. The classes ending in Parser guide the conversion process. Classes ending in ToCOL do the actual immediate translation. Finally there are a few rewrite passes that solve language-specific problems.
  • boogie: Old (?) prototypes for supporting boogie, dafny and chalice.
  • col/annotate: A single feature rewrite pass, unclear why it's in a different package.
  • col/ast: the AST of COL, divided into expressions (expr), declarations (stmt/decl), statements (stmt/{composite,terminal}) and types (type). Also defines some abstract intermediate node types (generic) and utility classes for traversing the tree in various ways (util).
  • col/print: logic to translate COL into text again for different frontends. Only Java is well-supported, as it's the default diagnostic output.
  • col/rewrite: this is where all rewrite passes are defined. They are under-documented, but the Main class offers a brief explanation for each of them.
  • col/syntax: abstract representation of the syntax of various frontends.
  • demo: unclear why this is in the source tree.
  • error: probably an attempt at better abstracting errors from the backend
  • learn: experiment that counts the different types of nodes in the AST, to attempt to correlate verification time with the presence of particular nodes.
  • logging: barely used; abstracts messages and errors for a particular pass
  • main: entry points for VerCors, as well as some poorly-sorted classes.
    • ApiGen: echoes back a java program immediately after parsing something; purpose unclear.
    • BoogieFOL: another prototype to interface with boogie, a deprecated backend (?)
    • Brain, SMTinter, SMTresult, Translator: attempt by student (?) to interface with z3
    • Main: the true entry point of Vercors.
  • silver: maps COL to Silver, the language used by the viper project.
  • test: the testing framework of Vercors. Collects cases from the examples directory and tests each in an isolated process.
  • util/Configuration.java: contains most command-line options, as well as the logic to determine the location of external tools (z3, silicon, etc.)

/viper

More logic to interface with the viper backend(s), unclear where exactly the cut is with regards to /src/main/java/vct/silver.

/viper/hre

The general utilities project ("Hybrid Runtime Environment"), located here so /viper may depend on it. From here under src/main/java:

  • hre/ast: definitions for the different types of Origin.
  • hre/config: defines different types of command line options (integer, choice, collect...)
  • hre/debug/HeapDump: dumps a class and its fields recursively using reflection. Largely replaced by DebugNode
  • hre/io: inter-process communication.
  • hre/lang/System: defines the logging system. Currently output to stdout and stderr directly is forbidden programatically, so that you're forced to use the logging framework.

IDE Import

This document gives instructions on how to configure a development environment for VerCors, using either Eclipse or Intellij IDEA. Below the instructions there is a list of encountered errors, you might want to check there if you encounter one. The setup for IntelliJ IDEA is considerably easier, so we recommend using that.

Configuring VerCors for Eclipse

First make sure that Eclipse is installed. The installation instructions described below have been tested with Ubuntu 18.04 and Eclipse version 4.11.0 (March 2019) from snap, not apt. The version from the eclipse website should be equivalent. Also make sure that VerCors has been installed according to the instructions given on the main Git page.

Install the Scala IDE plugin for Eclipse. Download- and installation instructions can be found here. After providing the installation/update site in Eclipse, make sure that all the suggested options are selected for installation. After installation has completed, navigate to Help > Install new software > Manage, and go to Scala > Compiler. We have to give scalac more memory to compile VerCors than is available by default, so enter "-J-Xmx2048m" under "Additional command line options" to increase the limit to 2048MB.

Install the eclipse plugin for sbt, instructions for which can be found here. It is recommended that you install it in the global file, and not in the vercors file, as we do not want to add eclipse-specific configuration in the repository. Create a global settings file for SBT (e.g. in ~/.sbt/1.0/global.sbt) and add the setting EclipseKeys.skipParents in ThisBuild := false

Configuring the VerCors modules

  1. Navigate to the vercors subdirectory using a terminal, and run sbt eclipse. This will generate all the eclipse projects necessary to build vercors within eclipse.
  2. In eclipse, go to File > Import and select General > Existing Projects into Workspace. Select the vercors subdirectory, and tick Search for nested projects. If all went well, it should list all the vercors subprojects (vercors, hre, parsers, viper, silicon, etc.). Click finish.
  3. Eclipse will automatically build vercors; wait for it to finish. If eclipse fails to build the projects in this stage, unfortunately the projects are left in a broken state. You should remove all the projects or clear the workspace, and try again.

Running VerCors from Eclipse

To run VerCors from Eclipse, and thereby allow debugging within Eclipse, a Run Configuration needs to be created and used. To create a run configuration, do the following. In the menu, navigate to "Run > Run Configurations...". Select "Java Application" in the left menu and press the "New" button/icon in the toolbar. From here you can assign a name to the new configuration, for example "VerCors". Under "Project" select the "Vercors" project. Under "Main class" select or type vct.main.Main. Under the "Arguments" tab, type ${string_prompt} in the "Program arguments" field, so that every time VerCors is run with this new configuration, a pop-up window will be given in which arguments to VerCors can be specified. Moreover, in the "VM arguments" field, type -Xss16m, which increases the stack size to 16MB for VerCors runs (the default stack size may not be enough). Set the working directory to the root directory of the git repository.

After performing these steps, you should be able to run VerCors from Eclipse via the "Run" option (do not forget selecting the new run configuration). The output of VerCors is then printed in Eclipse console view. To validate the configuration, try for example "--silicon examples/manual/fibonacci.pvl". If you get an error like NoClassDefFoundError: scala/Product, perform the workaround listed under "I got an error!" below.

Configuring VerCors for IntelliJ IDEA

The steps below were testing with Ubuntu 18.04 and Intellij IDEA community edition, version 2019.1.1 retrieved via snap. Also make sure that VerCors has been installed according to the instructions given on the main Git page.

When first installed, go to Configure > Plugins, or when already installed go to File > Settings > Plugins. Install the Scala plugin, and restart the IDE as suggested.

Configuring the project

  1. Go to Open when first installed, File > Open otherwise, and open vercors/build.sbt. Open it as a project as suggested. In the dialog "Import Project from sbt", you should tick "Use sbt shell: for imports" and "for builds"
  2. Wait for the running process to complete, which configures the whole project.
  3. If IntelliJ did not present you with the option "Use sbt shell [] for imports [] for build"; open File > Settings, and tick the two options in Build, Execution, Deployment > Build Tools > sbt.

Running VerCors from IntelliJ IDEA

Go to Run > Edit configurations, and add a Java application with the following settings:

  • Main class: vct.main.Main
  • VM options: -Xss16m (increases the stack size to 16MB)
  • Program arguments: $Prompt$ (asks for parameters every time)
  • Working directory: the root of the git repository
  • Use classpath of module: Vercors

You should now be able to run and debug VerCors from within IntellJ IDEA! The first time the run configuration is used the project will be built in full, so that will take some time.

I encountered an error!

Here is a collection of errors we encountered, with a solution. Is your problem not here? Please file an issue!

  • While eclipse is building the workspace, I get a StackOverflowException. The scala compiler has insufficient memory to compile the project, try increasing the limit at Help > Install New Software > Manage, then Scala > Compiler. Try adding -J-X____m at "Additional command line parameters", substituting ___ with the amount of memory (in MB) you want to try.
  • Silicon is not detected as a project when running sbt eclipse. By default, parent projects (SBT projects that aggregate other projects) are not included by this tool. Remember to add EclipseKeys.skipParents in ThisBuild := false to the global SBT settings file.
  • Only VerCors is detected as a project by eclipse. Remember to tick "Search for nested projects".
  • The run configuration only outputs NoClassDefFoundError: scala/Product. For whatever reason, the scala runtime environment is not included in the run configuration. You should add manual dependencies in the run configuration, at Dependencies > Classpath Entries > Add External JARs. Add scala-library.jar and scala-reflect.jar, which should be present in the sbt configuration directory, ~/.sbt/boot/scala-x.x.x/ or similar. It seems to me that these libraries should be included from the project classpath, so please let me know if I'm misunderstanding!
  • While IntelliJ is building, it encounters import errors in package vct.antlr4.generated. When creating the project from vercors/build.sbt, do not forget to tick "Use sbt shell: for builds", do not tick imports, and untick "allow overriding sbt version". I only encountered this on initial setup of the project and sometimes "accidentally" fixed it, so please let me know if you did set these options, but got this result anyway.