Hopefully you have VerCors installed. If not, please find installation instructions here:
https://utwente-fmt.github.io/vercors/TryOnline.html#install

VerCors can reason about Java and OpenCL programs (and also verify some OpenMP pragmas), but it (currently) works best for our own prototype verification language PVL. More information about the PVL syntax is available here:
https://github.com/utwente-fmt/vercors/wiki/PVL-Syntax

VerCors works from the commandline.
Once you have VerCors installed, you can run it to verify a class P.pvl, using the following command:
command
<vercors_installation_directory>/unix/bin/vct --silicon P.pvl

VerCors verifies code always under the assumption that it will be executed in a concurrent setting. Therefore it requires so-called permission annotations, which describe whether a thread has read and/or write access to a variable. In this series of exercises, the permission specifications will be given and you can just assume them. In the next part of the lecture, the intention of permissions will be further explained.

1. We start with a simple warm-up exercise.
Prove that the method toZero sets x to 0.

class C {

  int x;

  context Perm(x, write);
  void toZero() {
     x = 0;
  }
}

2. Next, prove that method allZero sets all elements in the array a to 0.
Do this in 2 steps:
- first add a loop invariant such that memory safety is proven
- add a postcondition that all elements are 0, and prove functional correctness

class C {

  invariant (\forall* int j; 0 <= j && j < a.length; Perm(a[j], write));
  void allZero(int [] a) {
     for (int i = 0; i < a.length; i++) {
       a[i] = 0;
     }
  }

}


3. Prove correctness of this linear search algorithm. Again first
prove memory safety, then add specifications to prove functional
correctness (i.e. the method only returns -1 if the element does not
occur, if it returns a value that is not -1, then this is the index of
element x).

class LinearSearch {

  invariant (\forall* int j; 0 <= j && j < a.length; Perm(a[j], write));
  int search (int [] a, int x) {
    int index = -1;
    for (int i = 0; i < a.length; i++) {
      if (a[i] == x) {
        index = i;
      }
    }
    return index;
  }
  
}

4. [Optional]
Prove correctness of the binary search algorithm. Some comments have
ben left to indicate the functional correctness properties you would
have to specfiy.