Skip to content

Instantly share code, notes, and snippets.

@nkavanagh

nkavanagh/fib.dfy

Last active August 29, 2015 14:01
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save nkavanagh/bc0f718a34e70bee6387 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save nkavanagh/bc0f718a34e70bee6387 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. nkavanagh revised this gist May 28, 2014. 1 changed file with 15 additions and 0 deletions.
    15 changes: 15 additions & 0 deletions fib.dfy
    View file
    Original file line number Diff line number Diff line change
    @@ -20,4 +20,19 @@ method testFib()
    assert 3 == fib(4);
    assert 55 == fib(10);
    assert 987 == fib(16);
    }

    method ifib(n: int) returns (f2: int) ensures f2 == fib(n);
    {
    var i: int := 0;
    var f1: int := 0;
    f2 := 0;

    while (i < n)
    invariant 0 <= i <= n;
    {
    f1 := f2;
    f2 := f1+f2;
    i := i + 1;
    }
    }
  2. nkavanagh created this gist May 28, 2014.
    23 changes: 23 additions & 0 deletions fib.dfy
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,23 @@
    function method fibn(n: int, f1: int, f2: int): int
    requires n >= 0;
    decreases n;
    {
    if n > 1 then fibn(n-1, f2, f1+f2) else f2
    }

    function method fib(n: int): int
    requires n >= 0;
    decreases n;
    {
    if n == 0 then n else fibn(n, 0, 1)
    }

    method testFib()
    {
    assert 0 == fib(0);
    assert 1 == fib(1);
    assert 2 == fib(3);
    assert 3 == fib(4);
    assert 55 == fib(10);
    assert 987 == fib(16);
    }