Termination

By default, VerCors focuses on partial correctness: if a method or function returns, then its postcondition must hold. To prove total correctness, you also need to prove termination.

You can ask VerCors to check termination with a decreases clause. Intuitively, a decreases measure must:

1. Strictly decrease on every recursive call or loop iteration.
2. Be bounded, so it cannot decrease forever.

The decreases measure must be either:

1. A single integer expression, for example decreases n;
2. A tuple of integer expressions, for example decreases n, m;

Tuples are compared lexicographically: first the first component must decrease; if that stays equal, then a later component must decrease.

Decreases tuples

Simple tuple example

This verifies with a lexicographic measure.

requires n >= 0;
requires m >= 0;
decreases n, m;
pure int count_down_2d(int n, int m) =
  n == 0 && m == 0 ?
    0 :
    (m > 0 ? count_down_2d(n, m - 1) : count_down_2d(n - 1, 2));

Why tuples are sometimes needed: mutually recursive functions

In this example, the first call keeps n unchanged (f(n) to g(n)), so a single measure decreases n; is not enough. The second tuple component distinguishes the two states and makes the proof go through.

requires n >= 0;
decreases n, 1;
pure int f(int n) =
  n == 0 ?
    0 :
    g(n);

requires n >= 0;
decreases n, 0;
pure int g(int n) =
  n == 0 ?
    0 :
    f(n - 1);

This is a mutually recursive (co-recursive style) pattern where the tuple is essential.

Recursive functions

Example that verifies

The measure n decreases (n - 1) and is bounded by the precondition n >= 1.

  requires n >= 1;
  decreases n;
pure int triangle_number(int n) =
  n > 1 ?
  n + triangle_number(n - 1) :
  1;

Example that fails: not decreasing

Here the recursive call uses n + 1, so the measure does not decrease.

  requires n >= 1;
  decreases n;
pure int triangle_number(int n) =
  n > 1 ?
  n + triangle_number(n + 1) :
  1;

Example that fails: not bounded

Even though n - 1 is syntactically smaller, without a guard/base case and lower bound proof, termination cannot be established.

  decreases n;
pure int triangle_number(int n) = n + triangle_number(n - 1);

Loops

It is checked if a loop iteration is terminating, by adding a decreases clause to the loop contract. However, it is not checked by default if any statements are also decreasing, such as function calls. Only if decreases is added to a method or function contract, each statement (and also loops) is checked for termination.

Example that fails: no decreasing argument for the loop

  //@ decreases;
int f() {
  //@ decreases;
  while (true) {
  }
  return 5;
}

This shape is expected to fail with loopDecreasesFailed.

Example that fails: loop does not terminate

//@ decreases;
int f() {
  while (true) {}
  return 5;
}

This shape is expected to fail with loopTerminationFailed.

Known limitation

At the moment, termination of pure functions is not fully checked when those functions are called from non-pure methods. This is known work to do.

pure int y() = y();

  decreases;
int x() {
  return y();
}

This should fail since y actually does not terminate, but currently does not.