Singly Linked List Sum / 单链表求和

English

Given the head pointer p of a singly linked list, prove that the supplied function sll_sum(p) returns the sum of all node values and preserves the list's values and links. Each node has this layout:

struct list {
  int data;
  struct list *next;
};

The input is a finite, acyclic, null-terminated list satisfying:

• Its length is between 0 and 100000, inclusive.
• Every node value is between -100000 and 100000, inclusive.
• For every prefix length k between 0 and the list length, the sum of the first k node values is between -2147483648 and 2147483647, inclusive.

The function starts with a sum of zero, adds p->data, and advances to p->next until the pointer is null. The empty list (p == NULL) returns 0. All specification sums use mathematical integers. The prefix bounds ensure that each addition fits in a signed 32-bit int; a bound on the final sum alone would not be sufficient.

The supplied problem.h contains the node declaration and the mathematical list model used by the contract:

The header initializes these definitions automatically. The ghost list input records the original values; the postcondition requires the result to equal list_sum input and restores sll at the original head pointer.

Define any auxiliary predicates and prove the lemmas needed for your invariants in starter.c; the header supplies only the contract model and its dependencies.

The implementation and contract are fixed. Add loop invariants and proof code only inside starter.c; changing the implementation or specification is rejected by the judge and consumes an attempt. Submit the completed starter.c. No main function, input/output code, or list allocation is needed.

中文

给定单链表头指针 p，请证明给定函数 sll_sum(p) 返回所有节点值之和，并保持链表节点值和链接结构不变。节点结构如下：

struct list {
  int data;
  struct list *next;
};

输入是有限、无环、以空指针结尾的单链表，并满足：

• 链表长度满足 0 <= length <= 100000。
• 对所有节点值 x，有 -100000 <= x <= 100000。
• 对所有 0 <= k <= length，从表头开始的前 k 个节点值之和满足 -2147483648 <= prefix_sum(k) <= 2147483647。

函数从 0 开始累加，每次加上 p->data，再沿 p->next 前进，直到指针为空。空链表（p == NULL）返回 0。规约中的求和使用数学整数；前缀和约束保证每次加法均在 32 位有符号 int 的范围内。仅保证最终总和不溢出是不够的。

给定的 problem.h 已包含节点定义以及规约使用的链表模型：

头文件会自动初始化这些固定定义。幽灵列表 input 记录原始节点值；后置条件要求返回值等于 list_sum input，并在原始头指针处恢复 sll 断言。

请在 starter.c 中自行定义不变式所需的辅助谓词并证明所需引理；头文件仅提供规约模型及其依赖定义。

实现和契约均为固定内容。你只能在 starter.c 中添加循环不变式和证明代码；修改实现或规约将被判定为失败，并消耗一次提交机会。提交完成后的 starter.c 即可，不需要编写 main 函数、输入输出代码或链表分配代码。

Examples / 示例