jbranchaud

/*
 * The ComputeFib method above is more complicated than necessary. Write
 * a simpler program by not introducing a as the Fibonacci number that
 * precedes b, but instead introducing a variable c that succeeds b.
 * Verify your program is correct according to the mathematical definition
 * of Fibonacci.
 */
function fib(n: nat): nat
{
   if n == 0 then 0 else

jbranchaud

/*
 * With the original loop invariant, change the loop guard from i < n
 * to i != n. Do the loop and the assertion after the loop still verify?
 * Why or why not?
 * It still verifies because the new loop condition doesn't impact the
 * correctness of the assertion.
 */
method m(n: nat)
{
   var i: int := 0;

jbranchaud

/*
 * Change the loop invariant to 0 <= i <= n+2. Does the loop still verify?
 * Does the assertion i == n after the loop still verify?
 * It no longer verifies because the invariant is no longer sufficient for
 * proving the assertion.
 */
method m(n: nat)
{
   var i: int := 0;
   while (i < n)

jbranchaud

/*
 * Now that we have an abs function, change the postcondition of method
 * Abs to make use of abs. After confirming the method still verifies,
 * change the body of Abs to also use abs. (After doing this, you will
 * realize there is not much point in having a method that does exactly
 * the same thing as a function method.)
 */
function method abs(x: int): int
{
   if x < 0 then -x else x

jbranchaud

/*
 * Change your test method from Exercise 4 to capture the value
 * of max to a variable, and then do the checks from Exercise 4
 * using the variable. Dafny will reject this program because you
 * are calling max from real code. Fix this problem using a
 * function method.
 */
function method max(a: int, b: int): int 
{
   if a > b then a else b

jbranchaud

/*
 * Write a function max that returns the larger of two given
 * integer parameters. Write a test method using an assert that
 * checks that your function is correct.
 */
function max(a: int, b: int): int 
{
   if a > b then a else b
}
method Testing() {

jbranchaud

/*
 * Keeping the postconditions of Abs the same as above, change
 * the body of Abs to just y := x + 2. What precondition do you
 * need to annotate the method with in order for the verification
 * to go through? What precondition doe you need if the body is
 * y := x + 1? What does that precondition say about when you can
 * call the method?
 */
method Abs(x: int) returns (y: int)
   requires x == -1;

jbranchaud

/*
 * Using a precondition, change Abs to say it can only be
 * called on negative values. Simplify the body of Abs into
 * just one return statement and make sure the method still
 * verifies.
 */
method Abs(x: int) returns (y: int)
   requires 0 > x;
   ensures 0 <= y;
   ensures 0 <= x ==> x == y;

jbranchaud

/*
 * Write a test method that calls your Max method from
 * Exercise 0 and then asserts something about the result.
 */
method Max(a: int, b:int) returns (c: int)
ensures c >= a && c >= b;
ensures a > b ==> c == a;
ensures a <= b ==> c == b;
{
  if (a > b) {

jbranchaud

/*
 * Write a method Max that takes two integer parameters and returns
 * their maximum. Add appropriate annotations and make sure  your code
 * verifies.
 */
method Max(a: int, b:int) returns (c: int)
  ensures c >= a && c >= b;
{
  if (a > b) {
    return a;