Verifying Fibonacci with Microsoft's Dafny

dafny-fibonacci

function method Fibonacci(n: int): int
  requires n >= 0;
  decreases n;
{
  if n < 2 then n else Fibonacci(n-2) + Fibonacci(n-1)
}

method Testing() {
  assert 0 == Fibonacci(0);
  assert 1 == Fibonacci(1);
  assert 1 == Fibonacci(2);
  assert 2 == Fibonacci(3);
  assert 3 == Fibonacci(4);
  assert 5 == Fibonacci(5);
  assert 8 == Fibonacci(6);
}