Ideally you do the examples both on paper and in Dafny

1
Prove the correctness of the following silly program.

method M (x0 : int) returns (x : int)
ensures (x0 < 3 ==> x == 1) && (x0 >= 3 ==> x < x0);
{
  x := x0 - 3;
  if (x < 0) {
    x := 1;
  } else {
    if (true) {
      x := x + 1;
    } else {
      x := 10;
    }
  }
}

2
Given the specification:

 ensures: (m = a || m = b || m = c) && (m <= a && m <= b && m <= c) 

3
Prove the partial correctness of:

method M3(x : int, y : int) returns (q : int, r : int)
requires x >= 0 && y > 0;
ensures q * y + r == x && r >= 0 && r < y; 
  q := 0;
  r := x;
  while (r >= y) {
    r = r - y;
    q = q + 1;
  }

4
Find the missing invariant which allows Dafny to prove correctness of the following program. If you have time, also prove the partial correctness on paper:

method M4 (n : int) returns (sq1 : int, sq2 : int)
requires n >= 0 && n * n >= n;
ensures  (sq1 == sq2 && sq1 * sq1 == n) ||
         (sq1 + 1 == sq2 && sq1 * sq1 < n && sq2 * sq2 >= n);
{
  sq1 := 0;
  sq2 := n;
  var mid := 0;
  while (sq2 - sq1 > 1) 
  {
    mid := (sq1 + sq2) / 2;
    if (mid * mid == n) {
      sq1 := mid;
      sq2 := mid;
    } else {
      if (mid * mid < n) {
        sq1 := mid;
      } else {
        sq2 := mid;
      }
    }
  }
  
}

5
Provide Dafny with the missing annotations required to prove the total correctness of the program below. If you want, also prove it correct on paper.

method M5(a0 : int, b0 : int) returns (c : int)
requires a0 >= 0 && b0 >= 0;
ensures c == a0+b0;
{
  c := 0;  
  var a, b, g, m := a0, b0, 1, 0;
  while (a > 0 || b > 0) 

  {
    m := m + a % 2 + b % 2;
    a := a / 2;
    b := b / 2;
    c := c + g * (m % 2);
    g := 2 * g;
    m := m / 2;
  }
  c := c + g * m;
}