斐波那契数列

输入一个整数n，返回斐波那契数列第n项的值。

斐波那契数列的第一、二项是1，1，后面的项是其前两项的加和，容易写出一个递归的式子。

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

注意，斐波那契数列的项显然是从1开始的整数，为了规范程序的正确性，需要加入前置条件requires，限定的布尔表达式为n > 0。

由于返回值是一个整数，我们可以用一条简洁的式子表示斐波那契数列的返回值。注意，由于存在递归项Fibonacci(n - 2)，Fibonacci(n - 1)，我们需要再加上decreases n表示n是逐次减小的(但是不会减为0)，Dafny在执行递归时每次都会检测该条件以保证程序的正确性。