The Tenth Catalan Number / 第十个卡特兰数

English

The Catalan sequence is defined by

C(0) = 1
C(t) = C(t - 1) * (4 * t - 2) / (t + 1)  for t >= 1

Here / denotes integer division. The supplied function

int catalan_10(void);

computes C(10) = 16796 by expanding this recurrence into ten calculations, without loops or recursion. The requested index is 10, not the tenth term counted from C(0). The function has no parameters and does not access external memory. All intermediate products fit in a signed 32-bit int, and every divisor is positive.

Verification Task

Verify that the function returns C(10). Its C* contract requires emp and ensures fact(__return == catalan 10i), preserving the empty owned heap. Complete starter.c with proof code establishing that the computed value 16796 equals catalan 10i, as defined in problem.h. Verification also checks the safety of the executable integer arithmetic.

The header supplies catalan_nat_def, the natural-indexed recurrence with mathematical integer values, and catalan_def, its extension to integer indices. Negative indices map to index zero, so their value is 1. Mathematical integer operations do not overflow. The literal 10i is a mathematical integer; natural-number indices use literals such as 10, and &(n + 1) converts a natural number to a mathematical integer.

You may add proof-only helper declarations and proof blocks in starter.c. Do not change the executable C implementation, its contract, or the supplied header. 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.

中文

卡特兰数列定义如下：

C(0) = 1
C(t) = C(t - 1) * (4 * t - 2) / (t + 1)  对所有 t >= 1

其中 / 表示整数除法。给定函数

int catalan_10(void);

将递推式展开为十次计算，求出 C(10) = 16796，不使用循环或递归。这里要求的是下标为 10 的值，而不是从 C(0) 开始计数的第十项。函数没有参数，也不访问外部内存。所有中间乘积均在 32 位有符号 int 的范围内，且每个除数均为正数。

验证任务

请验证该函数返回 C(10)。其 C* 契约的前置条件为 emp，后置条件为 fact(__return == catalan 10i)，保持所拥有的堆为空。请在 starter.c 中补全证明，说明计算得到的值 16796 等于 problem.h 中定义的 catalan 10i。验证还会检查可执行程序中整数运算的安全性。

头文件提供 catalan_nat_def 和 catalan_def：前者定义以自然数为下标、以数学整数为值的递推关系，后者将其扩展到整数下标。负下标映射到下标零，因此对应的值为 1。数学整数运算不会溢出。字面量 10i 表示数学整数；自然数下标使用 10 这样的字面量，&(n + 1) 将自然数转换为数学整数。

你可以在 starter.c 中添加仅用于证明的辅助声明和证明块。不得修改可执行 C 实现、函数契约或给定头文件。修改实现或规约将被判定为失败，并消耗一次提交机会。提交完成后的 starter.c 即可，不需要编写 main 函数或标准输入输出代码。

Examples / 示例