PAR平臺(tái)中若干軟件構(gòu)件形式化驗(yàn)證技術(shù)研究

胡啟敏,薛錦云 ,游 珍,程 著

(1.江西師范大學(xué)國(guó)家網(wǎng)絡(luò)化支撐軟件國(guó)際科技合作基地，江西 南昌 330022;2.江西省高性能計(jì)算技術(shù)重點(diǎn)實(shí)驗(yàn)室，江西 南昌 330022)

1 引言

PAR平臺(tái)[1 - 4]是本研究團(tuán)隊(duì)在十多項(xiàng)國(guó)家級(jí)項(xiàng)目連續(xù)資助下，歷經(jīng)二十多年潛心研究，最終研制成功的支撐軟件形式化和自動(dòng)化開(kāi)發(fā)的軟件平臺(tái)。PAR平臺(tái)的功能規(guī)約建模語(yǔ)言、抽象程序建模語(yǔ)言、軟件構(gòu)件的設(shè)計(jì)充分體現(xiàn)了功能抽象和數(shù)據(jù)抽象的優(yōu)越性，使得軟件開(kāi)發(fā)變得便捷和可靠。利用PAR方法和PAR平臺(tái)，已經(jīng)成功地形式化開(kāi)發(fā)了諸多極具挑戰(zhàn)性的算法問(wèn)題，包括：圖靈獎(jiǎng)獲得者Knuth提出的二進(jìn)制小數(shù)轉(zhuǎn)十進(jìn)制小數(shù)算法[5,6]、圖平面性判定算法[7]、循環(huán)置換乘方的線性算法[8]等。

PAR平臺(tái)設(shè)計(jì)了豐富的可重用構(gòu)件，包括“集合”“包”“序列”“樹(shù)”和“圖”等。這些構(gòu)件是PAR平臺(tái)能夠?qū)崿F(xiàn)便捷、可靠地開(kāi)發(fā)軟件的關(guān)鍵要素。例如：在“集合”和“樹(shù)”構(gòu)件支撐下，PAR平臺(tái)開(kāi)發(fā)樹(shù)的前序遍歷問(wèn)題僅需4行核心代碼；在“集合”和“圖”構(gòu)件支撐下，PAR平臺(tái)開(kāi)發(fā)圖的深度優(yōu)先遍歷問(wèn)題僅需5行核心代碼。在可重用軟件構(gòu)件的支撐下，PAR平臺(tái)實(shí)現(xiàn)了軟件開(kāi)發(fā)的簡(jiǎn)潔性、便捷性和可靠性。同時(shí)，也使得確保軟件構(gòu)件自身的正確性顯得尤為重要。

形式化驗(yàn)證指驗(yàn)證已有的系統(tǒng)(程序)是否滿足其規(guī)約的要求。常見(jiàn)的形式化驗(yàn)證方法主要分兩類：演繹驗(yàn)證(Deductive Verification)和模型檢測(cè)(Model Checking)。演繹驗(yàn)證基于定理證明的基本思想，采用邏輯公式描述系統(tǒng)及其性質(zhì)，通過(guò)一些公理或推理規(guī)則來(lái)證明系統(tǒng)具有某些性質(zhì)。演繹驗(yàn)證的過(guò)程一般需要通過(guò)定理證明器完成，它可以使用歸納的方法來(lái)處理無(wú)限狀態(tài)的問(wèn)題。

目前，支持演繹驗(yàn)證的定理證明工具有：法國(guó)國(guó)家信息與自動(dòng)化研究院(INRIA)開(kāi)發(fā)的Coq[9,10]、英國(guó)劍橋大學(xué)和德國(guó)慕尼黑大學(xué)開(kāi)發(fā)的Isabelle[11]和美國(guó)康奈爾大學(xué)開(kāi)發(fā)的Nuprl等。Coq 中的歸納類型擴(kuò)展了傳統(tǒng)程序設(shè)計(jì)語(yǔ)言中有關(guān)類型定義的概念，融合遞歸類型和依賴積，具有很強(qiáng)的抽象能力和表達(dá)能力。相比之下，Isabelle等定理證明器表達(dá)能力較弱。

本文利用公理語(yǔ)義學(xué)中的Hoare公理系統(tǒng)，給出PAR平臺(tái)中若干可重用構(gòu)件的形式語(yǔ)義；精確描述構(gòu)件向外提供操作的功能。然后，通過(guò)形式化推導(dǎo)和循環(huán)不變式開(kāi)發(fā)新技術(shù)，得到軟件構(gòu)件相關(guān)操作所對(duì)應(yīng)的循環(huán)不變式和實(shí)現(xiàn)程序。進(jìn)而根據(jù)定理證明工具Coq抽象表示能力強(qiáng)等顯著特點(diǎn)，利用它提供的歸納類型、依賴積等機(jī)制，形式化地刻畫(huà)可重用構(gòu)件實(shí)現(xiàn)程序以及相關(guān)循環(huán)不變式的屬性，對(duì)這些屬性能否滿足前后置斷言進(jìn)行機(jī)械的、嚴(yán)格的推導(dǎo)和證明，從而驗(yàn)證軟件構(gòu)件的正確性。

2 基礎(chǔ)知識(shí)

2.1 PAR方法和PAR平臺(tái)

形式化方法PAR方法及其支撐平臺(tái)PAR平臺(tái)由功能規(guī)約和算法建模語(yǔ)言Radl(Recur-based algorithm design language)、泛型抽象程序建模語(yǔ)言Apla(Abstract programming language)、以及Radl模型到Apla模型自動(dòng)生成系統(tǒng)、Apla模型到JAVA、C++、C#等可執(zhí)行語(yǔ)言模型自動(dòng)生成系統(tǒng)組成。

Radl語(yǔ)言用人們慣用的數(shù)學(xué)符號(hào)和書(shū)寫(xiě)方式來(lái)描述算法規(guī)約、規(guī)約變換規(guī)則和算法。Radl作為Apla語(yǔ)言的前端語(yǔ)言，具有數(shù)學(xué)引用透明性。使用統(tǒng)一的格式(Qi:r(i):f(i))表示“在范圍r(i) 上，對(duì)函數(shù)f(i)施行q運(yùn)算所得的量”，其中Q是q運(yùn)算的一般化，可以是全稱量詞?、存在量詞?、求最小值量詞MIN、求最大值量詞MAX、求和量詞∑、求積量詞Π等，分別對(duì)應(yīng)著的q運(yùn)算是∧、∨、min、max、+、×等。利用這些量詞的性質(zhì)可以進(jìn)行規(guī)約變換。

Apla是Radl算法—Apla程序轉(zhuǎn)換器的目標(biāo)語(yǔ)言，又是Apla到Dephi、Java、C++等可執(zhí)行語(yǔ)言程序轉(zhuǎn)換器的源語(yǔ)言。設(shè)計(jì)Apla的主要宗旨是充分體現(xiàn)數(shù)據(jù)抽象、功能抽象、泛型等現(xiàn)代程序設(shè)計(jì)思想，使得構(gòu)成的程序易于閱讀理解和驗(yàn)證。

Apla的一個(gè)重要特色是它的泛型可重用構(gòu)件庫(kù)，包括“集合”“包”“序列”“樹(shù)”和“圖”等。這些可重用構(gòu)件庫(kù)的定義和實(shí)現(xiàn)，是課題組長(zhǎng)期推導(dǎo)和證明各類程序的經(jīng)驗(yàn)總結(jié)，充分考慮了構(gòu)件的簡(jiǎn)潔性和通用性。例如：基于“序列”可重用構(gòu)件，就可以便捷地構(gòu)造隊(duì)列、堆棧等。

2.2 定理證明器Coq

Coq是法國(guó)INRIA研究院開(kāi)發(fā)的一種基于高階邏輯的交互式定理證明工具，它使用規(guī)約語(yǔ)言Gallina表示程序、程序的屬性和這些屬性的證明。Coq系統(tǒng)主要由兩部分組成：證明開(kāi)發(fā)系統(tǒng)和證明檢查器。證明開(kāi)發(fā)系統(tǒng)類似于程序開(kāi)發(fā)系統(tǒng)，擁有聲明模式和證明模式。在聲明模式里，程序員可以像設(shè)計(jì)程序一樣聲明變量、假設(shè)、公理；在證明模式里，程序員可以如同編寫(xiě)程序一樣利用已聲明的對(duì)象和系統(tǒng)提供的證明策略構(gòu)造引理或定理。證明檢查器用以驗(yàn)證被形式化表示的程序，其核心是類型檢查算法，此算法通過(guò)檢查程序是否滿足程序規(guī)范來(lái)判定證明是否成立。

基于Coq形式化驗(yàn)證程序的過(guò)程一般分為標(biāo)注階段、形式化階段和證明階段。其中，標(biāo)注階段完成對(duì)程序的前后置斷言、循環(huán)不變式、要證明的程序?qū)傩缘拿枋觥Ｐ问交A段在Coq系統(tǒng)中采用形式化的方法完成對(duì)程序、標(biāo)注的相關(guān)定義。證明階段根據(jù)形式化的程序、標(biāo)注來(lái)抽取關(guān)于程序滿足相關(guān)屬性的定理，然后在Coq系統(tǒng)中對(duì)定理進(jìn)行證明。

本文利用研究團(tuán)隊(duì)在復(fù)雜算法程序形式化推導(dǎo)、求解問(wèn)題的遞推關(guān)系式構(gòu)造、循環(huán)不變式開(kāi)發(fā)新技術(shù)等方面取得的研究成果，結(jié)合Hoare公理體系、Dijkstra最弱前置謂詞方法和Coq系統(tǒng)的自身特點(diǎn)，將基于Coq形式化驗(yàn)證程序分為以下5個(gè)步驟：

(1)給出程序的形式化語(yǔ)義，即：給出程序前后置斷言的精確描述。

(2)從程序前后置斷言出發(fā)，進(jìn)行形式化推導(dǎo)，找出程序求解的遞推關(guān)系式，并利用該遞推關(guān)系式和循環(huán)不變式開(kāi)發(fā)新技術(shù)構(gòu)造循環(huán)不變式ρ和具體實(shí)現(xiàn)程序。

(3)使用Coq系統(tǒng)的Gallina語(yǔ)言和歸納類型、遞歸類型和依賴積等機(jī)制，定義相關(guān)數(shù)據(jù)類型、數(shù)據(jù)結(jié)構(gòu)以及相關(guān)函數(shù)；用Gallina語(yǔ)言描述第(2)步得到的循環(huán)不變式。

(4)給出程序應(yīng)滿足相關(guān)屬性的定理，并用Gallina語(yǔ)言描述。如果用S表示程序語(yǔ)句，謂詞公式Q、R表示程序的前置和后置斷言，從S和R定義最弱前置謂詞WP(‘S’,R)。程序應(yīng)滿足的定理即：Q→(WP(‘S’,R)。

如果程序中有循環(huán)語(yǔ)句，則要把Dijkstra最弱前置謂詞法中證明循環(huán)語(yǔ)句的五個(gè)蘊(yùn)含表達(dá)式分別描述成Coq能夠識(shí)別的五個(gè)定理，如下所示：

Theoremwp1:Q→ρ//程序循環(huán)開(kāi)始前ρ為真

Theoremwp2:ρ∧Ci→wp(‘Si’,ρ)/*每一次循環(huán)，ρ為真*/

Theoremwp3:ρ∧┐Guard→R//循環(huán)結(jié)束時(shí)，R為真

Theoremwp4:ρ∧Guard→τ> 0/*循環(huán)沒(méi)結(jié)束時(shí)，界函數(shù)大于0*/

Theoremwp5:ρ∧Ci→wp(‘τ1:=τ;Si’,τ<τ1)/*每一次循環(huán)，界函數(shù)的值減少*/

(5)利用Coq系統(tǒng)提供的證明規(guī)則和第(3)步定義的數(shù)據(jù)類型、數(shù)據(jù)結(jié)構(gòu)和相關(guān)函數(shù)，證明第(4)步的定理。

3 “集合”構(gòu)件的形式語(yǔ)義與驗(yàn)證

無(wú)重復(fù)元素的一組同類型數(shù)據(jù)構(gòu)成集合。集合構(gòu)件可以通過(guò)數(shù)組或鏈表實(shí)現(xiàn)。用數(shù)組實(shí)現(xiàn)的集合，元素個(gè)數(shù)受限制，稱為有限集合；用鏈表實(shí)現(xiàn)的集合，元素個(gè)數(shù)無(wú)限制，稱為無(wú)限集合。

3.1 “集合”構(gòu)件的形式語(yǔ)義

程序的形式語(yǔ)義主要有操作語(yǔ)義、指稱語(yǔ)義、代數(shù)語(yǔ)義、公理語(yǔ)義等4種。為便于驗(yàn)證，本節(jié)給出構(gòu)件各操作的公理語(yǔ)義；操作語(yǔ)義等限于篇幅，此處省略。 “集合”構(gòu)件各個(gè)操作的公理語(yǔ)義如下(其中，前后置斷言采用Radl語(yǔ)言書(shū)寫(xiě)，“集合”構(gòu)件各操作的實(shí)現(xiàn)程序是否滿足前后置斷言，將在3.2節(jié)進(jìn)行驗(yàn)證)：

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

/*T表示集合元素是泛型的，可以是整型、字符型等。SIZE是可選項(xiàng)，如果有SIZE，指集合元素的個(gè)數(shù)不超過(guò)SIZE，該集合用數(shù)組實(shí)現(xiàn)。如果缺省SIZE，指集合元素沒(méi)有限制，該集合需要用鏈表實(shí)現(xiàn)。下文重點(diǎn)討論有限集合*/

Invariant: 0≤length≤SIZE;

Initially:set=nullset;

VarS:set,length:integer;

Operations:

Oneitemset(elem:T)/*Oneitemset操作可建立僅含一個(gè)元素的集合，’S表示操作執(zhí)行后，集合對(duì)應(yīng)的狀態(tài)，S[0]表示集合的首元素*/

Pre True

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

Intersection(R:set) return(‘S:set)/*Intersection操作計(jì)算集合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操作計(jì)算集合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中出現(xiàn)的元素*/

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 “集合”構(gòu)件的形式化驗(yàn)證

“集合”構(gòu)件提供了“求并集”“求交集”等7個(gè)操作。選取“集合”的判斷兩個(gè)集合是否存在子集關(guān)系的Include操作進(jìn)行驗(yàn)證。

(1)給出該操作的前后置斷言。

根據(jù)上文給出的Include操作的前后置斷言，假設(shè)集合S含m+1個(gè)元素，集合R含n+1個(gè)元素，可將后置斷言寫(xiě)為：

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

(2)從程序后置斷言出發(fā)，進(jìn)行形式化推導(dǎo)，找出程序求解的遞推關(guān)系式，構(gòu)造循環(huán)不變式和求解程序。

利用量詞變換規(guī)則，作如下形式化推導(dǎo)，得出求解該操作的遞推關(guān)系式：

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]))

{單點(diǎn)范圍}

≡(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]) 的值，即可得到循環(huán)不變式:

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

根據(jù)遞推關(guān)系和循環(huán)不變式，可得該操作的求解程序?yàn)椋?/p>

i:=0;flag:=true;

WHILEi

BEGIN

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

THENflag:=false;RETURN

ELSEi:=i+1;

END.

(3)定義相關(guān)數(shù)據(jù)類型、數(shù)據(jù)結(jié)構(gòu)以及相關(guān)函數(shù)。

利用Coq提供的歸納類型、遞歸和依賴積等抽象機(jī)制，定義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

同時(shí)，分別定義取集合S的第n個(gè)元素，和取集合S中前j個(gè)元素組成的子集如下：

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)給出程序應(yīng)滿足相關(guān)屬性的定理。

利用上面定義的歸納類型和函數(shù)，證明循環(huán)不變式在每次循環(huán)執(zhí)行前后均為真，如下所示：

首先給出首次執(zhí)行循環(huán)，循環(huán)不變式為真的定理：

Theormwp1:

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

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

然后給出每次循環(huán)，循環(huán)不變式均為真的定理:

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

再給出當(dāng)循環(huán)終止時(shí)，后置斷言為真的定理:

Theormwp3:

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

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

循環(huán)的終止性證明的定理較為簡(jiǎn)單，此處略。

(5)證明相關(guān)定理。

以上定理都可以在定理證明工具Coq中，使用“Induction”“Apply auto”等規(guī)則進(jìn)行求證。

4 “包”構(gòu)件的形式語(yǔ)義與驗(yàn)證

允許重復(fù)元素的一組同類型數(shù)據(jù)構(gòu)成包。包構(gòu)件可以通過(guò)數(shù)組或鏈表實(shí)現(xiàn)。用數(shù)組實(shí)現(xiàn)的包，元素個(gè)數(shù)有限制，稱為有限包，用鏈表實(shí)現(xiàn)的包，元素個(gè)數(shù)無(wú)限制，稱為無(wú)限包。

4.1 “包”構(gòu)件的形式語(yǔ)義

“包”的形式語(yǔ)義類似于集合，但由于“包”允許有重復(fù)元素，所以“包”的大部分操作規(guī)范不同于“集合”。給出“包”的公理語(yǔ)義如下：

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

/*T表示包元素是泛型的，可以是整型、字符型等。SIZE是可選項(xiàng)，如果有SIZE，指包中元素的個(gè)數(shù)不超過(guò)SIZE，該包用數(shù)組實(shí)現(xiàn)。如果缺省SIZE，指包中元素沒(méi)有限制，該包需要用鏈表實(shí)現(xiàn)。下文重點(diǎn)討論有限包*/

Invariant: 0≤length≤SIZE;

Initially:bag=nullbag;

VarS:bag,length:integer;

Operations:

Oneitembag(elem:T)/*Oneitembag操作可建立僅含一個(gè)元素的包，’S表示操作執(zhí)行后，包對(duì)應(yīng)的狀態(tài)，S[0]表示包的首元素*/

Pre True

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

Intersection(R:bag) return(‘S:bag)/*Intersection操作計(jì)算包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操作計(jì)算包S與包R的并集，其中謂詞occ(x,S)表示x在包S中出現(xiàn)的次數(shù)*/

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中出現(xiàn)的元素*/

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中出現(xiàn)的次數(shù)*/

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中出現(xiàn)的次數(shù)*/

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 “包”構(gòu)件的形式化驗(yàn)證

“包”構(gòu)件提供了“求包的并集”“求包的交集”等7個(gè)操作。選取“包”的判斷兩個(gè)“包”是否存在子集關(guān)系的Include操作進(jìn)行驗(yàn)證。

(1)給出該操作的前后置斷言。

根據(jù)上文給出的Include操作的前后置斷言，假設(shè)包S含m+1個(gè)元素，包R含n+1個(gè)元素，occ(x,S)表示x在包S中出現(xiàn)的次數(shù)，可將后置斷言形式寫(xiě)為：

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

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

(2)從程序前后置斷言出發(fā)，進(jìn)行形式化推導(dǎo)，找出程序求解的遞推關(guān)系式，構(gòu)造循環(huán)不變式和求解程序。

利用量詞變換規(guī)則，作如下形式化推導(dǎo)，得出求解該操作的遞推關(guān)系式：

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))

{單點(diǎn)范圍}

≡(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]) 的值，即可得到循環(huán)不變式:

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

根據(jù)遞推關(guān)系和循環(huán)不變式，可得該操作的求解程序?yàn)椋?/p>

i:=0;flag:=true;

WHILEi

BEGIN

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

THEN flag:=false;RETURN

ELSEi:=i+1;

END.

(3)定義相關(guān)數(shù)據(jù)類型、數(shù)據(jù)結(jié)構(gòu)以及相關(guān)函數(shù)。

定義歸納類型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)給出程序應(yīng)滿足相關(guān)屬性的定理。

首先給出首次執(zhí)行循環(huán)，循環(huán)不變式為真的定理：

Theormwp1:

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

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

然后給出每次循環(huán)，循環(huán)不變式均為真的定理:

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

再給出當(dāng)循環(huán)終止時(shí)，后置斷言為真的定理:

Theormwp3:

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

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

循環(huán)的終止性證明的定理較為簡(jiǎn)單，此處略。

(5)證明相關(guān)定理。

以上定理都可以在定理證明工具Coq中，使用“Induction”“Apply auto”等規(guī)則進(jìn)行求證。

5 相關(guān)研究工作

文獻(xiàn)[12，13]在Coq 中利用一階語(yǔ)法對(duì)C語(yǔ)言的語(yǔ)法進(jìn)行描述，并基于歸納謂詞對(duì)C語(yǔ)言、中間語(yǔ)言以及目標(biāo)語(yǔ)言的操作語(yǔ)義進(jìn)行機(jī)械化。文獻(xiàn)[14]中提出了如何在Coq 中對(duì)內(nèi)存模型和并行編譯的正確性進(jìn)行證明。該編譯器的源語(yǔ)言為并行的Clight，目標(biāo)語(yǔ)言為并行的x86 匯編語(yǔ)言。Ynot是Coq 的一個(gè)擴(kuò)展庫(kù)，實(shí)現(xiàn)了分離邏輯?；贑oq 和Ynot，文獻(xiàn)[15]中實(shí)現(xiàn)了一個(gè)輕量級(jí)的、完全經(jīng)過(guò)驗(yàn)證的關(guān)系型數(shù)據(jù)庫(kù)管理系統(tǒng)(RDBMS)，RDBMS 的功能規(guī)范、具體實(shí)現(xiàn)以及該實(shí)現(xiàn)滿足規(guī)范要求的證明，都在Coq 中進(jìn)行了書(shū)寫(xiě)和驗(yàn)證。文獻(xiàn)[16]將CompCert 項(xiàng)目的正確性驗(yàn)證理念運(yùn)用在硬件綜合設(shè)計(jì)上，為Fe-Si(Bluespec的簡(jiǎn)化版)的高級(jí)硬件描述語(yǔ)言實(shí)現(xiàn)了一個(gè)驗(yàn)證編譯器。

上述驗(yàn)證工作主要集中在語(yǔ)義機(jī)械化、編譯過(guò)程驗(yàn)證、關(guān)系數(shù)據(jù)庫(kù)和硬件系統(tǒng)驗(yàn)證上。本文結(jié)合Coq系統(tǒng)特點(diǎn)和團(tuán)隊(duì)在循環(huán)不變式方面的開(kāi)發(fā)新技術(shù)，程序形式化推導(dǎo)上的技術(shù)優(yōu)勢(shì)，強(qiáng)調(diào)循環(huán)不變式在形式化驗(yàn)證中所起的關(guān)鍵作用，將基于Coq的形式化驗(yàn)證過(guò)程分為5個(gè)主要步驟，并驗(yàn)證了PAR平臺(tái)若干典型軟件構(gòu)件的正確性。

6 結(jié)束語(yǔ)

PAR平臺(tái)中的可重用軟件構(gòu)件是PAR平臺(tái)體現(xiàn)功能抽象和數(shù)據(jù)抽象特性，實(shí)現(xiàn)便捷、可靠開(kāi)發(fā)軟件的關(guān)鍵因素。因此，這些軟件構(gòu)件自身的正確性和可靠性顯得尤為重要。

本文利用Hoare公理系統(tǒng)對(duì)軟件構(gòu)件進(jìn)行形式化描述，給出了精確的語(yǔ)義。進(jìn)而，利用定理證明器Coq提供的歸納類型等抽象表示機(jī)制刻畫(huà)軟件構(gòu)件實(shí)現(xiàn)程序和對(duì)應(yīng)循環(huán)不變式的屬性，利用Coq提供的命題演算、謂詞演算功能機(jī)械地證明實(shí)現(xiàn)程序是否滿足前后置斷言，從而實(shí)現(xiàn)形式化驗(yàn)證軟件構(gòu)件正確性的目標(biāo)。

將在此工作基礎(chǔ)上，進(jìn)一步探索如何給出PAR平臺(tái)Radl語(yǔ)言、Apla語(yǔ)言的完整語(yǔ)義，如何形式化刻畫(huà)Apla抽象程序到C++、Java等可執(zhí)行程序自動(dòng)生成系統(tǒng)的主要功能，進(jìn)而利用Coq工具，形式化驗(yàn)證PAR平臺(tái)程序自動(dòng)生成系統(tǒng)關(guān)鍵功能的正確性。

[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.