Proving Program Correctness in Dafny

The goal of this assignment is for you to prove correctness of two simple programs using Dafny. Submit your solutions in the form of Dafny source code into the dafny folder of our github repo. As usual, create a subfolder there based on your github username. The assignment is due on Dec 10.

1. Write a method Min that takes 3 integer parameters and returns their smallest absolute value. Add appropriate postconditions and make sure your code verifies. As we learned in class, there are many postconditions that you could write and prove, some of which are weaker and some are stronger. For the purpose of this assignment, your postconditions should ensure that the returned value is precisely the smallest absolute value of the 3 inputs. Your procedure should have no preconditions.

2. Write loop invariants needed to prove this procedure (i.e., its postcondition) correct. Do not change anything else, but just write loop invariants.

method Multiply2(n:int) returns (r:int)
 requires 0 <= n;
 ensures r == 2*n;
{
 r := 0;
 var i:int := 0;
 while (i < n)
 {
   r := r + 2;
   i := i + 1;
 }
}