指针逻辑

1. 简介

指针就是一个程序变量, 作用是指向其他程序结构. 这里的程序结构可以是一个变量, 一个函数, 或者另一个指针. 同时, 指针可以允许对一个数据集合进行操作来提升程序运行的效率.

指针能够工作的基础是因为计算机体系结构存在内存单元, 而且这些内存单元有与之对应的地址或者说编号. 指针的值无非就是内存单元的地址. 而指针作用的方式就是这些内存单元寻址的方式, 称为内存模型(memory model).

内存模型描述的是关于内存单元寻址方式的假设. 我们假定内存提供一块连续的统一的内存空间, 比如说地址空间集合 \(A\) 用一个整数集合表示 \(\{0,...,N-1\}\). 每一个地址都对应一个内存单元, 可以用来存储一个数据字(data word). 数据字的集合记为 \(D\). 一种映射关系内存取值(memory valuation)是从地址集合到数据字集合的映射.

编译器为每一个全局变量都分配一个特定的内存位置即地址. 这种映射关系称为内存布局(memory layout). 内存布局 \(L:V\longrightarrow A\) 是一个每一变量 \(v\in V\) 到一个地址 \(a\in A\) 的映射关系. 变量 \(v\) 的地址称为自身的内存位置(memory location).

指针除了能够为变量静态分配内存空间, 也能够为一些动态数据结构分配地址空间. 动态数据结构依赖于指定的内存区域, 以供程序运行时创建的对象使用. 运行时库维护一个未使用内存区域的链表. 该库中的一个函数, 分配一个指定大小的空间区域, 并返回一个指向该内存区域开始(低地址)的指针. 因此, 内存布局会在运行时发生相应的变化. 只要有足够的空间, 内存分配就能够无限制地执行, 因此创建对象的数量理论上也是无上限的. 在编程语言中, 实现这种内存分配的函数, 在 C 中是 malloc(), 在 C++, C# 和 Java 中是 new 关键字. 相应, 如果为了重用不再需要的数据结构所占用的内存, C 程序调用 free, C++ 调用 delete, C# 和 Java 分别有自己的垃圾回收机制. 那么, 动态对象的生命周期是其分配与释放之间的时间.

2. 简单的指针逻辑

指针逻辑的语法如下: \[ \begin{align*} formula\ &:\ formula\land formula\ |\ \neg formula\ |\ (formula)\ |\ atom\\ atom\ &:\ pointer = pointer\ |\ term = term\ |\ pointer <pointer\ |\ term < term\\ pointer\ &:\ pointer-identifier\ |\ pointer + term\ |\ (pointer)\ |\ \&identifier\ \\ &\;|\;\&*pointer\ |\ *pointer\ |\ NULL\\ term\ &:\ identifier\ |\ *pointer\ |\ term\ op\ term\ |\ (term)\ \\ &\;|\;integer\text{-}constant\ |\ identifier[term]\\ op\ &:\ +\ |\ - \end{align*} \] 合法的指针逻辑公式:

• \(*(p+i)=1\),
• \(*(p+*p)=0\),
• \(p=q\land *p=5\),
• \(*****p=1\),
• \(p\lt q\).

不合法的指针逻辑公式:

• \(p+i\),
• \(p=i\),
• \(*(p+q)\),
• \(*1=1\),
• \(p\lt i\).

3.堆数据结构的建模

3.1 链表

在程序中, 堆上分配的数据结构起着非常重要的作用, 也是形成指针错误的重要原因. 接下来说明如何通过指针逻辑去建模常用的数据结构.

在数组之后, 比较常见的动态分配的数据结构是链表. 它通常是通过一种结构类型来实现的, 该结构类型包含下一个指针的字段以及要存储在列表中的数据. 比如, 下图所示的单向链表,

用递归定义的方式定义上面的单向链表中第 \(i\) 个成员: \[ \begin{aligned} list\text{-}elem(p,0)&\doteq p,\\ list\text{-}elem(p,i)&\doteq list\text{-}elem(p,i-1)\to n\ for\ i\ge 1 \end{aligned} \] 接下来定义长度为 \(l\), 以NULL指针结束的单向链表 \(list(p,l)\): \[ list(p,l)\doteq list\text{-}elem(p,l)=\rm NULL. \] 如果是循环链表

定义为 \[ \begin{align*} c\_list(p,l)\doteq list\text{-}elem(p,l)=p. \end{align*} \] 但是, 如上定义是不严谨的. 因为, 如果只有一个元素的循环单链表也是符合如上定义的.

这是由于尽管我们打算指定存在 \(l\) 个不相交的链表元素, 但我们的定义并不能够排除共享链表元素的事实. 这种性质通常称为分离性质(separation properties), 断言链表元素不相交的一种方法是定义overlap, 如下所示: \[ overlap(p,q)\doteq p=q\lor p=q+1\lor p+1=q. \] 由此可以声明链表元素彼此不相交: \[ \begin{aligned} list\text{-}disjoint(p,0)&\doteq \rm TURE,\\ list\text{-}disjoint(p,l)&\doteq list\text{-}disjoint(p,l-1)\land\\ &\forall 0\le i\lt l-1.\neg overlap(list\text{-}elem(p,i), list\text{-}elem(p,l-1)). \end{aligned} \]

3.2 树

我们可以通过向数据结构的每个元素添加另一个指针域来实现二叉树.

上图所示的是二叉排序树, 我们用 \(l\) 表示左子树节点, \(r\) 表示右子树节点. 只要给定一个整数, 该二叉树能够在 \(O(h)\) 时间复杂度内结束查询, 其中 \(h\) 是树的高度. 同样地, 二叉排序树的性质可以表示为: \[ \begin{aligned} (n.l\ne NULL\Longrightarrow n.l\to x\lt n.x)\\ \land (n.r\ne NULL\Longrightarrow n.r\to x\gt n.x). \end{aligned} \] 但是以上公式并不完整. 因此, 我们需要定义谓词 \(tree\text{-}reach(p,q)\), 如果 \(p\) 能够在一步到达 \(q\), 那么该谓词为真. \[ tree\text{-}reach(p,q)\doteq p\ne NULL \land q\ne NULL\land \\ (p=q\lor p\to l=q\lor p\to r =q). \] 为了获得一个谓词, 该谓词在当且仅当 \(q\) 在任意数量的步骤中可以从 \(p\) 到达时才成立, 我们需要定义一个给定二元关系 \(R\) 上的传递闭包(transitive closure).

transitive closure: 给定一个二元关系 \(R\), 如果存在 \(z_1,...,z_n\), 那么存在关于 \(x,y\) 的传递闭包: \[ xRz_1\land z_1Rz_2 \land...\land z_nRy. \] 传递闭包可以形式化地递归定义如下: \[ \begin{aligned} TC_R^1(p,q)&\doteq R(p,q),\\ TC_R^i(p,q)&\doteq \exists p'.TC_R^{i-1}(p,p')\land R(p',q),\\ TC(p,q)&\doteq \exists i.TC^i_R(p,q). \end{aligned} \] 利用 \(tree-reach\) 关系的传递闭包, 可以得到一个新的关系 \(tree-reach^*(p,q)\), 该关系成立当且仅当 \(q\) 从 \(p\) 在任意步之内是可达的: \[ tree\text{-}reach^*(p,q)\Longleftrightarrow TC_{tree\text{-}reach}(p,q). \] 所以可以扩展二叉排序树的性质: \[ (\forall p.tree-reach^*(n.l,p)\Longrightarrow p\to x\lt n.x)\\ \land (\forall p.tree-reach^*(n.r,p)\Longrightarrow p\to x\gt n.x) \]

4. 基于规则的判定过程

指针逻辑所具有的表达能力可以对像链表, 树这样的数据结构建模, 可以应用到基于规则的判定程序中去.

基本思想是, 定义一个指针逻辑的片段(fragment), 对于特定类型数据结构(链表, 树)的谓词进一步对该指针逻辑进行修饰, 还有一组足以证明在实践中产生的各种验证条件的证明规则.

首先对之前用于指定链表的 \(list\text{-}elem\) 进行泛化, 将结构中"next"指针域对其进行参数化. 假设 f 是一种结构的指针域. \(follow_n^f (q)\) 代表的是, 指针 q 沿着指针域 f 连续移动 n 次. \[ \begin{aligned} follow_0^f(p)&\doteq p,\\ follow_n^f(p)&\doteq follow_{n-1}^f(p)\to f. \end{aligned} \] 如果 \(follow_n^f (p)=q\) 成立, 就说指针 p 沿着指针域 f 的方向移动 n 次之后能够到达(reach) q. 可以用类似链表形式的谓词对此进行说明: \[ p\xrightarrow[x]{f}q \] 上面的谓词称作可达性谓词(reachability predicate). 可以用 follow() 将其形式化为: \[ p\xrightarrow[x]{f}\Longleftrightarrow \exists n.(follow_n^f(p)=q\land \forall m\lt n.follow_m^f(p)\ne x). \] 考虑如下程序验证问题.

struct S
{
    struct S *next;
    int payload;
}*list;
bool find(int a){
    for(struct S *p; p!=0; p=p->next){
        if (p->payload == a)	return true;
    }
    return false;
}

可以用如下公式说明上述例程返回结果的正确性 \[ find(a)\Longleftrightarrow \exists p'.(list\xrightarrow[0]{next}p'\land p'\to payload=a). \] 如果以下两个条件满足则说明 find(a) 为真:

• 在指针域的方向上, 存在一个链表元素在不经过NULL指针的情况下是可达的;

• 该链表元素的值等于 a.

循环体开始的不变式定义为 INV: \[ {\mathbf{\rm INV}}:=list\xrightarrow[0]{next}p\land (\forall q\ne p.list\xrightarrow[p]{next}q\Longrightarrow q\to payload\ne a). \] 程序执行过程中, 保持循环不变式的性质; 同时, INV能够蕴涵这种特性. 形式化地, 这种性质可以用四个验证条件表明. 所有验证条件的有效性能够说明循环不变式的性质. \[ \begin{aligned} {\rm \mathbf{IND\text{-}BASE}}&:=p=list \Longrightarrow {\rm \mathbf{INV}}\\ {\rm \mathbf{IND\text{-}STEP}}&:=({\rm \mathbf{INV}}\land p\to payload\ne a)\Longrightarrow {\rm \mathbf{INV}}[p/p\to next]\\ {\rm \mathbf{VC\text{-}P1}}&:=({\rm \mathbf{INV}}\land p\to payload=a)\\&\Longrightarrow \exists p'.(list\xrightarrow[0]{next}p'.p'\to payload=a)\\ {\rm \mathbf{VC\text{-}P2}}&:=({\rm \mathbf{INV}}\land p=0)\Longrightarrow \neg \exists p'.(list\xrightarrow[0]{next}p'.p'\to payload=a) \end{aligned} \] 证明这些验证条件的正确性, 就可表明程序满足所要求的性质.

判定可达性谓词公式

以验证条件 IND-BASE 为例 \[ \begin{aligned} &p=list \Longrightarrow {\rm \mathbf{INV}}\\ &\Longleftrightarrow p=list \Longrightarrow list\xrightarrow[0]{next}p\land (\forall q\ne p.list\xrightarrow[p]{next}q\Longrightarrow q\to payload\ne a)\\ &\Longleftrightarrow list\xrightarrow[0]{next}list\land (\forall q\ne list.list\xrightarrow[list]{next}q\Longrightarrow q\to payload\ne a)\\ &\Longleftrightarrow (\exists n.follow_n^{next}(list)=list\land \forall m\lt n.follow_m^{next}(list)\ne list)\land\\ &\quad\quad\;\;(\forall q\ne list.((\exists n.follow_n^{next}(list)=q\land \forall m\lt n.follow_m^{next}(list)\ne list)\\ &\quad\quad\;\Longrightarrow q\to payload\ne a)). \end{aligned} \] 证明如下可达性谓词的有效性 \[ list\xrightarrow[0]{next}list\land (\forall q\ne list.list\xrightarrow[list]{next}q\Longrightarrow q\to payload\ne a) \] 即证 \[ (\forall q\ne list.list\xrightarrow[list]{next}q\Longrightarrow q\to payload\ne a) \] 引入 Skolem 变量, 消除全称量词 \[ (q'\ne list\land list\xrightarrow[list]{next}q'\Longrightarrow q'\to payload\ne a) \] 因为 \(list\xrightarrow[list]{next}q' \Longleftrightarrow list=q'\), 所以蕴涵式的左边为假, 整体为真, 原式得证.