Background

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

Software Verification

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

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

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

As an example, consider the following code:

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

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

Separation Logic

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