PAR平台中若干软件构件形式化验证技术研究

胡启敏,薛锦云 ,游 珍,程 着

(1.江西师范大学国家网络化支撑软件国际科技合作基地，江西 南昌 330022;2.江西省高性能计算技术重点实验室，江西 南昌 330022)

1 引言

PAR平台[1 - 4]是本研究团队在十多项国家级项目连续资助下，历经二十多年潜心研究，最终研制成功的支撑软件形式化和自动化开发的软件平台。PAR平台的功能规约建模语言、抽象程序建模语言、软件构件的设计充分体现了功能抽象和数据抽象的优越性，使得软件开发变得便捷和可靠。利用PAR方法和PAR平台，已经成功地形式化开发了诸多极具挑战性的算法问题，包括：图灵奖获得者Knuth提出的二进制小数转十进制小数算法[5,6]、图平面性判定算法[7]、循环置换乘方的线性算法[8]等。

PAR平台设计了丰富的可重用构件，包括“集合”“包”“序列”“树”和“图”等。这些构件是PAR平台能够实现便捷、可靠地开发软件的关键要素。例如：在“集合”和“树”构件支撑下，PAR平台开发树的前序遍历问题仅需4行核心代码；在“集合”和“图”构件支撑下，PAR平台开发图的深度优先遍历问题仅需5行核心代码。在可重用软件构件的支撑下，PAR平台实现了软件开发的简洁性、便捷性和可靠性。同时，也使得确保软件构件自身的正确性显得尤为重要。

形式化验证指验证已有的系统(程序)是否满足其规约的要求。常见的形式化验证方法主要分两类：演绎验证(Deductive Verification)和模型检测(Model Checking)。演绎验证基于定理证明的基本思想，采用逻辑公式描述系统及其性质，通过一些公理或推理规则来证明系统具有某些性质。演绎验证的过程一般需要通过定理证明器完成，它可以使用归纳的方法来处理无限状态的问题。

目前，支持演绎验证的定理证明工具有：法国国家信息与自动化研究院(INRIA)开发的Coq[9,10]、英国剑桥大学和德国慕尼黑大学开发的Isabelle[11]和美国康奈尔大学开发的Nuprl等。Coq 中的归纳类型扩展了传统程序设计语言中有关类型定义的概念，融合递归类型和依赖积，具有很强的抽象能力和表达能力。相比之下，Isabelle等定理证明器表达能力较弱。

本文利用公理语义学中的Hoare公理系统，给出PAR平台中若干可重用构件的形式语义；精确描述构件向外提供操作的功能。然后，通过形式化推导和循环不变式开发新技术，得到软件构件相关操作所对应的循环不变式和实现程序。进而根据定理证明工具Coq抽象表示能力强等显著特点，利用它提供的归纳类型、依赖积等机制，形式化地刻画可重用构件实现程序以及相关循环不变式的属性，对这些属性能否满足前后置断言进行机械的、严格的推导和证明，从而验证软件构件的正确性。

2 基础知识

2.1 PAR方法和PAR平台

形式化方法PAR方法及其支撑平台PAR平台由功能规约和算法建模语言Radl(Recur-based algorithm design language)、泛型抽象程序建模语言Apla(Abstract programming language)、以及Radl模型到Apla模型自动生成系统、Apla模型到JAVA、C++、C#等可执行语言模型自动生成系统组成。

Radl语言用人们惯用的数学符号和书写方式来描述算法规约、规约变换规则和算法。Radl作为Apla语言的前端语言，具有数学引用透明性。使用统一的格式(Qi:r(i):f(i))表示“在范围r(i) 上，对函数f(i)施行q运算所得的量”，其中Q是q运算的一般化，可以是全称量词∀、存在量词∃、求最小值量词MIN、求最大值量词MAX、求和量词∑、求积量词Π等，分别对应着的q运算是∧、∨、min、max、+、×等。利用这些量词的性质可以进行规约变换。

Apla是Radl算法—Apla程序转换器的目标语言，又是Apla到Dephi、Java、C++等可执行语言程序转换器的源语言。设计Apla的主要宗旨是充分体现数据抽象、功能抽象、泛型等现代程序设计思想，使得构成的程序易于阅读理解和验证。

Apla的一个重要特色是它的泛型可重用构件库，包括“集合”“包”“序列”“树”和“图”等。这些可重用构件库的定义和实现，是课题组长期推导和证明各类程序的经验总结，充分考虑了构件的简洁性和通用性。例如：基于“序列”可重用构件，就可以便捷地构造队列、堆栈等。

2.2 定理证明器Coq

Coq是法国INRIA研究院开发的一种基于高阶逻辑的交互式定理证明工具，它使用规约语言Gallina表示程序、程序的属性和这些属性的证明。Coq系统主要由两部分组成：证明开发系统和证明检查器。证明开发系统类似于程序开发系统，拥有声明模式和证明模式。在声明模式里，程序员可以像设计程序一样声明变量、假设、公理；在证明模式里，程序员可以如同编写程序一样利用已声明的对象和系统提供的证明策略构造引理或定理。证明检查器用以验证被形式化表示的程序，其核心是类型检查算法，此算法通过检查程序是否满足程序规范来判定证明是否成立。

基于Coq形式化验证程序的过程一般分为标注阶段、形式化阶段和证明阶段。其中，标注阶段完成对程序的前后置断言、循环不变式、要证明的程序属性的描述。形式化阶段在Coq系统中采用形式化的方法完成对程序、标注的相关定义。证明阶段根据形式化的程序、标注来抽取关于程序满足相关属性的定理，然后在Coq系统中对定理进行证明。

本文利用研究团队在复杂算法程序形式化推导、求解问题的递推关系式构造、循环不变式开发新技术等方面取得的研究成果，结合Hoare公理体系、Dijkstra最弱前置谓词方法和Coq系统的自身特点，将基于Coq形式化验证程序分为以下5个步骤：

(1)给出程序的形式化语义，即：给出程序前后置断言的精确描述。

(2)从程序前后置断言出发，进行形式化推导，找出程序求解的递推关系式，并利用该递推关系式和循环不变式开发新技术构造循环不变式ρ和具体实现程序。

(3)使用Coq系统的Gallina语言和归纳类型、递归类型和依赖积等机制，定义相关数据类型、数据结构以及相关函数；用Gallina语言描述第(2)步得到的循环不变式。

(4)给出程序应满足相关属性的定理，并用Gallina语言描述。如果用S表示程序语句，谓词公式Q、R表示程序的前置和后置断言，从S和R定义最弱前置谓词WP(‘S’,R)。程序应满足的定理即：Q→(WP(‘S’,R)。

如果程序中有循环语句，则要把Dijkstra最弱前置谓词法中证明循环语句的五个蕴含表达式分别描述成Coq能够识别的五个定理，如下所示：

Theoremwp1:Q→ρ//程序循环开始前ρ为真

Theoremwp2:ρ∧Ci→wp(‘Si’,ρ)/*每一次循环，ρ为真*/

Theoremwp3:ρ∧┐Guard→R//循环结束时，R为真

Theoremwp4:ρ∧Guard→τ> 0/*循环没结束时，界函数大于0*/

Theoremwp5:ρ∧Ci→wp(‘τ1:=τ;Si’,τ<τ1)/*每一次循环，界函数的值减少*/

(5)利用Coq系统提供的证明规则和第(3)步定义的数据类型、数据结构和相关函数，证明第(4)步的定理。

3 “集合”构件的形式语义与验证

无重复元素的一组同类型数据构成集合。集合构件可以通过数组或链表实现。用数组实现的集合，元素个数受限制，称为有限集合；用链表实现的集合，元素个数无限制，称为无限集合。

3.1 “集合”构件的形式语义

程序的形式语义主要有操作语义、指称语义、代数语义、公理语义等4种。为便于验证，本节给出构件各操作的公理语义；操作语义等限于篇幅，此处省略。 “集合”构件各个操作的公理语义如下(其中，前后置断言采用Radl语言书写，“集合”构件各操作的实现程序是否满足前后置断言，将在3.2节进行验证)：

Type ADTset(elem:T,[SIZE:integer])

/*T表示集合元素是泛型的，可以是整型、字符型等。SIZE是可选项，如果有SIZE，指集合元素的个数不超过SIZE，该集合用数组实现。如果缺省SIZE，指集合元素没有限制，该集合需要用链表实现。下文重点讨论有限集合*/

Invariant: 0≤length≤SIZE;

Initially:set=nullset;

VarS:set,length:integer;

Operations:

Oneitemset(elem:T)/*Oneitemset操作可建立仅含一个元素的集合，’S表示操作执行后，集合对应的状态，S[0]表示集合的首元素*/

Pre True

Post ‘S.length=1∧’S[0]=elem

Intersection(R:set) return(‘S:set)/*Intersection操作计算集合S与集合R的交集*/

Pre 0≤R.length

Post (∀k:0≤k≤’S.length-1:‘S[k]∈S∧‘S[k]∈R)

Union(R:set) return(‘S:set)/*Union操作计算集合S与集合R的并集*/

Pre 0≤S.length+R.length

Post (∀k: 0≤k≤’S.length-1: ‘S[k]∈S∨‘S[k]∈R)

Sub(R:set) return(‘S:set)/*Sub操作用于在集合S中去除在集合R中出现的元素*/

Pre 0≤R.length

Post (∀k:0≤k≤’S.length-1: ‘S[k]∈S∧‘S[k] ∉R)

Involve(elem:T)return(flag:Boolean)/*Involve操作用于判断elem是否属于集合S*/

PreTrue

Post(flag=true∧(∃: 0≤k≤S.length-1: S[k]=elem) ∨(flag=false)

Include(R:set) return(flag:Boolean)/*Include操作用于判断S是否是R的子集*/

PreS.length

Post (flag=true∧(∀k: 0≤k≤S.length-1:S[k]∈R)) ∨(flag=false)

Equal(R:set) return(flag:Boolean)/*Equal操作用于判断集合S与集合R是否相等*/

Pre 0≤R.length

Post (flag=true∧S.length=R.length∧(∀k:0≤k≤S.length-1:S[k]∈R))∨(flag=false)

Copy(R:set)/*Copy操作用于将集合R替换为集合S*/

Pre 0≤R.length

Post ‘S.length=R.length∧(∀k: 0≤k≤’S.length-1: ’S[k]=R[k])

3.2 “集合”构件的形式化验证

“集合”构件提供了“求并集”“求交集”等7个操作。选取“集合”的判断两个集合是否存在子集关系的Include操作进行验证。

(1)给出该操作的前后置断言。

根据上文给出的Include操作的前后置断言，假设集合S含m+1个元素，集合R含n+1个元素，可将后置断言写为：

Include(S[0..m],R[0..n]) ≡(i:0≤i≤m:(彐j:0≤j≤n:R[j]=S[i]))

(2)从程序后置断言出发，进行形式化推导，找出程序求解的递推关系式，构造循环不变式和求解程序。

利用量词变换规则，作如下形式化推导，得出求解该操作的递推关系式：

Include(S[0..m],R[0..n])

≡(i:0≤i≤m:(彐j:0≤j≤n:S[i]=R[j]))

{范围分裂}

≡(i:0≤i≤m-1:(彐j:0≤j≤n:S[i]=R[j]))∧

(i:0≤i=m:(彐j:0≤j≤n:S[i]=R[j]))

{单点范围}

≡(i:0≤i≤m-1:(彐j:0≤j≤n:S[i]=R[j]))∧

(彐j:0≤j≤n:S[m]=R[j])

{Include的定义}

≡Include(S[0..m-1],R[0..n])∧(彐j:0≤j≤n:S[m]=R[j])

用布尔类型变量flag表示Include(S[0..i],R[0..n]) 的值，即可得到循环不变式:

ρ：flag=Include(S[0..i],R[0..n]) ∧0≤i≤m

根据递推关系和循环不变式，可得该操作的求解程序为：

i:=0;flag:=true;

WHILEi

BEGIN

IF notInvole(S[i],R[0..n])

THENflag:=false;RETURN

ELSEi:=i+1;

END.

(3)定义相关数据类型、数据结构以及相关函数。

利用Coq提供的归纳类型、递归和依赖积等抽象机制，定义Involve，Include如下：

FixpointInvolve(x:z,S:set):bool:=MatchSwith

|nil⟹false

|consyq⟹ifx=ythen true elseInvolvexq

FixpointInclude(S:set,R:set):bool:=MatchSwith

|nil⟹true

|consyq⟹ifInvolveyRthenIncludeqRelse false

同时，分别定义取集合S的第n个元素，和取集合S中前j个元素组成的子集如下：

Fixpointnth(n:z,S:set):z=matchSwith

|nil⟹default

|x::r⟹ matchnwith

|0⟹x

|Sm⟹nthmrdefault

end.

end.

Fixpointupto(j:z,S:set):set =matchjwith

|0⟹ matchswith

|nil⟹nil

|a::l⟹a::nil end

|Sn⟹ matchswith

|nil⟹nil

|a::l⟹a::(firstnnl) end

end.

(4)给出程序应满足相关属性的定理。

利用上面定义的归纳类型和函数，证明循环不变式在每次循环执行前后均为真，如下所示：

首先给出首次执行循环，循环不变式为真的定理：

Theormwp1:

i=0∧Include(upto(0,S),R)

→Include(upto(i,S),R) ∧0≤i∧i

然后给出每次循环，循环不变式均为真的定理:

Theormwp2.1:

Include(upto(i,S),R)∧0≤i∧i

→Include(upto(suci,S),R) ∧0≤suci∧suci≤m

Theormwp2.2:

Include(upto(i,S),R)∧0≤i∧i

→negbInclude(upto(suci,S),R) ∧0≤i∧i

再给出当循环终止时，后置断言为真的定理:

Theormwp3:

Include(upto(i,S),R) ∧0≤i∧i

→Include(upto(m-1,S),R)

循环的终止性证明的定理较为简单，此处略。

(5)证明相关定理。

以上定理都可以在定理证明工具Coq中，使用“Induction”“Apply auto”等规则进行求证。

4 “包”构件的形式语义与验证

允许重复元素的一组同类型数据构成包。包构件可以通过数组或链表实现。用数组实现的包，元素个数有限制，称为有限包，用链表实现的包，元素个数无限制，称为无限包。

4.1 “包”构件的形式语义

“包”的形式语义类似于集合，但由于“包”允许有重复元素，所以“包”的大部分操作规范不同于“集合”。给出“包”的公理语义如下：

Type ADTbag(elem:T,[SIZE:integer])

/*T表示包元素是泛型的，可以是整型、字符型等。SIZE是可选项，如果有SIZE，指包中元素的个数不超过SIZE，该包用数组实现。如果缺省SIZE，指包中元素没有限制，该包需要用链表实现。下文重点讨论有限包*/

Invariant: 0≤length≤SIZE;

Initially:bag=nullbag;

VarS:bag,length:integer;

Operations:

Oneitembag(elem:T)/*Oneitembag操作可建立仅含一个元素的包，’S表示操作执行后，包对应的状态，S[0]表示包的首元素*/

Pre True

Post ‘S.length=1∧’S[0]=elem

Intersection(R:bag) return(‘S:bag)/*Intersection操作计算包S与包R的交集*/

Pre 0≤R.length

Post (∀k:0≤k≤’S.length-1: ‘S[k]∈S∧‘S[k]∈R)

Union(R:bag) return(‘S:bag)/*Union操作计算包S与包R的并集，其中谓词occ(x,S)表示x在包S中出现的次数*/

Pre 0≤S.length+R.length

Post ‘S.lengh=S.length+R.length∧

(∀k: 0≤k≤’S.length-1:occ(‘S[k],’S)=occ(‘S[k],S)+occ(‘S[k],R))

Sub(R: bag)return(‘S: bag)/*Sub操作用于在包S中去除在包R中出现的元素*/

Pre0≤R.length

Post(∀k:0≤k≤’S.length-1: ‘S[k]∈S∧‘S[k]∉∈R)

Involve(elem:T) return(flag:Boolean)/*Involve操作用于判断elem是否属于包S*/

Pre True

Post (flag=true∧(∃k: 0≤k≤S.length-1:S[k]=elem) ∨(flag=false)

Include(R:bag) return(flag:Boolean)/*Include操作用于判断包S是否是R的子集，其中谓词occ(x,S)表示x在包S中出现的次数*/

PreS.length

Post (flag=true∧(∀k: 0≤k≤S.length-1:occ(S[k],S)≤occ(S[k],R)))∨(flag=false)

Equal(R:bag) return(flag:Boolean)/*Equal操作用于判断包S与R是否相等，其中谓词occ(x,S)表示x在包S中出现的次数*/

Pre 0≤R.length

Post (flag=true∧S.length=R.length∧

(∀k:0≤k≤S.length-1:occ(S[k],S)=occ(S[k],R))∨(flag=false))

Copy(R:bag)//Copy操作用于将包R替换为S

Pre 0≤R.length

Post ‘S.length=R.length∧(∀k: 0≤k≤’S.length-1: ’S[k]=R[k])

4.2 “包”构件的形式化验证

“包”构件提供了“求包的并集”“求包的交集”等7个操作。选取“包”的判断两个“包”是否存在子集关系的Include操作进行验证。

(1)给出该操作的前后置断言。

根据上文给出的Include操作的前后置断言，假设包S含m+1个元素，包R含n+1个元素，occ(x,S)表示x在包S中出现的次数，可将后置断言形式写为：

Include(S[0..m],R[0..n]) ≡

∀(i: 0≤i≤S.length-1:occ(S[i],S)≤occ(S[i],R))

(2)从程序前后置断言出发，进行形式化推导，找出程序求解的递推关系式，构造循环不变式和求解程序。

利用量词变换规则，作如下形式化推导，得出求解该操作的递推关系式：

Include(S[0..m],R[0..n])

≡(i:0≤i≤m:occ(S[i],S)≤occ(S[i],R))

{范围分裂}

≡(i:0≤i≤m-1:occ(S[i],S)≤occ(S[i],R) ∧

(i:0≤i=m:occ(S[i],S)≤occ(S[i],R))

{单点范围}

≡(i:0≤i≤m-1:occ(S[i],S)≤occ(S[i],R)∧

occ(S[m],S)≤occ(S[m],R))

{Include的定义}

≡Include(S[0..m-1],R[0..n])∧occ(S[m],S)≤occ(S[m],R)

用布尔类型变量flag表示Include(S[0..i],R[0..n]) 的值，即可得到循环不变式:

ρ：flag=Include(S[0..i],R[0..n]) ∧0≤i≤m

根据递推关系和循环不变式，可得该操作的求解程序为：

i:=0;flag:=true;

WHILEi

BEGIN

IF notocc(S[i],S)≤occ(S[i],R)

THEN flag:=false;RETURN

ELSEi:=i+1;

END.

(3)定义相关数据类型、数据结构以及相关函数。

定义归纳类型Occ，Include如下：

FixpointOcc(x:z,s:bag):z:=Matchswith

|nil⟹0

|consyq⟹letn:=Occ(x,q) in

Ifeq_decyxthenn+1 elsen.

FixpointInclude(S:bag,R:bag):bool:=MatchSwith

|nil⟹true

|consyq⟹Occ(y,S)≤Occ(y,R)∧IncludeqR

(4)给出程序应满足相关属性的定理。

首先给出首次执行循环，循环不变式为真的定理：

Theormwp1:

i=0∧Include(upto(0,S),R)

→Include(upto(i,S),R) ∧0≤i∧i

然后给出每次循环，循环不变式均为真的定理:

Theormwp2.1:

Include(upto(i,S),R)∧0≤i∧i

→Include(upto(suci,S),R) ∧0≤suci∧suci≤m

Theormwp2.2:

Include(upto(i,S),R) ∧0≤i∧i

→negbInclude(upto(suci,S),R) ∧0≤i∧i

再给出当循环终止时，后置断言为真的定理:

Theormwp3:

Include(upto(i,S),R) ∧0≤i∧i

→Include(upto(m-1,S),R)

循环的终止性证明的定理较为简单，此处略。

(5)证明相关定理。

以上定理都可以在定理证明工具Coq中，使用“Induction”“Apply auto”等规则进行求证。

5 相关研究工作

文献[12，13]在Coq 中利用一阶语法对C语言的语法进行描述，并基于归纳谓词对C语言、中间语言以及目标语言的操作语义进行机械化。文献[14]中提出了如何在Coq 中对内存模型和并行编译的正确性进行证明。该编译器的源语言为并行的Clight，目标语言为并行的x86 汇编语言。Ynot是Coq 的一个扩展库，实现了分离逻辑。基于Coq 和Ynot，文献[15]中实现了一个轻量级的、完全经过验证的关系型数据库管理系统(RDBMS)，RDBMS 的功能规范、具体实现以及该实现满足规范要求的证明，都在Coq 中进行了书写和验证。文献[16]将CompCert 项目的正确性验证理念运用在硬件综合设计上，为Fe-Si(Bluespec的简化版)的高级硬件描述语言实现了一个验证编译器。

上述验证工作主要集中在语义机械化、编译过程验证、关系数据库和硬件系统验证上。本文结合Coq系统特点和团队在循环不变式方面的开发新技术，程序形式化推导上的技术优势，强调循环不变式在形式化验证中所起的关键作用，将基于Coq的形式化验证过程分为5个主要步骤，并验证了PAR平台若干典型软件构件的正确性。

6 结束语

PAR平台中的可重用软件构件是PAR平台体现功能抽象和数据抽象特性，实现便捷、可靠开发软件的关键因素。因此，这些软件构件自身的正确性和可靠性显得尤为重要。

本文利用Hoare公理系统对软件构件进行形式化描述，给出了精确的语义。进而，利用定理证明器Coq提供的归纳类型等抽象表示机制刻画软件构件实现程序和对应循环不变式的属性，利用Coq提供的命题演算、谓词演算功能机械地证明实现程序是否满足前后置断言，从而实现形式化验证软件构件正确性的目标。

将在此工作基础上，进一步探索如何给出PAR平台Radl语言、Apla语言的完整语义，如何形式化刻画Apla抽象程序到C++、Java等可执行程序自动生成系统的主要功能，进而利用Coq工具，形式化验证PAR平台程序自动生成系统关键功能的正确性。

[1] Xue J.A unified approach for developing efficient algorithmic programs[J].Journal of Computer Science and Technology,1997,12(4):314-329.

[2] Xue J.Two new strategies for developing loop invariants and their applications[J].Journal of Computer Science and Technology,1993,8(2):147-154.

[3] Xue Jin-yun. A practicable approach for formal development of algorithmic programs[C]∥Proc of the International Symposium on Future Software Technology,1999: 158-160.

[4] Xue Jin-yun.PAR method and its supporting platform [C]∥Proc of the 1st International Workshop on Asian Working Conference on Verified Software,2006:159-169.

[5] Xue J,Davis R.A derivation and proof of Knuth’ binary to decemal program[J].Software Concepts & Tools,1997,18(4):149-156.

[6] Xue J,Davis R.A simple program whose derivation and proof is also[C]∥Proc of the 1st IEEE International Conference on Formal Engineering Method(ICFEM’97),1997:1.

[7] Gries D, Xue Jin-yun. The hopcroft-tarjan planarity algorithm presentations and improvements:TR88-906[R].New York:Department of Computer Science, Cornell University,1998.

[8] Xue Jin-yun,David G.Developing a linear algorithm for cubing a cycle permutation[J].Science of Computer Programming,1998,11:161-165.

[9] The Coq proof assistant[EB/OL].[2014-01-01].http: ∥coq.inria.fr/.

[10] Bertot Y， Castéran P． Interactive theorem proving and program development-Coq’Art: The calculus of inductive constructions[M]．London,UK: Springer，2004．

[11] Nipkow T, Paulson L C, Wenzel M． Isabelle /HOL: A proof assistant for higher-order logic[M].London,UK: Springer,2002．

[12] Lero X.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115．

[13] Boldo S,Jourdan J-H,Leroy X,et al.A formally verified C compiler supporting floating-point arithmetic[C]∥Proc of the 21st IEEE International Symposium on Computer Arithmetic,2013: 107-115.

[14] Evcik J, Vafeiadis V, Nardelli F Z,et al.Relaxed-memory concurrency and verified compilation[C]∥Proc of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,2011: 43-54．

[15] Malecha G, Morrisett G, Shinnar A,et al.Toward a verified relational database management system[C]∥Proc of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,2010: 237-248.

[16] Braibant T,Chlipala A.Formal verification of hardware synthesis[C]∥/Proc of the 25th International Conference on Computer Aided Verification,2013:213-228.