RiSE4fun samples for Dafny

Hello

method Main() { print "hello, Dafny\n"; assert 10 < 2; }

Fibonacci

function Fibonacci(n: int): int decreases n; { if n < 2 then n else Fibonacci(n+2) + Fibonacci(n+1) }

CountToN

class Example { method M(n: int) { // count up to 'n'; will this program terminate? var i := 0; while (i < n) { i := i + 1; } } }

Ackermann

function Ackermann(m: int, n: int): int // The following lexicographic pair allows Dafny to prove termination. // Still, you may not want to sit around and wait for a call to Ackermann // to terminate. decreases m, n; { if m <= 0 then n + 1 else if n <= 0 then Ackermann(m - 1, 1) else Ackermann(m - 1, Ackermann(m, n - 1)) }

Mul

// Multiply two numbers by addition to the next smaller multiple, // the smaller multiple being computed recursively. // Can you find the error below? method Mul(x: int, y: int) returns (r: int) requires 0 <= x && 0 <= y; ensures r == x*y; decreases x; { if (x == 0) { r := 0; } else { var m := Mul(x-1, y); r := m + x; } }

zb

function method isLeapYear(y: int): bool { (y % 4 == 0) && ((y % 100 != 0) || (y % 400 == 0)) } // Does this method terminate? method WhichYear_InfiniteLoop(d: int) returns (year: int) { var days := d ; year := 1980 ; while (days > 365) { if (isLeapYear(year)) { if (days > 366) { days := days - 366 ; year := year + 1 ; } } else { days := days - 365 ; year := year + 1 ; } } }

Cube

// This method is supposed to compute out-parameter 'c' to // be the cube of 'N'. Can you correct the program? method Cube(N: int) returns (c: int) requires 0 <= N; ensures c == N*N*N; { c := 0; var n := 0; var k := 0; var m := 0; while (n < N) invariant n <= N; invariant c == n*n*n; invariant k == 3*n*n + 3*n + 1; invariant m == 6*n + 6; { c := c + k; k := k + m; m := m + 6; n := n + 1; } }

z

function method isLeapYear(y: int): bool { (y % 4 == 0) && ((y % 100 != 0) || (y % 400 == 0)) } // Does this method terminate? method WhichYear(d: int) returns (year: int) { var days := d ; year := 1980 ; while (days > 365) { if (isLeapYear(year)) { if (days > 366) { days := days - 366 ; year := year + 1 ; } else { break ; } } else { days := days - 365 ; year := year + 1 ; } } }

CountToAndReturnN

// This example uses specifications. There is a postcondition // (keyword 'ensures') that says the method is intended to set // the out-parameter 'r' to 'n'. Other possible specifications // are preconditions (keyword 'requires') and loop invariants // (keyword 'invariant', place just before the open-curly brace // of the loop body). // Can you make the program verify? method M(n: int) returns (r: int) ensures r == n; { var i := 0; while (i < n) { i := i + 1; } r := i; }

Problem1-SumMax

// This method computes the sum and max of a given array of // integers. The method's postcondition only promises that // 'sum' will be no greater than 'max'. Can you write a // different method body that also achieves this postcondition? // Hint: Your program does not have to compute the sum and // max of the array, despite the suggestive names of the // out-parameters. method M(N: int, a: array) returns (sum: int, max: int) requires 0 <= N && a != null && a.Length == N; ensures sum <= N * max; { sum := 0; max := 0; var i := 0; while (i < N) invariant i <= N && sum <= i * max; { if (max < a[i]) { max := a[i]; } sum := sum + a[i]; i := i + 1; } }

Add

// The following program is intended to compute // twice 'x' plus 'y' into the out-parameter 'r', // given that 'x' and 'y' are non-negative integers. // The precondition (keyword 'requires') states the // non-negative assumption and the postcondition // (keyword 'ensures') states the intended result. // The loop invariant (keyword 'invariant') states // a condition that is intended to hold at the top // of every loop iteration, just before the loop // guard is evaluated. // Can you correct the program and get Dafny to // verify it? method Add(x: int, y: int) returns (r: int) requires 0 <= x && 0 <= y; ensures r == 2*x + y; { r := x; var n := y; while (n != 0) invariant r == x+y-n && 0 <= n; { r := r + 1; n := n - 1; } }