1. Adapt the list predicate (in list.pvl) such that it not only recognizes a list
structure, but also checks that the contents of the list is equal to a particular
sequence.

2. Given a class Tree (in tree.pvl) for binary trees, define a tree predicate that checks whether we
have wellformed tree.

3. Consider the classical swap-function, which swap the contents of
two variables (in swap.pvl).

class Swap {

  int x;
  int y;

  void swap() {
    int z = x;
    x = y;
    y = z;
  }
}

Use ghost variables to specify its swapping behaviour. In addition,
add a ghost variable to return the maximum of the two variables.

4. If you did not finish functional correctness of your kernel
encoding (exercise 3.2), do it now, using what you learned about ghost
variables.

5. In the lecture, we saw a verification of the classical Owicki Gries
example using futures (in file owicikgries.pvl). To check this
example:
- if VerCors is run with the --check-defined flag, it checks that the model is correct;
- if VerCors is run with the --check-history flag, it checks that the
program correctly implements the model

Adapt this example, such that one thread adds 4, and the other thread multiplies by 4.

6. Use Futures to give a functional specification for LockPar. Note:
rewrite the LockPar program in a way that is similar to the
OwickiGries example (exercise 3, series 2).