The Tenth Fibonacci Number / 第十个斐波那契数

English

The Fibonacci sequence is defined by

F(0) = 0
F(1) = 1
F(t + 2) = F(t + 1) + F(t)  for t >= 0

The supplied C function fibonacci_10(void) computes the tenth Fibonacci number using a sequence of additions. It has no parameters, loops, or recursive calls, and does not access external memory.

Verify that the function returns F(10). Complete the proof that the computed value, 55, is equal to fib 10i as defined in the supplied problem.h.

Verification Task

The function already has its complete C* specification: it requires emp and ensures fact(__return == fib 10i). Add proof code to starter.c to discharge the remaining verification condition. No loop invariants or additional function contracts are needed.

The header supplies fibonacci_nat_def, the natural-indexed Fibonacci recurrence with mathematical integer values, and fib_def, its extension to integer indices. Negative indices map to zero. The literal 10i is a mathematical integer; natural-number indices in fibonacci_nat_def use literals such as 10.

Do not change the C implementation, its specification, or the mathematical definitions in problem.h. Changing the implementation or specification is rejected by the judge and consumes an attempt. Submit the completed starter.c. No main function or standard input/output handling is needed.

中文

斐波那契数列定义如下：

F(0) = 0
F(1) = 1
F(t + 2) = F(t + 1) + F(t)  对所有 t >= 0

给定 C 函数 fibonacci_10(void) 通过一系列加法计算第十个斐波那契数。该函数没有参数、循环或递归调用，也不访问外部内存。

请验证该函数返回 F(10)。你需要补全证明，说明计算得到的值 55 等于给定 problem.h 中定义的 fib 10i。

验证任务

函数已经具有完整的 C* 规约：前置条件为 emp，后置条件为 fact(__return == fib 10i)。请在 starter.c 中添加证明代码，完成剩余的验证条件。不需要添加循环不变式或额外的函数契约。

头文件提供 fibonacci_nat_def 和 fib_def：前者定义以自然数为下标、以数学整数为值的斐波那契递推关系，后者将其扩展到整数下标。负下标对应的值为零。字面量 10i 表示数学整数；fibonacci_nat_def 中的自然数下标使用 10 这样的字面量。

不得修改 C 实现、函数规约或 problem.h 中的数学定义。修改实现或规约将被判定为失败，并消耗一次提交机会。提交完成后的 starter.c 即可，不需要编写 main 函数或标准输入输出代码。

Examples / 示例