1. Class SimplePar implements a very simple parallel calculation. Given is a class Point, and it resets the first and second element to a given reset value, but it does this in parallel.

Prove correctness of this method:
- first add permisison annotations to show the program is free of data races
- then add functional correctness specifications to show that afterwards, both x and y have been reset to the value reset.

2. Consider class Fibonacci, with a fork-join implementation of the Fibonacci-function.

a. Add sufficient permissions to prove that it is free of data races
b. The file contains a mathematical definition of the fibonnaci function: 

  static int fib(int n)=n<2?1:fib(n-1)+fib(n-2);
  
Add specifications to prove that the result value corresponds to the result of this mathematical function. 

3. Reconsider the class Point. In class LockPar we have two parallel threads that compete to set the reset variable to either the first or the second component of the point.

a. Show that the program is free of data races. Ideally, keep your research invariant as minimal as possible.
b. Why is it not possible to add and verify a postcondition that after resetCompete has finished, reset should be equal to either x or y.
c. An alternative way to show that reset is always equal to either x or y is to add this property to the resource invariant. Do this, and make your program verify again (note, you might have to change which variables are proteced by the resource invariant).

4. Add a class counter to your Fibonacci file with an increase method, such that everytime a new instance of class Fib is created, inc is called on this counter. Let all instances of class Fib use the same instance of class Counter. Make sure that your program is still free of data races. (Hint: remember to add enough specifications that the instance of class Counter is non-null.)

5. [Optional] If you have time left, you might want to start working on Challenge 3a from the VerifyThis 2019 program verification competition. (Hint: if you want to prove functional correctness, you will have to define your own function that sums over sequences.)