Does the Linked List Contain Zero? / 判断单链表中是否有零

English

Given the head pointer p of a singly linked list, prove that the supplied function sll_has_zero(p) returns 1 if any node's data is 0, and returns 0 otherwise. The function must preserve every node's value and link.

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.

The implementation scans from the head and returns 1 immediately when it finds a zero. It returns 0 when it reaches the end without finding one. The empty list (p == NULL) returns 0 without reading a node.

The supplied problem.h defines sll using sllseg and supplies the node structure and list membership model required by the contract.

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 ghost list input records the original node values. MEM 0i input expresses membership of zero. The postcondition restricts the result to 0 or 1: returning 1 requires that membership be true, and returning 0 requires that it be false. The postcondition also restores sll at the original head pointer, including when the function returns early.

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_has_zero(p) 在链表中存在节点值为 0 时返回 1，否则返回 0。函数必须保持所有节点值和链接结构不变。

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

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

• 链表长度满足 0 <= length <= 100000。
• 对所有节点值 x，有 -100000 <= x <= 100000。

给定实现从表头开始扫描，遇到零时立即返回 1；如果扫描到末尾仍未找到零，则返回 0。空链表（p == NULL）返回 0，不会读取任何节点。

给定的 problem.h 使用 sllseg 定义 sll，并提供规约所需的节点结构及列表成员关系模型。

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

幽灵列表 input 记录原始节点值。MEM 0i input 表示零属于该列表。后置条件将返回值限制为 0 或 1：返回 1 时要求该成员关系为真，返回 0 时要求其为假。同时，后置条件要求在原始头指针处恢复 sll 断言；提前返回时也必须满足这一要求。

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

Examples / 示例