删除循环双向链表
从表头开始逐一删除循环双向链表中所有的节点。（验证时间约 15sec）
[Back to Index]
验证特点：循环双向链表，内置谓词 \c_dlist，逻辑变量，幽灵变量
标注说明：函数前条件：利用逻辑变量记录函数入口处指向循环双向链表的实参指针；
函数后条件：逻辑变量或为悬空指针（=表已删空）；或为空指针（=原表为空）。
程序样例 
从表头开始逐一删除循环双向链表中所有的节点。（验证时间约 15sec）
验证特点：循环双向链表，内置谓词 \c_dlist，逻辑变量，幽灵变量
标注说明：函数前条件：利用逻辑变量记录函数入口处指向循环双向链表的实参指针；
函数后条件：逻辑变量或为悬空指针（=表已删空）；或为空指针（=原表为空）。
程序样例