General guideline:

You may be asked to implement and check some programs in Dafny, as well as constructing proofs by hand.

Whenever you are asked to construct a proof by hand you should go like this: first state an expression for the weakest precondition of the program. Then, proceed to calculate the weakest precondition of the program by applying the appropriate inference rules. If required, show that it follows from the preconditions. Each main step of the proof should correspond to applying one of the Weakest Precondition calculus rules. State which rule you apply and also the result, which may be one or several new statements or logical formula.

• If the rule application resulted in a new statement, simply continue with the proof in the same way.
• If it resulted in a logical formula, explain why the formula is valid.
• If it resulted in several new subgoals or conjuncts, you may pick one of them and continue proving that one. When the first subgoal has been proved true, don't forget that you have to go back and prove the other ones, too. Number the intermediate results if there is any danger of confusion.
• If you used the loop invariant rule, clearly state which formula you are using as invariant.

The proofs can be rather lengthy. You can copy and paste to avoid excessive typing. When you are dealing with large formulas in the pre or postcondition you can introduce names to abbreviate them. Just keep in mind that when you are applying an update to a formula you have to unfold the abbreviation first before you apply the update.

Whenever you are asked to implement something using Dafny you should:

1. Write a .dfy file corresponding to the program.
2. Make sure Dafny can prove your program correct according to specification.

Question 1: Pure methods should not be methods!

Let's start with a warm up question:
Below is the familiar Dafny program for computing an absolute value of a number. However, instead of a function, the author made a design mistake and decided to write it as a method!

method Abs(x : int) returns (y : int) 
  // return value doesn't deviate from intended value
  ensures 0 <= x ==> y == x; 
  ensures x < 0 ==> y == -x;
   // return value is greater or equal to zero
  ensures 0 <= y; 
{
  if (x < 0)
   { y := -x; }
  else
   { y := x; }
}

1. Write down the initial weakest precondition of the program (based on its postconditions only)
2. Construct the correctness proof by hand using wp(S, R)
3. [Open question] Why is this method considered as a design mistake?

Question 2: Missing specs or wrong program?

Below is a small Dafny program:
Dafny will NOT be able to prove the above program correct (try it!), as its specification is incomplete.

method Q2(x : int, y : int) returns (big : int, small : int) 
  ensures big > small;
{
  if (x > y)
   {big, small := x, y;}
  else
   {big, small := y, x;}
}

Your task is to figure out exactly why the proof fails, and from there derive a verfiable version of this program.

1. Describe in words why is the program not verifiable?
2. With only description it can be difficult to convince others that the mistake is really there! Your second task is to use wp(S, R) to show the postcondition really fails to hold according to weakest precondition calculus

1. Without changing the postcondition nor the method body, try to fix
   this program so that it becomes verifiable
2. Without adding new precondition nor changing the method body, try to fix
   this program so that it becomes verifiable
3. [Bonus: think outside the box] Without changing its specification, can this program be verifiable?

(If you managed to answer the bonus question above, can you try to go back to original question and refine the specifications so the method is more precisely described by its specs?)

Question 3: Correct program AND missing specs!

method Q3(n0 : int, m0 : int) returns (res : int)
  
{
  var n, m : int;
  res := 0;
  if (n0 >= 0) 
       {n,m := n0, m0;} 
  else 
       {n,m := -n0, -m0;}
  while (0 < n) 
  { 
    res := res + m; 
    n := n - 1; 
  }
}

1. Why can't we use the inputs directly? (n0, m0)
2. What IS the purpose of method? In other words, what should the specification (postcondition(s)) of the program be? (You can of course always give a silly specification for which the program is correct, but this will not be considered a correct specification.)
3. Prove by hand that the program is correct with respect to your specification. Follow the steps in the "checklist" for proving loops correct from the lecture notes. See also Chapter 11 of [Gries].

[Hint] If you successfully figure out the method's purpose, try to include additional specification so that you can demonstrate the correctness of this program against standard library function.

Question 4: Factorial!

The factorial (written often written as n! in mathematics) computes the product of all numbers from 1 up to n, given positive n. (for example: 3! == 1 * 2 * 3 == 6.)

The following Dafny program calculates the factorial of a number.

method ComputeFact(n : nat) returns (res : nat)
  requires n > 0;
  ensures res == fact(n);
 {
  res := 1;
  var i := 2;
  while (i <= n) 
  {
    res := res * i;
    i := i + 1;
  }
 }

  fact(1) = 1
  fact(m) = m * fact(m - 1)

1. Complete the specification so that Dafny is able to prove ComputeFact correct.
2. Prove correctness of the loop using the checklist for proving loops correct from the lecture notes. See also Chapter 11 of [Gries].