File: fib.dfy

package info (click to toggle)
cloc 2.06-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 8,064 kB
  • sloc: perl: 30,146; cpp: 1,219; python: 623; ansic: 334; asm: 267; makefile: 244; sh: 186; sql: 144; java: 136; ruby: 111; cs: 104; pascal: 52; lisp: 50; haskell: 35; f90: 35; cobol: 35; objc: 25; php: 22; javascript: 15; fortran: 9; ml: 8; xml: 7; tcl: 2
file content (27 lines) | stat: -rw-r--r-- 598 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
 
/*
https://dafny.org/latest/OnlineTutorial/guide
*/
function fib(n: nat): nat
{
  if n == 0 then 0
  else if n == 1 then 1
  else fib(n - 1) + fib(n - 2)
}
method ComputeFib(n: nat) returns (b: nat)
  ensures b == fib(n)  // Do not change this postcondition
{
  // Change the method body to instead use c as described.
  // You will need to change both the initialization and the loop.
  if n == 0 { return 0; }
  var i: int := 1;
  var a := 0;
  b := 1;
  while i < n
    invariant 0 < i <= n
    invariant a == fib(i - 1)
    invariant b == fib(i)
  {
    a, b := b, a + b;
    i := i + 1;
  }
}