Specification Syntax Auxiliary Annotations & Ghost Code

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

Loop Invariants

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

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

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

[!Warning] Without further instruction, 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. VerCors can check loop termination by adding a decreases clause, more on that in the section on Termination.

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

In PVL and C a loop invariant may also be attached to a label such that loops formed using gotos can be verified.

Assumptions and Assertions

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

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

[!Note] VerCors would be able to verify this example even without the assertion, but this demonstrates how to use assert.

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

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

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

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

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

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

For assert, VerCors supports the following alternative syntax:

⊢ expr;

Ghost Code

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

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

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

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

Here is an example for ghost code inside a method:

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

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

Ghost Methods and Functions

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

/*@
ghost
requires x > 0;
ensures \result == (cond ? x+y : x);
static int cond_add(boolean 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). We then use this ghost method in the body of some_method (but only inside annotations!).

[!Note] The precondition is not wrapped in the special comment //@, like the precondition of some_method is, because the entire ghost method already is inside a special comment /*@.

Functions and Pure Methods

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

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

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

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

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

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

Abstract Methods and Functions

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

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

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

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

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

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

Inline Functions

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

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

[!Note] The inline keyword is also used for inline predicates (see section Predicates), which are a similar concept.

Ghost Parameters and Results

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

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

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

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