Complete the exercises below, which involve writing Dafny code, or
adding annotaitons to get existing code to verify. Submit your final
version as a text file. I should be able to paste it into the Dafny
web system and see that it verifies.

Note that you should go through the Dafny tutorial before trying this;
it will be a lot easier if you do!

1. Computes the Fibonacci function. The first definition is the
specification, the second is the code to compute it
(imperatively). Extend the second part with annotations so that it
verifies. (Tutorial exercise 10)

function Fib(n: nat): nat
{
  if n < 2 then n else Fib(n - 1) + Fib(n-2)
}

method Compute_Fib(n: nat) returns (x: nat)
ensures x == Fib(n);
{
  var i := 0;
  x := 0;
  var y := 1;
  while (i < n) {
    x, y := y, x + y;
    i := i + 1;
  }
}

2. Fill in the following definition for finding the maximum element of
an array, and prove that it does so. (Tutorial exercise 12)

method FindMax(a: array<int>) returns (i: int)
   // Annotate this method with pre- and postconditions
   // that ensure it behaves as described.
{
   // Fill in the body that calculates the INDEX of the maximum.
}

3. Write out the predicate that defines when the arrray a is sorted
(tutorial exercise 13).

predicate sorted(a: array<int>)
   requires a != null
   reads a
{
   // Fill in a new body here.
}


4. Get the following method to verify (only adding invariants, etc.,
without changing any code).

method Cube(N: int) returns (c: int)
  requires 0 <= N;
  ensures c == N*N*N;
{
  c := 0;
  var n := 0;
  var k := 1;
  var m := 6;
  while (n < N) {
    c := c + k;
    k := k + m;
    m := m + 6;
    n := n + 1;
  }
}