数组理论 (一)

1. 数组

现代多数编程语言都对数组类型提供了支持, 并且数组在对像内存这样的硬件组件建模时也会用到. 所以对硬件系统的分析就要求能够对包含数组的公式进行判定. 首先说明如何用数组理论对一个循环不变式进行判定.

考虑如下伪代码片段: \[ \begin{aligned} &a: \mathbf{array}\ 0..99\ \mathbf{of\ integer;}\\ &i: \mathbf{integer;}\\ \\ &\mathbf{for}\ \rm i:=0\ \mathbf{to}\ 99\ \mathbf{do}\\ &\hspace{2cm} \mathbf{assert} (\forall x\in \mathbb{N}_0.x\lt i\Longrightarrow a[x]=0);\\ &\hspace{2cm} \rm a[i]:=0;\\ &\hspace{2cm} \mathbf{assert}(\forall x\in \mathbb{N}_0.x\le i \Longrightarrow a[x]=0);\\ &\mathbf{done;}\\ &\mathbf{assert}(\forall x\in \mathbb{N}_0.x\le 99 \Longrightarrow a[x]=0); \end{aligned} \] 正确性论证的主要步骤是在执行循环体内的赋值时, 证明赋值之后的断言是从赋值前的断言中产生的. 通常的做法是生成验证条件(verification conditions), 比如说, 使用霍尔公理系统(Hoare's axiom system). 能够得到如下的验证条件: \[ \begin{gather*} (\forall x\in \mathbb{N}_0.x\lt i\Longrightarrow a[x]=0) \\ \land a'=a\{i\leftarrow 0\}\\ \Longrightarrow (\forall x\in \mathbb{N}_0.x\le i \Longrightarrow a'[x]=0).\tag{f.1} \end{gather*} \]

数组理论允许对数组进行公式化的表达, 数组被形式化为从索引类型(index type)到元素类型(element type)的映射. 用 \(T_I\) 表示索引类型, \(T_E\)表示元素类型. 数组自身的类型表示为 \(T_A\), 也就是 \(T_I \rightarrow T_E\) 的简写形式, 比如说, 将 \(T_I\) 的一个元素映射到 \(T_E\) 的一个元素的函数的集合. 索引集和元素集都不需要是有限的.

令 \(a\in T_A\) 表示一个数组. 有两个基本的数组操作:

1. 从 \(a\) 中读取一个下标为 \(i\in T_I\) 的元素. 下标为 \(i\) 的元素的值表示为 \(a[i]\). 该运算符称作数组索引运算符.
2. 向 \(a\) 中写入一个下标为 \(i\in T_I\) 的元素. 令 \(e\in T_E\) 表示要写入的值. 数组 \(a\) 中元素 \(i\) 被 \(e\) 替换记为 \(a\{i\leftarrow e\}\). 该运算符称作数组更新或者数组存储运算符.

我们将用于推理索引和元素的理论分别称为索引理论(index theory)和要素理论(element theory). 数组理论通过索引和元素理论进行参数化. 通过递归地定义 \(T_A(n)\) 就能得到 \(n\) 维数组. 对于 \(n \ge 2\), 我们只需将 \(T_A(n-1)\) 添加到 \(T_A(n)\) 的元素类型中去.

索引和元素理论的选择将影响所得数组理论的表达能力. 例如, 索引理论需要允许存在和全称量词, 以便对诸如"存在一个数组元素为零"或"该数组的所有元素都大于零"之类的属性进行建模. 合适的索引理论的一个例子是Presburger算术(Presburger arithmetic), 即具有量词的整数的线性演算.

1.1 语法

我们将数组理论的语法定义为对索引理论和元素理论的组合的扩展. 令 \(term_I\) 和 \(term_E\) 分别表示这两个理论中的一项. 先定义一个数组项 \(term_A\): \[ term_A:array-identifier\ |\ term_A\{ term_I\leftarrow term_E \}. \] 然后将元素的项扩展至包含数组元素, 比如说, \[ term_E:term_A[term_I]\ |\ (previous\ rules), \] 其中 \(previous\ rules\) 表示在此扩展之前定义 \(term_E\) 的语法规则. 最终, 我们通过允许数组项之间的等式来扩展公式中的谓词: \[ formula:term_A=term_A\ |\ (previous\ rules), \] 其中 \(previous\ rules\) 表示在此扩展之前定义 \(formula\) 的语法规则. 如果索引理论包括量词, 则在数组之间具有显式等式的语法的扩展是多余的, 因为对于数组 \(a_1\) 和 \(a_2\),如果 \(a_1 = a_2\), 那么该等式也可以写成 \(\forall i.a_1[i]=a_2[i]\).

1.2 语义

我们用三个公理说明数组理论中新的原子和项的含义.

第一个公理给出了数组索引运算符的确切含义. 如果数组相同并且索引相同, 则两个数组索引项的值相同. \[ \forall a_1\in T_A.\forall a_2\in T_A.\forall i\in T_I.\forall j\in T_I.(a_1=a_2\land i=j)\Longrightarrow a_1[i]=a_2[j].\tag{a.1} \] 用于定义数组更新运算符含义的公理是"读写公理"(read-over-write axiom): 数组值 \(e\) 在被写入下标为 \(i\) 的数组 \(a\) 中之后, 那么该数组索引为 \(i\) 的值就为 \(e\). 数组中任意下标不为 \(i\) 的值与写之前一致: \[ \forall a\in T_A.\forall e\in T_E.\forall i\in T_I.\forall j\in T_I.a\{ i\leftarrow e\}[j]= \begin{equation} \left\{ \begin{array}{lr} e&:&i=j\\ a[j]&:&otherwise. \end{array} \right. \end{equation}\tag{a.2} \] 最后, 我们用可扩展性规则(extensionality rule)赋予数组相等的明显的含义: \[ \forall a_1\in T_A.\forall a_2 \in T_A.(\forall i\in T_I.a_1[i]=a_2[i])\Longrightarrow a_1=a_2.\tag{a.3} \]

2. 消除数组项

我们提出一种将数组理论中的公式转换为由索引理论和元素理论组成的公式的方法. 如果这种组合的理论包含未解释函数和针对索引的量词, 该变换是可应用的.

考虑公理 \(a.1\), 该公理定义了数组索引操作符的语义. 再考虑以下函数一致性. 非正式地, 函数一致性要求同一个函数的两个应用, 如果它们的参数一样的话, 那所得到的返回结果必须一致. 可以将公理 \(a.1\) 看作是函数一致性的一种特例.

可以用一个未解释函数对数组索引操作符做替换. 有如下数组理论公式, 其中 \(a\) 是一个 \(\rm char\) 类型的数组: \[ (i=j\land a[j]='z')\Longrightarrow a[i]='z'. \] 字符常量 \('z'\) 是一个数组元素的成员. 令 \(F_a\) 代表为数组 \(a\) 引入的未解释函数: \[ (i=j\land F_a(j)='z')\Longrightarrow F_a(i)='z'. \] 上面的公式用针对等式和未解释函数的判定程序可以验证其有效性.

关于数组更新操作符. 一种对数组更新操作进行建模的方法是用一个新的同类型的数组变量 \(a'\) 替换 \(a\{i\leftarrow e\}\) 形式的每一个表达式. 然后, 添加两个约束, 这些约束直接对应于可重写公理的两种情况:

1. \(a'[i]=e\) 为要写入的值,
2. \(\forall j\ne i.a'[j]=a[j]\) 为那些未改变的值.

以上称之为写规则(write rule), 是对数组理论公式的等价保留转换.

比如说, 公式 \[ a\{i\leftarrow e\}[i]\ge e \tag{2.1} \] 就是通过引入一个新的数组标识符 \(a'\) 替换了 \(a\{i\leftarrow e\}\) 转换过来的. 另外, 添加约束 \(a'[i]=e\), 就能得到 \[ a'[i]=e \Longrightarrow a'[i]\ge e, \] 上式子也显示了(2.1)的有效性. 需要使用重写公理的第二部分来显示如下公式的有效性 \[ a[0]=10\Longrightarrow a\{1\leftarrow 20\}[0]=10. \] 和以前一样, 通过用新的标识符 \(a'\) 替换 \(a\{ 1\leftarrow 20 \}\), 并添加上述两个约束来对公式进行转换: \[ (a[0]=10\land a'[1]=20\land (\forall j\ne 1.a'[j]=a[j]))\Longrightarrow a'[0]=10. \] 通过使用两个未解释函数 \(F_a\) 和 \(F_b\) 分别替换 \(a\) 和 \(a'\) 得到: \[ (F_a(0)=10\land F_{a'}(1)=20\land (\forall j\ne 1.F_{a'}(j)=F_a(j))\Longrightarrow F_{a'}(0)=10. \] 这个简单的例子表明, 只要索引理论提供了量词, 数组理论就可以简化为索引理论和未解释函数的组合. 问题在于这种组合不一定是可判定的. 带有量词的便捷索引理论是Presburger演算, 实际上, 它与未解释函数的组合是不可判定的. 如上所述，即使索引理论和元素理论的组合是可判定的, 数组理论也是不可判定的. 因此需要限制所考虑的公式集, 以便得到一个判定程序. 这是归约算法使用的方法.

3. The Reduction Algorithm

规约算法从数组理论的数组属性片段中接收一个公式, 并将其简化为一个使用元素和索引理论与等式和未解释函数相结合的可满足公式. \[ \begin{aligned} &\mathbf{Algorithm\ 1}:\ \text{ARRAY-REDUCTION}\\ \\ &\mathbf{Input:}\ \text{An array property formula}\ \phi_A\ \text{in NNF}\\ &\mathbf{Output:}\quad \text{A formula }\phi_{UF}\ \text{in the index and element theories with}\\ &\quad\quad\quad\quad\quad\; \text{uninterpretedted functions}\\ \\ &1.\; \text{Apply the write rule to remove all array updates from }\phi_A.\\ &2.\; \text{Replace all existential quantifications of the form}\ \exists i\in T_I.P(i)\ \text{by}\ P(j),\\ &\quad\;\text{where } j\ \text{is a fresh variable}.\\ &3.\; \text{Replace all universal quantifications of the form }\forall i\in T_I.P(i)\ \text{by }\\ &\hspace{73mm} \bigwedge_{i\in\mathcal{I}(\phi)} P(i).\\ &4.\; \text{Replace the array read operators by uninterpreted function and obtain}\\ &\quad \phi_{UF};\\ &5.\; \mathbf{return}\; \phi_{UF}; \end{aligned} \]

上述算法将一个数组理论公式作为输入. 将数组属性(也就是数组理论公式的标准型)转换为否定范式可能会将索引的全称量词转换为存在量词. 由于句法上的限制, 公式不包含明显的量词替换. 算法第一步, 应用写规则并移除所有的数组更新操作符. 所得到的公式包含针对索引的量词, 数组读取操作, 基于元素和索引理论的子公式.

因为公式是否定范式形式的, 所以存在量词可以用一个新的变量(也就是隐式地存在量化)进行替换. 全称量词 \(\forall i\in T_I.P(i)\) 用合取式 \(\bigwedge_{i\in \mathcal{I}(\phi)}P(i)\) 进行替换, 其中集合 \(\mathcal{I}(\phi)\) 表示索引表达式, \(i\) 就可能与公式 \(\phi\) 等价. 该集合包含如下元素:

1. 在 \(\phi\) 中用作数组索引的所有表达式均不是量化变量.
2. 在 \(\phi\) 中的数组索引表达式内使用的所有表达式都不是量化变量.
3. 如果公式 \(\phi\) 均不包含以上两项, 为了获得一组非空的索引表达式, \(\mathcal{I}(\phi)\) 就必须为 \(\{0\}\).

最后, 数组读取操作符就用未解释函数进行了替换.

用一个例子说明规约算法的流程:

证明如下公式的有效性: \[ \begin{gather*} (\forall x\in \mathbb{N}_0.x\lt i\Longrightarrow a[x]=0) \\ \land a'=a\{i\leftarrow 0\}\\ \Longrightarrow (\forall x\in \mathbb{N}_0.x\le i \Longrightarrow a'[x]=0). \end{gather*} \] 也就是说, 要说明以下公式的不可满足性: \[ \begin{gather*} (\forall x\in \mathbb{N}_0.x\lt i\Longrightarrow a[x]=0) \\ \land a'=a\{i\leftarrow 0\}\\ \land(\exists x\in \mathbb{N}_0.x\le i \land a'[x]\ne0). \end{gather*} \] 应用写规则,得到 \[ \begin{gather*} (\forall x\in \mathbb{N}_0.x\lt i\Longrightarrow a[x]=0) \\ \land a'[i]=0\land \forall j\ne i.a'[j]=a[j]\\ \land (\exists x\in \mathbb{N}_0.x\le i \land a'[x]\ne0). \end{gather*} \] 算法的第二步, 用一个新变量 \(z\in \mathbb{N}_0\) 实例化存在量词: \[ \begin{gather*} (\forall x\in \mathbb{N}_0.x\lt i\Longrightarrow a[x]=0) \\ \land a'[i]=0\land \forall j\ne i.a'[j]=a[j]\\ \land z\le i\land a'[z]\ne0. \end{gather*} \] 这个例子中的集合 \(\mathcal{I}\) 为 \(\{i,z\}\). 所以替换两个全称量词: \[ \begin{gather*} (i\lt i\Longrightarrow a[i]=0)\land (z\lt i\Longrightarrow a[z]=0) \\ \land a'[i]=0\land (i\ne i\Longrightarrow a'[i]=a[i])\land(z\ne i\Longrightarrow a'[z]=a[z])\\ \land z\le i\land a'[z]\ne0. \end{gather*} \] 删除显然满足的合取式子: \[ \begin{gather*} (z\lt i\Longrightarrow a[z]=0) \\ \land a'[i]=0\land(z\ne i\Longrightarrow a'[z]=a[z])\\ \land z\le i\land a'[z]\ne0. \end{gather*} \] 然后分别用未解释函数 \(F_a\) 和 \(F_{a'}\) 替换两个数组 \(a\) 和 \(a'\): \[ \begin{gather*} (z\lt i\Longrightarrow F_a[z]=0) \\ \land F_{a'}[i]=0\land(z\ne i\Longrightarrow F_{a'}[z]=F_a[z])\\ \land z\le i\land F_{a'}[z]\ne0. \end{gather*} \] 通过区分 \(z\lt i\), \(z = i\) 和 \(z\gt i\) 三种情况, 很容易看出该公式是不可满足的.