复杂的程序常常含有指针以及递归数据结构, 这类程序的证明是困难的.即使提供了断言 (assertion) 和不变式 (invariant), 目前的工作, 如文献[1-3], 仍然难以验证动态操纵堆的性质.验证工具如VeriFast^[1]和Bedrock^[2]需要用户写低层次的辅助定理 (low-level lemmas) 和证明策略 (proof tactics) 去指导验证.它们要求用户熟悉程序 (code) 和规约语言 (specification), 需要用户提供合适的不变式 (invariant)——这是非常困难的工作.

为了简化证明复杂程序的难度, 本文提出了利用抽象程序辅助证明具体程序的方法.抽象程序是指使用抽象数据结构 (ADTs), 如set, list, map及其上的操作的程序.具体程序即真正的程序, 比如C语言程序.利用抽象程序, 本文的方法将复杂具体程序的证明分成两步:首先证明抽象程序满足规约 (本文不关注抽象程序的证明); 然后证明具体程序和抽象程序满足一致性.这种分层次证明可以简化证明难度, 这体现在:

(1) 抽象程序的证明比较容易.抽象程序使用抽象数据类型描述程序, 从而抽离了实现细节, 比如指针等;

(2) 一些复杂经典的算法 (如图算法) 在书中使用抽象程序的形式描述, 它们已被严格地验证了正确性.程序员只需实现这些算法, 然后证明具体实现和抽象算法满足一致性即可;

(3) 在软件开发过程中, 程序员需要将高层的设计 (high-level design) 转化为底层实现, 程序员常常使用抽象程序理解和描述算法, 程序员有必要证明底层实现符合高层的设计.有时候根据不同的环境, 具体程序会有多个实现版本, 分层证明之后, 程序员只需要证明1次抽象程序, 然后证明多个版本的具体程序和抽象程序满足一致性, 从而减少证明负担;

(4) 本文将展示证明抽象程序和具体程序满足一致性关系是相对简单的.通常, 抽象程序和具体程序的一致性证明可以被分解, 分解后往往变成了对抽象数据类型的操作, 从而可能实现自动证明.

本文主要关注抽象程序和具体程序的一致性关系证明.图 1显示了证明抽象程序与具体程序一致性关系的框架.

·首先, 需要用户给出抽象程序和具体程序, 然后给出抽象程序变量和具体程序变量的等式关系以及抽象程序程序点和具体程序程序点的对应关系;

·之后验证义务生成器会在具体程序程序点上生成验证义务;

·最终, 通过程序证明工具证明具体程序上的验证义务是否成立:如果成立, 那么具体程序和抽象程序满足一致性关系; 否则, 无法确定.

1 一个例子

考虑证明图 2所示的程序 (Ci表示程序点).

程序点C1给出前置条件, C5给出后置条件.SL_IsSList(first) 表示first指向一个单链表.SL_IsSList定义如下:

SL_IsSList(x:P(Node)):bool$\triangleq $x=NULL?true:SL_IsSList(x→Link).

SL_DataList(first) 从first指向的单链表中生成数据域D的set.SL_DataSet定义如下:

SL_DataSet(x:P(Node)):Set(int)$\triangleq $x=NULL?{}:x→D+SL_DataSet(x→Link).

在程序点C5, SL_DataSet(second)=SL_DataSet(first)@C1表示second指向的数据域的集合等于程序点C1处first指向的数据域的集合.

翻转链表程序中存在循环, 为了证明图 2中的性质, 验证工具需要用户提供合适的循环不变式, 但这一工作往往是困难的.在这个证明中, 需要下面的不变式.

SL_NodeSet(first)+SL_DataSet(second)=SL_NodeSet(first)@C1

SL_NodeSet(first)∩SL_DataSet(second)=∅

SL_IsSList(first)

SL_IsSList(second)

SL_NodeSet定义如下:

SL_NodeSet(x:P(Node)):Set(P(Node))$\triangleq $x=NULL?{}:x+SL_DataSet(x→Link).

1.1 利用抽象程序证明具体程序

在软件开发过程中, 程序员常常使用抽象程序理解和描述算法.图 3给出了翻转链表的抽象程序 (Ai表示程序点).对应地, 本文将最终的实现称作具体程序 (如图 2所示).

抽象程序和具体程序之间存在对应关系.这体现在如下几个方面.

·抽象程序中的变量实现为具体程序中的变量.

$ firstList=SL\_DataList(first),\text{ }secondList=SL\_DataList(second). $

SL_DataList定义如下:

SL_DataList(x:P(Node)):List(int)$\triangleq $x=NULL?[]:x→D+SL_DataList(x→Link).

·抽象程序中的语句实现为具体程序中的语句.

程序点Ai~Aj之间的语句对应程序点Ci~Cj之间的语句.根据语句的对应关系, 可以将整个程序的一致性关系证明分解为若干语句的一致性证明义务, 从而减少证明负担.

根据本文的方法, 要证明翻转链表抽象程序 (如图 3所示) 的循环体 (A3~A4) 与其具体程序 (图 2所示) 的循环体 (C3~C4) 满足一致性关系, 只需证明图 4中的性质.为了证明图 4所示的性质, 只需满足下面的条件:

$SL\_IsSList\left( first \right)$

(1)

$SL\_IsSList(second)$

(2)

$SL\_NodeSet(first)\cap SL\_NodeSet(second)=\varnothing $

(3)

相对于证明具体程序而言, 证明一致性关系不再需要下面的不变式.

$SL\_DataSet\left( first \right)+SL\_DataSet\left( second \right)=SL\_DataSet\left( first \right)@C1$

(4)

公式 (1)~公式 (3) 是关于指针的形状 (shape) 性质, 目前有大量形状分析 (shape abalysis) 的工作^[4-9].利用这些形状分析结果, 图 4中的证明可以达到自动化的证明.比如, 可以使用文献[2, 10, 11]的方法达到自动化的证明.

2 程序一致性关系

本节介绍程序语法、程序的精化关系以及一致性关系.

2.1 程序语法

具体程序就是C语言语法.因此, 这里只给出抽象程序的语法.抽象程序使用抽象数据结构 (ADTs), 如set, list, map及其上的操作.抽象程序语法如下.

$ \begin{align} & type::=set|list|map|BiRelation \\ & st::=e1:=e2|st;st|\bf{if} (e)\rm{ }st \bf{else} st|\bf{while} (e)\rm{ }st. \\ \end{align} $

BiRalation是两个集合的笛卡尔乘积, map是数学上的函数.表 1给出了ADT上的常见操作.

表 1中, S表示集合, L表示序列, M表示Map, x表示元素.

2.2 精化关系

程序B是程序A的精化, 意味着B应该满足任何A满足的规约^[12].即:在任何上下文中, B可以替换A.使用连接不变式 (coupling invariant)I, 精化条件可以表达成下面的形式^[12].

$wp(A,\top)\wedge I\Rightarrow wp(B,\neg wp(A,\neg I))$

(5)

连接不变式I描述A和B变量之间的关系.wp(B, Q) 表示当程序B终止并且满足后置条件Q时, 程序需要满足的最弱前置条件.精化条件 (5) 表示:对于任何初始条件满足连接不变式I的B的执行, 存在一个A的天使 (angelic) 执行, 使得I在A和B的最终状态仍然成立.如果程序A是确定性的 (deterministic), 精化条件 (5) 可以简化为

$wp(A,\top)\Rightarrow wp(assume\text{ }I;B;A;assert\text{ }I;\top)$

(6)

公式 (6) 要求A和B的状态空间不相交, A和B的初始和最终状态满足I.本文描述的抽象程序全部满足确定性.

2.3 一致性关系

精化关系要求具体程序能够满足抽象程序的所有前后置条件, 但在实际过程中, 抽象程序往往具有确定的前后置条件.因此, 本文提出了比精化关系更弱的一致性关系.

为了描述抽象程序和具体程序的一致性关系, 首先需要描述一致性标准 (consistency criterion).一致性标准是一个二元组 (S, E).S是一个程序规约, 表示为前置条件P和后置条件Q组成的二元组 (P, Q).E是抽象变量与具体变量的等式关系, E的形式如下:

Abv=exp (Cv1, Cv2, …, Cvn).

Abv表示抽象变量, Cv表示具体变量.抽象变量等于一组具体变量的表达式.E可以看作满足如上等式关系的连接不变式.

定义1(一致性关系).令S=(P, Q) 是一个程序规约, ProgA是一个满足P{ProgA}Q的抽象程序, C=(S, E) 是一个一致性标准, 一个具体程序ProgC是ProgA关于C的一致性实现, 标记为ProgC < _cProgA, 假如

M(P){ProgC}M(Q)

成立, 其中, M是一个映射函数, M(P) 和M(Q) 分别是通过一致性标准中的变量等式关系E, 将P和Q中的抽象变量替换为对应具体变量表达式之后的公式.

根据一致性的定义, 如果P和Q是一致性标准C中给出的规约, 并且ProgC < _cProgA, 那么抽象程序ProgA满足P{ProgA}Q, 具体程序ProgC满足M(P){ProgC}M(Q).

一致性关系要弱于精化关系, 这体现在:ProgC和ProgA是在特定的一致性标准C下满足一致性关系, 即, ProgC只需要满足特定的规约:M(P) 和M(Q), 其中, P和Q是一致性标准C中给定的规约.直观上, 一致性关系可以看作:具体程序在特定的前置条件下实现了抽象程序; 而精化关系要求具体程序在任何前置条件下都实现了抽象程序.本文之所以提出一致性关系, 是因为在实际过程中, 抽象程序往往具有确定的前后置条件, 具体程序只需在该前置条件下实现抽象程序即可满足要求.基于一致性关系, 复杂程序的证明可以分成两步:首先证明抽象程序满足特定规约 (本文不关注抽象程序的证明), 然后证明具体程序是抽象程序在这个特定规约下的一致性实现.这样做的优点在于可以减少证明负担.

(1) 在第2步证明过程中, 可以利用第1步证明的结果, 从而减轻证明负担;

(2) 因为抽象程序和具体程序具有对应关系, 抽象程序和具体程序的一致性证明可以分解, 从而减轻了证明负担.

3 抽象程序和具体程序的对应关系

本文的方法需要用户建立抽象程序和具体程序的对应关系.主要有变量关系和程序点关系.下面分别介绍.

3.1 变量关系

变量关系由两部分构成.

(1) 抽象变量与具体变量的等式关系E, 它满足如下形式:

Abv=exp (Cv1, Cv2, …, Cvn).

Abv表示抽象变量, Cv表示具体变量.抽象变量等于一组具体变量的表达式, 这种表示形式方便将抽象变量替换为具体变量表达式, 这对于在具体程序点上生成验证义务是有用的.

(2) 具体变量数据结构内的不变式, 如指针指向单链表、数组是有序的, 等等.

下面用一个例子来讲解如何建立抽象变量和具体变量的等式关系.

如图 5所示, 抽象程序reach实现了从给定顶点v0找到它所有可达顶点的集合reachableSet的过程 (Ai和Ci表示程序点).抽象程序中, 抽象集合nds描述节点集合, nds上的二元关系edges表示边; 在具体程序中, 使用节点指针数组LinkedListNode^*A[n]表示图.

首先, 使用一些抽象符号将具体变量抽象成集合、序列等, 这些抽象符号由逻辑描述语言提供.本文使用文献[13]中的抽象符号.抽象变量nds和具体变量之间的等式关系如下:

nds=0…n-1.

然后, 使用ADT的运算符和lamda表达式构造复杂的抽象数据类型, 比如二元关系、Map等.

这里使用笛卡尔乘积x构造二元关系, 使用lamda表达式构造二元关系的集合.抽象变量edges和具体变量的等式关系如下:

edges=λ(x)({x}×SL_DataSet(A[x])) in (0…n-1).

3.2 程序点关系

本文的方法需要用户给出抽象程序程序点和具体程序程序点的对应关系.

抽象和具体的语句之间有一定的对应关系, 但是抽象程序和具体程序结构之间差异较大, 比如一个抽象语句可能被实现为具体程序中的一个循环语句, 因此, 自动建立语句之间的映射关系是比较困难的.但是程序员手动建立语句之间的对应关系是容易的, 因此, 本文的方法要求程序员手动建立语句之间的映射关系.

虽然抽象和具体的语句之间有一定的对应关系, 但是经常会出现一些语句之间不能直接对应的情况.图 6给出了语句无法直接对应的一个例子 (Ai和Ci表示程序点).

图 6(b)展示了Schorr-Waite算法, 它是一种垃圾回收的算法.一般的垃圾回收算法 (图 6(a)所示) 使用深度优先遍历 (DFS) 搜索, 使用一个栈记录当前访问路径.Schorr-Waite程序不使用栈, 仅使用图本身的指针实现回溯.

表 2给出了图 6中的变量对应关系, 其中, STACK定义如下:

STACK(x:P(Node)):List(P(Node))$\triangleq $x=NULL?[]:x+STACK(x→chk?x→r:x→l).

图 6中, 整个抽象程序对应整个具体程序, 但是抽象程序A5~A6之间的语句与具体程序C5~C6之间的语句不存在对应关系:因为C5~C6临时修改了图结构, 使得抽象程序点A6成立的性质

$L=L@A5$

(7)

$R=R@A5$

(8)

其所对应的具体性质 (9)、性质 (10) 在具体程序点C6上不成立.

$(\lambda (x)((x,x \to l)){\text{ in}}\;NS0) = (\lambda (x)((x,x \to l)){\text{ in}}\;NS0)@C5$

(9)

$(\lambda (x)((x,x \to r)){\text{ in}}\;NS0) = (\lambda (x)((x,x \to r)){\text{ in}}\;NS0)@C5$

(10)

这时, 采用语句对应方式导致抽象程序和具体程序无法分解证明.但是我们注意到:尽管A5~A6与C5~C6不存在完全的对应关系, 但是语句之间仍然存在部分的对应关系, 这体现在大部分A6处成立的性质, 如性质 (11)、性质 (12).

$explored = explored@A5$

(11)

$stack = tail(stack)@A5$

(12)

其对应的具体性质 (13)、性质 (14) 在C6处仍然成立.

$\{ x|x \in NS0 \wedge x \to mk = {\text{true}}\} = \{ x|x \in NS0 \wedge x \to mk = {\text{true}}\} @C5$

(13)

$[t] + STACK(p) = tail([t] + STACK(p))@C5$

(14)

为了获取抽象性质到具体性质的映射关系, 本文从程序点的角度来确定对应关系.这样操作更灵活, 可以避免一些语句无法完全映射的问题.

这里需要指出的是:虽然图 6的具体程序是抽象程序的精化, 但是因为具体程序临时修改了图结构, 导致语句无法分解对应, 精化关系证明无法分解.比如, 因为下面的连接不变式在图 6所示的A6和C6处不成立:

$ \begin{gathered} L = (\lambda (x)((x,x \to l)){\text{ in }}NS0), \hfill \\ R = (\lambda (x)((x,x \to r)){\text{ in }}NS0), \hfill \\ \end{gathered} $

所以图 6所示的A5~A6之间的抽象语句与C5~C6之间的具体语句不满足精化关系.

抽象程序程序点和具体程序程序点的对应关系能够帮助程序员减轻证明负担, 并且建立这种对应关系对于程序员是容易的.但并不是任何程序点的对应关系都是可行的, 下面给出合适的程序点对应关系需要满足的约束.

·合适的程序点对应关系.

合适的抽象程序程序点和具体程序程序点之间的对应关系满足下面的条件.

(1) 抽象程序的一个程序点最多只能和一个具体程序点对应, 但是多个抽象程序点可能对应到同一个具体程序点.

(2) 抽象程序的入口和出口必须分别对应于具体程序的入口和出口.

(3) 如果抽象程序中某个循环语句的内部有一个程序点和具体程序点对应, 那么,

  a) 抽象的循环语句必然和某个具体的循环语句对应; 且

  b) 抽象循环语句body之前/之后的程序点分别对应于这个具体循环语句的body之前/之后的程

序点;

  c) 抽象循环语句之前/之后的程序点分别对应于具体程序中的程序点.

(4) 如果抽象程序中的某个if语句内部的程序点和某个具体程序点对应, 那么,

  a) 这个if语句必然和具体程序中的某个if语句所对应;

  b) 抽象的if语句的两个分支之前/之后的程序点分别对应于相应具体if语句的两个分支之前/之后的程序点;

  c) 抽象if语句之前/之后的程序点分别对应于具体程序中的程序点.

(5) 对于抽象程序中两个任意的程序点AP和AQ, 如果AP dominate AQ且AQ reverse-dominate AP, 那么它们对应的具体程序点CP和CQ在具体程序中也有CP dominate CQ且CQ reverse-dominate CP.

4 验证义务

如果用户已经建立了抽象变量和具体变量之间的等式关系, 并已建立具体数据结构必须满足的性质, 即数据结构不变式, 并且已经给出抽象程序程序点和具体程序程序点的对应关系, 那么本文的方法能够在相应的具体程序点上生成验证义务.

4.1 基本验证义务

首先假设抽象程序已经是被证明的, 证明过程中的性质已被加入到各个抽象程序点上.为了证明抽象程序和具体程序满足一致性关系, 需要证明下面的验证义务.

·关于一致性标准C的基本验证义务.

对于任意对应的程序点AP及其所对应的具体程序点CP, 必须证明如下性质.

(1) 具体数据结构必须满足的性质, 即数据结构不变式, 在CP上成立;

(2) 对于AP上的性质P, 在CP上必须证明M(P) 成立, 其中, M(P) 是通过一致性标准C中的等式关系E和程序点对应关系, 将P中抽象变量、抽象程序点替换为对应具体变量、具体程序点之后的公式.

直观地, 基本验证义务就是将抽象程序点上的证明性质映射到对应的具体程序点上证明.

定理1.令S=(P, Q) 是一个程序规约, C=(S, E) 是一个一致性标准, ProgA和ProgC分别是抽象程序和具体程序.如果ProgA满足P{ProgA}Q, 并且ProgC满足关于一致性标准C的基本验证义务, 那么ProgC < _cProgA.

证明:因为P{ProgA}Q成立, 根据一致性关系的定义, 要证明ProgC < _cProgA, 只需证明M(P){PorgC}M(Q) 成立.P和Q分别是抽象程序入口和出口处的性质.因为程序点的映射必须满足合适的程序点对应关系, 所以抽象程序的入口和出口必须分别对应于具体程序的入口和出口.又因为关于C的基本验证义务成立, 所以M(P) 和M(Q) 分别在具体程序的入口和出口处成立, 即M(P){PorgC}M(Q) 成立.因此, ProgC < _cProgA.

4.2 简化证明义务

抽象程序点上可能有太多的证明过程中的性质, 其中, 部分的证明义务对于证明抽象程序和具体程序的一致性是冗余的.本节将介绍简化证明义务的两个规则.

·非循环语句的简化证明义务规则.

令抽象程序点Ai, Aj分别与Ci, Cj对应, Ai在Aj之前.Ast表示Ai和Aj之间的语句, Cst表示Ci和Cj之间的语句.Ast中不包括循环语句, 为了证明抽象语句Ast和具体语句Cst满足一致性关系, 只需在具体程序点Cj上证明如下性质:

$ M(sp(S,\overrightarrow {abv} = \overrightarrow {abv@Ai} )). $

$\overrightarrow {abv} $表示抽象语句Ast中的变量序列, $\overrightarrow {abv@Ai} $是变量序列$\overrightarrow {abv} $在程序点Ai的值.在程序点Ai处, $\overrightarrow {abv} = \overrightarrow {abv@Ai} $恒成立.M是抽象程序到具体程序的映射函数.M(P) 是将性质P中的抽象变量替换为对应具体变量, 抽象程序点替换为对应具体程序点后的性质.

sp表示最强后置条件 (strongest postconditions), $sp(Ast,\overrightarrow {abv} = \overrightarrow {abv@Ai} )$表示当程序Ast的初始条件满足$\overrightarrow {abv} = \overrightarrow {abv@Ai} $时, Ast终止时满足的最强的后置条件.当抽象语句Ast中没有循环语句时, $sp(Ast,\overrightarrow {abv} = \overrightarrow {abv@Ai} )$的计算是确定的.

定理2.令抽象程序点Ai, Aj分别与Ci, Cj对应, Ai在Aj之前.Ast表示Ai和Aj之间的语句, Cst表示Ci和Cj之间的语句, S=(P, Q) 是任何程序规约, E是变量对应关系, C=(S, E) 是一致性标准.如果Ast和Cst能够应用非循环语句的简化证明义务规则并且简化证明义务成立, 那么Cst < _cAst.

证明:这里直接使用一个精化方法的结论.如果下面公式可以被证明, 那么Ast和Cst满足精化关系^[14]:

$M(wp(Ast,{\text{true}}) \wedge \vec v = \overrightarrow {v@Ai} )\{ Cst\} M(sp(Ast,\vec v = \overrightarrow {v@Ai} ))$

(15)

其中, $\vec v$是Ast中的变量序列, $\overrightarrow {v@Ai} $是变量序列$\vec v$在程序点Ai的值.wp(Ast, true) 用于检查语句Ast是否终止.当语句Ast不包含循环语句时, 公式 (15) 可以简化为

$M(\vec v = \overrightarrow {v@Ai} {\text{)}}\{ Cst\} M(sp(Ast,\vec v = \overrightarrow {v@Ai} ))$

(16)

$M(\vec v = \overrightarrow {v@Ai} {\text{)}}$在Ci处恒成立.如果Ast和Cst能够应用非循环语句的简化证明义务规则并且简化证明义务成立, 那么公式 (16) 成立, Ast和Cst满足精化关系, 因此, Ast和Cst一定也满足关于一致性标准C的一致性关系Cst < _cAst.

推论1.如果抽象语句Ast和具体语句Cst可以应用非循环语句的简化证明义务规则, 并且简化证明义务可证, 那么Ast和Cst满足精化关系.

4.2.1 While循环语句

本节考虑while loop语句的简化证明义务.

表 3描述了抽象循环语句和具体循环语句, 其中, 抽象程序点Ai, Aj, Ak, Ap分别对应具体程序点Ci, Cj, Ck, Cp.注意, Ci不一定是具体循环语句直接前驱处的程序点.

· while语句的简化证明义务规则.

如果抽象循环语句的程序点和具体循环语句的程序点满足表 3所示的对应关系, 为了证明抽象循环语句和具体循环语句满足一致性关系, 只需证明下面的条件成立.

(1) 在具体程序点Cm处, $M(\overrightarrow {abv} = \overrightarrow {abv@Ai} )$成立;

(2) 在具体程序点Cj处, M(AbCon) 成立;

(3) 抽象循环体Ast₁和具体循环体Cst₁满足精化关系;

(4) 在具体程序点Cp处, M(﹁AbCon) 成立.

M(P) 是将P中的抽象变量替换为对应具体变量、抽象程序点替换为对应具体程序点后的公式.

定理3.令Ast和Cst分别表示抽象循环语句和具体循环语句, S=(P, Q) 是任何程序规约, E是变量对应关系, C=(S, E) 是一致性标准.如果Ast和Cst能够应用while语句的简化证明义务规则并且简化证明义务成立, 那么Cst < _cAst.

证明:如果能够证明Ast和Cst满足精化关系, 那么Cst < _cAst.对于任何前置条件P和后置条件Q使得P{Ast}Q成立, 只需证明M(P){Cst}M(Q) 成立即可.前置条件M(P) 在Ci处成立, 因为$M(\overrightarrow {abv} = \overrightarrow {abv@Ai} )$在C处成立, 所以M(P) 在Cm成立.令INV表示任何使得公式 (17) 成立的不变式.

$(P \Rightarrow INV) \wedge (INV \wedge AbCon\left\{ {As{t_1}} \right\}INV) \wedge (INV \wedge \neg AbCon \Rightarrow Q)$

(17)

因为Ast₁和Cst₁满足精化关系, 因此公式 (18) 成立.

$\begin{gathered} (M\left( P \right) \Rightarrow M\left( {INV} \right)) \wedge (M\left( {INV} \right) \wedge M\left( {AbCon} \right)\left\{ {Cs{t_1}} \right\}M\left( {INV} \right)) \hfill \\ \wedge (M\left( {INV} \right) \wedge M(\neg AbCon) \Rightarrow M\left( Q \right)) \hfill \\ \end{gathered} $

(18)

因为在Cm处M(P) 成立, 在Cj处M(AbCon) 成立, 在Cp处M(﹁AbCon) 成立, 并且公式 (18) 成立, 因此, M(P) {Cst}M(Q) 成立, Ast和Cst满足精化关系.因此, Cst < _cAst.

推论2.如果抽象语句Ast和具体语句Cst可以应用循环语句的简化证明义务规则, 并且简化证明义务可证, 那么Ast和Cst满足精化关系.

推论3.令S=(P, Q) 是任何程序规约, E是变量对应关系, C=(S, E) 是一致性标准.如果抽象语句Ast₁和Ast₂与具体语句Cst₁和Cst₂可以分别应用简化证明义务规则 (非循环语句简化规则或者循环语句简化规则), 并且简化证明义务可证, 那么Cst₁; Cst₂ < _cAst₁; Ast₂.

综上, 对变量对应关系E, 任何程序规约S=(P, Q), 一致性标准C=(S, E), 如果抽象语句Ast和具体语句Cst可以应用非循环语句简化规则或者循环语句简化规则, 并且简化证明义务成立, 那么Cst < _cAst.

5 案例研究

本节使用我们的方法验证reach程序 (如图 5所示) 和Schorre-Waite程序 (如图 6所示).

5.1 reach程序

图 5给出了抽象reach程序及其具体实现.抽象程序reach实现了从给定顶点v0找到它所有可达顶点的集合reachableSet的过程.表 4给出了reach抽象程序和具体程序的变量对应关系, 其中, SL_DataSet和SL_ DataSegment定义分别如下所示:

$ \begin{gathered} SL\_DataSet(x:\boldsymbol{P}(\boldsymbol{Node})):\boldsymbol{Set}(\boldsymbol{int}) \triangleq x = NULL?\{ \} :x \to node + SL\_DataSet(x \to next), \hfill \\ SL\_DataSegment(x:\boldsymbol{P}(\boldsymbol{Node}),y:\boldsymbol{P}(\boldsymbol{Node})):\boldsymbol{Set}(\boldsymbol{int}) \triangleq \hfill \\ (x = NULL)?\{ \} :((x = y)?\{ \} :p + SL\_NodeSetSeg(x \to next,y)). \hfill \\ \end{gathered} $

reach抽象程序和具体程序的程序点如图 5所示, 图 5中的抽象程序点Ai对应具体程序点Ci.

在给出程序点对用关系之后, 本文的方法可以在具体程序上生成验证义务 (目前, 通过手动方式在具体程序上生成验证义务).因为抽象程序和具体程序的映射很细, 因此这里可以完全应用简化证明义务规则.图 7给出了reach具体程序上的验证义务, 为了简化表示, 图 7使用v'表示M(v), M(v) 表示抽象变量v对应的具体变量表达式.

在具体程序上生成验证义务后, 可以使用证明工具证明这些性质.因为生成了细粒度的验证义务, 所以证明这些验证义务是较为容易的.具体程序上验证义务的详细证明过程, 可以参考我们的工具网址:http://seg.nju.edu.cn/scl/download.html.

5.2 Schorre-Waite程序

图 6(a)展示了一般的垃圾回收算法, 它使用深度优先遍历 (DFS) 搜索, 使用一个栈记录当前访问路径.图 6(b)展示了Schorr-Waite算法, 它不使用栈, 仅使用图本身的指针实现回溯.表 5给出了Schorre-Waite抽象程序和具体程序的变量对应关系, 其中, NS0表示节点图中所有节点引用的集合.

STACK定义如下:

STACK(x:P(Node)):List(P(Node))$ \triangleq $x=NULL?[]:x+STACK(x→chk?x→r:x→l).

具体变量数据结构内的不变式为

$ IsRotateList(p) \wedge \mathop \wedge \limits_{x \in STACK(p)} (x \to mk). $

IsRotateList定义如下:

IsRotateList(x:P(Node)):bool$ \triangleq $(x=NULL)?true:x+IsRotateList(x→chk?x→r:x→l).

图 8给出了Schorre-Waite具体程序上的验证义务 (目前是通过手动方式在具体程序上生成验证义务).需要指出的是:图 8中的验证义务只是关于explored, stack, CHK, parent变量的验证义务, 没有关于L, R变量的验证义务.如果一致性标准C中的规约是关于explored, stack, CHK, parent变量的性质 (不包括L, R变量的性质), 那么图 8的验证义务可以证明Schorre-Waite程序是抽象DFS垃圾回收算法关于C的一致性实现.图 8使用INV表示具体变量数据结构不变式.

附录描述了Schorre-Waite大概的证明过程.具体程序上验证义务的详细证明过程, 可以参考我们的工具网址:http://seg.nju.edu.cn/scl/download.html.

6 相关工作和讨论 6.1 精化

精化演算 (refinement calculus) 方法广泛被研究^[15-18], 精化方法分为操作精化 (operation refinement) 和数据精化 (data refinement).

·操作精化是指在不改变规约的前提下, 从抽象操作推导更加具体的操作.它也被称为算法设计 (algorithm design);

·数据精化^[19-25]是指使用具体数据表示替换抽象数据表示.假设a是一组抽象变量 (abstract), c是一组具体变量 (concrete), I是公式, 称作连接不变式.程序progA通过a, c, I数据精化到progC当且仅当对所有的不包含c的后置条件A, 有:

(∃a.I∧wp(progA, A))⇒wp(progC, ∃a.I∧A).

本文的方法借鉴了精化的思想, 但并非用于证明精化关系, 而是用于证明一致性关系.本文的方法通过程序点之间的映射分解来证明.

6.2 程序验证

程序员首先给出待验证程序, 并使用前置条件 (pre-condition)、后置条件 (post-condition)、断言 (assertion) 和不变式 (invariant) 标记程序.这些标记 (annotation) 不仅有软件规约 (specification), 而且包含不变式, 这些不变式分解标记程序成为不含循环的Hoare三元组 (Hoare triples).最终, 利用程序语言的语义, 将程序验证 (program verification) 规约成推导逻辑公式是否正确, 这可以使用定理证明器进行推导.工具Bedrock^[2], VCC^[26], AFNY^[27], HAVOC^[28], VeriFast^[1], jStar^[29]和Smallfoot^[30]等都属于这一类框架.其中一些工具虽然能够减轻程序证明负担, 比如Bedrock支持接近自动化 (mostly-automated) 的程序证明^[2], 但它需要用户给出准确的辅助定理 (low-level lemmas) 和证明策略 (proof tactics) 来指导验证, 需要用户提供合适的循环不变 (loop invariant) 来处理循环语句. Cao^[11]开发了针对单链表的特殊策略, 从而可以接近自动化的处理单链表程序.但是, 当处理非单链表程序时, 仍然需要用户给出准确的辅助定理和合适的证明策略和不变式.相比这些方法, 本文的方法通过分层将证明负担解耦到两个部分:首先证明抽象程序, 然后证明具体程序是抽象程序的一致性实现.抽象程序抽离了实现细节, 比如没有指针, 证明相对容易.抽象程序和具体程序的一致性证明可以被分解, 分解后的证明相对容易, 甚至可能自动化.

本文的方法使用scope logic^[13]作为后端logic工具.Scope logic是Hoare logic的扩展, 它可以处理指针程序.它的主要观察是可以语法构造出表达式e的值依赖的内存单元集合, 这个内存单元集合称为表达式e的memory scope.Scope logic支持local reasoning, 支持程序点指定 (program-point-specific) 表达式e@i.e@i表示表达式e在程序点i处的值.

7 结束语

本文提出了一个证明复杂具体程序的框架:首先证明抽象程序满足规约, 然后证明具体程序和抽象程序满足一致性.这种分层次证明可以简化证明难度.本文具体介绍了证明抽象程序和具体程序满足一致性的方法.抽象程序和具体程序的一致性证明可以分解, 分解后往往变成对抽象数据类型的操作, 从而容易证明并可能自动证明.