(1. 廣州大學(xué) 計(jì)算機(jī)科學(xué)與網(wǎng)絡(luò)工程學(xué)院, 廣東 廣州 510006; 2. 北京大學(xué) a.信息科學(xué)技術(shù)學(xué)院軟件研究所; b.高可信軟件技術(shù)教育部重點(diǎn)實(shí)驗(yàn)室, 北京 100871)

1 研究背景

1.1 形式化驗(yàn)證方法簡介

作為計(jì)算機(jī)系統(tǒng)的靈魂，軟件中存在的任何缺陷都可能成為隱患，以至于對整個(gè)計(jì)算機(jī)系統(tǒng)造成致命影響.目前，軟件質(zhì)量的可靠性保障方法正在受到工業(yè)界和學(xué)術(shù)界的廣泛關(guān)注.經(jīng)過多年努力，相繼出現(xiàn)了很多相關(guān)的工具和技術(shù)，它們有的應(yīng)用于軟件開發(fā)前的程序架構(gòu)，有的用于開發(fā)期間的實(shí)現(xiàn)與測試，還有的用于對已發(fā)布的軟件進(jìn)行分析和驗(yàn)證等.但是對于強(qiáng)安全需求的(safty critical)計(jì)算機(jī)系統(tǒng)，例如核電站的溫控系統(tǒng)、導(dǎo)彈的制導(dǎo)系統(tǒng)等等，不允許程序中隱藏任何潛在錯(cuò)誤，否則將會造成巨大的財(cái)產(chǎn)損失，甚至對社會造成不可預(yù)計(jì)的災(zāi)難.

形式化驗(yàn)證方法通過運(yùn)用嚴(yán)格的數(shù)學(xué)方法分析和驗(yàn)證計(jì)算機(jī)程序的正確性[1]，從數(shù)學(xué)角度保證程序中不存在錯(cuò)誤，通常使用的方法有公理推導(dǎo)、模型檢驗(yàn)(model checking)、約束求解、抽象解釋和符號執(zhí)行等.形式化驗(yàn)證的優(yōu)點(diǎn)是，其描述計(jì)算機(jī)軟、硬件及其性質(zhì)的語言是無歧義的，構(gòu)造和驗(yàn)證計(jì)算機(jī)軟、硬件的方法是嚴(yán)格的，因此，該技術(shù)被廣泛應(yīng)用于驗(yàn)證強(qiáng)安全需求的計(jì)算機(jī)系統(tǒng)的正確性.

1.2 分離邏輯的研究背景

對程序進(jìn)行形式化驗(yàn)證的過程中，邏輯斷言是用來描述程序狀態(tài)的主要技術(shù).圖靈(Turing)[2]曾在1949年嘗試運(yùn)用斷言來驗(yàn)證特定程序的正確性，隨后Floyd[3]和Hoare[4]在20世紀(jì)60年代將該方法推廣到程序證明的一般形式，建立了新的邏輯系統(tǒng)，稱為Hoare邏輯系統(tǒng)(也稱Floyd-Hoare邏輯).Hoare邏輯的中心特征是Hoare三元組，為命令式程序的規(guī)范說明，定義了程序執(zhí)行前后系統(tǒng)狀態(tài)應(yīng)滿足的屬性.Hoare邏輯系統(tǒng)對于處理簡單原始的數(shù)據(jù)類型非常有效(例如：整數(shù)或字符串)，但Hoare不便于描述程序中的地址操作，因此，在處理包含指針的結(jié)構(gòu)化數(shù)據(jù)時(shí)，指針操作雖簡單直觀，但驗(yàn)證過程會相當(dāng)復(fù)雜晦澀[5].

分離邏輯(Separation Logic)是一種推導(dǎo)共享可操作存儲程序的新方法，最初由Reynolds[6]和Ishtiaq等[7]提出，該邏輯系統(tǒng)是Hoare邏輯的一個(gè)擴(kuò)展，其中心特征也是三元組.其基本形式為

{P}C{Q},

其中P稱為前置斷言，Q為后置斷言，C是指令.直觀描述為：若在C執(zhí)行前，P成立.則當(dāng)執(zhí)行終止后(若終止)，Q成立.例如，下述規(guī)范說明

{x==N}code{x==N∧y==N!}

可以應(yīng)用到“將變量x值的階乘賦值于y” 程序的驗(yàn)證中.分離邏輯通過解決潛在的指針別名問題，從而簡化對包含共享可操作數(shù)據(jù)結(jié)構(gòu)程序的驗(yàn)證.

在過去的15年中，分離邏輯發(fā)展成為針對可擴(kuò)展程序(scalable program)的主流驗(yàn)證技術(shù)[8].在LICS、POPL、JACM等頂尖國際會議和期刊上，幾乎年年都有相關(guān)文章發(fā)表.分離邏輯之所以能夠成功，是因?yàn)樗軌驅(qū)④浖こ處煂τ谟?jì)算機(jī)共享可操作存儲程序的概念模型與邏輯中解釋語句正確性的邏輯模型相結(jié)合，從而形成一整套證明系統(tǒng)來幫助解決可操作存儲程序推理任務(wù)的關(guān)鍵問題.

分離邏輯可以對含有各類鏈表、樹以及圖等復(fù)雜數(shù)據(jù)結(jié)構(gòu)的程序進(jìn)行驗(yàn)證，如鏈表的排序、完全二叉樹的操作、堆排序、AVL樹等等.還有很多用于實(shí)際程序的驗(yàn)證，比如驗(yàn)證Schorr-Waite算法與DFS算法的等價(jià)性[9]，Schorr-Waite是一種基于圖的垃圾回收的算法，一般的垃圾回收算法使用深度優(yōu)先遍歷(DFS)搜索,需使用棧記錄當(dāng)前訪問路徑.而Schorr-Waite程序不使用棧,僅使用圖本身的指針實(shí)現(xiàn)回溯，這種數(shù)據(jù)結(jié)構(gòu)可以被分離邏輯簡單直接的表示.此外，還有驗(yàn)證內(nèi)存管理系統(tǒng)中Cheney的復(fù)制垃圾回收器 (Copying Garbage Collector) 程序的正確性[10]；運(yùn)用SpaceInvader分析器驗(yàn)證Linux和Windows系統(tǒng)中近1萬個(gè)指針的安全性[11]；以及在該驗(yàn)證器的基礎(chǔ)上由微軟開發(fā)的SLAyer，甚至可以在Windows的設(shè)備驅(qū)動(dòng)程序中找出10多個(gè)隱藏的內(nèi)存安全錯(cuò)誤等等[12].這些分離邏輯在學(xué)術(shù)和商業(yè)上的應(yīng)用，很好地說明了其具有很強(qiáng)的實(shí)用性.

由于篇幅有限，本文將簡要闡述分離邏輯的基本方法，包括該邏輯系統(tǒng)對存儲的抽象描述方法、推理過程，以及在自動(dòng)化驗(yàn)證技術(shù)上的革新，并會簡要概括分離邏輯的一些拓展及相關(guān)工作.

2 理論基礎(chǔ)及驗(yàn)證實(shí)例

2.1 分離邏輯對存儲空間的抽象描述

分離邏輯對于Hoare邏輯的擴(kuò)展在于，能夠直觀地分析程序中復(fù)雜的動(dòng)態(tài)內(nèi)存變化，這種分析能力依賴于該邏輯系統(tǒng)對計(jì)算機(jī)程序訪存過程的描述.分離邏輯引入棧(Stack)和堆(Heap)的概念，與數(shù)據(jù)結(jié)構(gòu)中提到的堆和棧不同，分離邏輯中棧表示“變量→地址”和“變量→值”的映射，堆則表示“地址→值”的映射.運(yùn)用堆和棧，分離邏輯系統(tǒng)不僅可以模擬程序直接訪問寄存器中的值，還可以模擬“變量→地址→值”的一般情況[13].可以用下面的例子：

{x0*y0}
[x]=y;
[y]=x
{xy*yx}

作為規(guī)范說明來描述兩個(gè)內(nèi)存地址連接成循環(huán)鏈表.其中xv表示指針變量x保存著指向“內(nèi)存中已分配空間”v所對應(yīng)的地址；指令[x]=y表示更改x引用地址中的內(nèi)容，使其值更新為v′；通過使用“*”而不是通常的布爾連接符“∧”，確保x和y不出現(xiàn)別名混淆，即多個(gè)變量指向同一地址，由此在后置條件下就可以描述一個(gè)雙元素的循環(huán)列表[14].上述解釋可參考圖1理解.

圖1 循環(huán)鏈表語義示意圖Fig.1 The semantics of cyclic linked list

根據(jù)分離邏輯對存儲空間的描述，下面闡述該邏輯系統(tǒng)語義域，以此來劃分它在語義上的討論范圍.一般的程序語義驗(yàn)證系統(tǒng)不考慮浮點(diǎn)型，因此，本文所描述的分離邏輯系統(tǒng)中的數(shù)值只考慮整型，不考慮浮點(diǎn)型，并且該邏輯系統(tǒng)的運(yùn)算不包含除法.程序中變量的值可能為整數(shù)或地址：

Value=Integers∪Addresses.

地址在計(jì)算機(jī)中以整型的數(shù)據(jù)類型存儲：

Addresses?Integers；

堆表示“地址與值”的映射關(guān)系：

Heap=∪A→Addresses(A→Values)，A是有限集；

棧表示“變量→值”的映射關(guān)系(包括“變量→地址”)：

StackV=V→Values，V是代表Variables的有限集；

狀態(tài)(StatesV)表示當(dāng)前系統(tǒng)中的存儲狀態(tài)，以棧和堆的笛卡爾積表示：

StatesV=StacksV×Heaps.

為方便討論，在本文中規(guī)定以s表示棧，以h表示堆.(s,h)表示當(dāng)前系統(tǒng)的存儲狀態(tài).

2.2 分離邏輯的語法及斷言語言

了解分離邏輯的對計(jì)算機(jī)存儲的抽象，便可以如下定義分離邏輯的語法的BNF表示：

v∈V,n∈Values

q|p*q|p|p-*q|?v.p|?v.p

分離邏輯對于Hoare邏輯的拓展主要是通過引入4種新的斷言形式，以細(xì)化對計(jì)算機(jī)系統(tǒng)存儲狀態(tài)的描述.下面主要介紹這些新引入的斷言.

Assertionsp,q∷=…

|emp空堆

|ke單堆

|p*q分離合取

|p-*q分離蘊(yùn)含

定義新形式斷言的語義要依靠其在狀態(tài)(s,h)中的賦值，因此，下面結(jié)合狀態(tài)(s,h)來說明新斷言的語義.用eexps表示表達(dá)式e在s中的取值，pasrtsh表示斷言p在狀態(tài)(s,h)中可以被滿足，由此可定義新斷言的語義如下：

空堆

empasrtshiffdomh={ }.

空堆即堆h為空，其中domh表示堆h的定義域.

單堆

e

domh={eexps} andh(eexps)=

單堆的意思是系統(tǒng)狀態(tài)的堆中僅包含了一個(gè)單元，且該單元的地址是eexps，內(nèi)容是e′.直觀來講，單堆準(zhǔn)確地描述了計(jì)算機(jī)的存儲狀態(tài)，如圖1中xy所代表的“x指向y，且y指向空”消除了對內(nèi)存表示的歧義：指針x和y分別表示某個(gè)值(x=10,y=32)，x的值是該變量被分配的地址空間(address:10)，該地址用于存儲值y，但y的值并沒有被分配空間存儲.

分離合取

handp0asrtsh0andp1asrtsh1.

分離合取斷言了堆h可以被分割成兩個(gè)互不相交的子堆h0,h1，并且兩個(gè)子堆分別滿足斷言p0和p1，其中h0⊥h1代表兩個(gè)堆互不相交.分離合取是分離邏輯很重要的一個(gè)斷言形式，該斷言可以分離堆和內(nèi)存，但它并不會分割變量與值的關(guān)聯(lián).如圖1中xy*yx就斷言了兩個(gè)不相交的堆的合取.由上述單堆的定義可知，不考慮分離合取的連接詞，就有“x指向y，且y指向空”以及“y指向x，且x指向空”這兩個(gè)形式的單堆.在兩個(gè)堆中，指針變量x和y都分別在內(nèi)存中被分配了地址.故經(jīng)過分離合取，就可以得到“x指向y，且y指向x”的結(jié)果.

分離合取連接詞“*”和布爾合取連接詞“∧”的區(qū)別是：P*P≠P但P∧P=P.尤其xv*xv是永假式，因?yàn)闆]有辦法將同一個(gè)變量x所對應(yīng)的存儲單元，劃分到兩個(gè)不相交的堆中.分離合取經(jīng)常被應(yīng)用到表示鏈表結(jié)構(gòu)中.比如用list(x,y)表示一個(gè)從x到y(tǒng)的非循環(huán)鏈表，將在下文的驗(yàn)證實(shí)例中對其形式化定義.那么運(yùn)用分離合取連接詞，就可以描述某個(gè)鏈表片段，后面接上一個(gè)單獨(dú)的節(jié)點(diǎn)，甚至一個(gè)終止節(jié)點(diǎn)為0(null)的鏈表片段，圖2所示：

list(x,t)*ty*list(y,0).

圖2 鏈表結(jié)構(gòu)示意圖
Fig.2 A structure with a list segment

分離蘊(yùn)含

分離蘊(yùn)含指如果有一個(gè)與當(dāng)前堆h互不相交的拓展堆h′，可以使斷言p0滿足.那么斷言p1也可以被該拓展堆滿足.舉例說明，對于

(x-)*((x3)-*Q),

其中x-指x已分配但不關(guān)心其具體存儲的值，則該命題公式表示了x在當(dāng)前堆中已分配的情況下，如果將其內(nèi)容改為3，那么Q將成立,即描述了對于后置條件Q對于命令[x]=3的“最弱前置條件”.這種類似A*(A-*B)├B的推理，被稱為分離邏輯相關(guān)的演繹推理.

2.3 分離邏輯的推導(dǎo)規(guī)則

作為一個(gè)形式化系統(tǒng)的推理工具，推導(dǎo)規(guī)則在驗(yàn)證過程中起到了很重要的作用.圖3包含了分離邏輯中的部分規(guī)則，這些規(guī)則被分為描述基礎(chǔ)數(shù)據(jù)更改操作的小公理和用于模塊化推理的局部推理規(guī)則.推理規(guī)則可以被理解為“如果橫線上面的可以被推導(dǎo)出來，那么就可以推導(dǎo)出橫線下的結(jié)果”，而公理是已知的可滿足公式.

圖3 分離邏輯的部分規(guī)則
Fig.3 Partial rules of Separation logic

第一條公理表示如果x之前指向某個(gè)值，把其地址對應(yīng)的內(nèi)容改為v后，x將指向新的值v；第二條公理表示如果x之前存儲了值v，用變量y讀取x地址所對應(yīng)的內(nèi)容時(shí)，y將會暫存v的值.這條公理為我們區(qū)分值在寄存器和堆中的不同描述：由于y只是將值v用作暫存，不會被分配地址空間，也就不會對堆產(chǎn)生更改，因此用y==v表示，該公理假設(shè)x不出現(xiàn)在表達(dá)式v中；第三條公理表示如果開始時(shí)沒有堆，執(zhí)行分配操作后就會產(chǎn)生大小為1的堆；反之，第四條公理表示如果開始時(shí)是大小為1的堆，那么執(zhí)行釋放操作后將以空堆作為結(jié)束.

從某種意義上，小公理涵蓋了它們所描述語句的關(guān)鍵信息.直觀來講，這些簡單的語句每次只更新或訪問一個(gè)內(nèi)存單元，那么僅描述這個(gè)單元格發(fā)生什么就足夠了，以此可以運(yùn)用就地推理的策略對程序狀態(tài)進(jìn)行驗(yàn)證，即僅在上一個(gè)狀態(tài)的基礎(chǔ)上作更新.但又因?yàn)樾」磉^于簡單，所以它暫時(shí)不能基于系統(tǒng)全局的狀態(tài)進(jìn)行推理.

圖3中的框架規(guī)則(Frame Rule)則為分離邏輯提供了從局部推導(dǎo)到全局推導(dǎo)的邏輯上的幫助.它允許我們將推理從一個(gè)拓展到多個(gè)存儲單元，因此，僅作用于一個(gè)單元的小公理便不會再是一種限制，反而成為了一種簡潔直觀的描述.以上文提到的關(guān)于構(gòu)造循環(huán)鏈表的程序?yàn)槔旅嬲f明運(yùn)用框架規(guī)則將局部推導(dǎo)應(yīng)用到全局，假定以r來描述全局的其他狀態(tài)，即框架公式，為直觀起見將框架公式記為紅色，那么對于在上文提到的關(guān)于構(gòu)造循環(huán)鏈表的程序，就可以做如下驗(yàn)證：

{x0*y0*r}，
[x]=y;
{xy*y0*r}，
[x]=y;
{xy*yx*r}.

上述推導(dǎo)過程說明了基于小公理的就地推理，以及框架規(guī)則對局部推理到全局的拓展，可以實(shí)現(xiàn)對系統(tǒng)全局狀態(tài)的推理驗(yàn)證.該例子涉及到的推理方法，可以推廣到若干由鏈表或樹作為數(shù)據(jù)結(jié)構(gòu)的程序中.

2.4 驗(yàn)證實(shí)例

通過運(yùn)用上文所介紹的分離邏輯的理論基礎(chǔ)，本節(jié)將證明鏈表的原地翻轉(zhuǎn)和二叉樹的刪除這兩個(gè)程序，以說明分離邏輯的表達(dá)能力以及其實(shí)際應(yīng)用價(jià)值.

2.4.1 驗(yàn)證鏈表的原地翻轉(zhuǎn)程序

由于描述鏈表的斷言是一個(gè)斷言的公式序列，而且其存儲情況又比較復(fù)雜，因此對于該類情況的考察，需要定義一些額外的虛擬符號便于說明.對斷言序列α和β，定義如下符號：

α·β表示形如序列α后跟隨著β的公式序列；

α?表示序列α的映象，即序列α中所含內(nèi)容.

使用謂詞listα(i,j)表示第一個(gè)結(jié)點(diǎn)由i指向，最后一個(gè)結(jié)點(diǎn)由j指向的鏈表片段α，其存儲狀態(tài)如圖4所示.

圖4 鏈表list α(i, j)示意圖Fig.4 The semantics of list α(i, j)

易知一個(gè)完整的鏈表應(yīng)形如listα(i,nil)，nil代表空結(jié)點(diǎn).根據(jù)listα(i,j)的結(jié)構(gòu)可以直接定義斷言公式如下：

以及歸納如下的基礎(chǔ)性質(zhì)：

list(nil,nil)?emp；

lista(i,j)?ia,j；

listα·β(i,k)?j.listα(i,j)*listβ(j,k).

下面演示如何使用分離邏輯，對原地反轉(zhuǎn)單向鏈表的程序段，進(jìn)行存儲情況的分析以及部分正確性證明.

例：單向鏈表原地反轉(zhuǎn)的程序REV，代碼如下：

while(i≠nil)；

證明

(1){listα0(i,nil)}

前置條件

(4){i≠nil}

由(1)可得

(8){?a,α,β,k.(i(7)可得.a為listα頭結(jié)點(diǎn)

循環(huán)體第1條語句

(10){?a,α,β.(i

循環(huán)體第2條語句

(12){?a,α,β.(listα(k,nil)*(ia,k)

循環(huán)體其他語句

上述推理驗(yàn)證了對鏈表原地反轉(zhuǎn)程序的規(guī)范說明，即證明了鏈表原地翻轉(zhuǎn)程序的正確性.下面將舉例說明，運(yùn)用分離邏輯證明二叉樹刪除實(shí)際程序的正確性.

2.4.2 驗(yàn)證二叉樹刪除實(shí)際程序

例：二叉樹刪除程序deletetree，實(shí)際代碼如下：

voiddeletetree(structnode*root){

if(root!= 0){

structnode*left=root->l, *right=root->r;

deletetree(left);

deletetree(right);

free(root);

} }

需證:程序開始時(shí),樹以root為根節(jié)點(diǎn);當(dāng)程序段執(zhí)行完成后, 系統(tǒng)狀態(tài)為空堆.即

{tree(root)}deletetree(root) {emp}.

證明

首先定義描述二叉樹tree()的語義如下(圖5),

else ?xy.root[l:x,r:y]*tree(x)*tree(y).

圖5 root[l:x,r:y]的示意圖Fig.5 The semantics of root[l:x,r:y]

這里使用謂詞root[l:x,r:y]來描述具有l(wèi)和r字段的對應(yīng)的內(nèi)容.下面用分離邏輯證明刪除二叉樹的操作，注意使用紅色標(biāo)記框架公式.

{root[l:left,r:right]*tree(left)*tree(right)}

deletetree(left)

{root[l:left,r:right]*emp*tree(right)}

deletetree(right)

{root[l:left,r:right]*emp*emp}

free(root)

{emp*emp*emp}

{emp}

程序證明中的初始條件是對tree(root)中root≠0分支的語義展開.證明步驟按照算法的直觀描述：首先遞歸調(diào)用刪除左子樹，其次刪除右子樹，最后一個(gè)語句刪除根節(jié)點(diǎn).在該證明過程中，每一步的推導(dǎo)都是對整體的歸納證明，并且由于框架規(guī)則，未被遞歸調(diào)用函數(shù)所影響的存儲空間保持不變.由此可見基于局部推理，可以簡單且直觀地對程序進(jìn)行證明.框架規(guī)則提供了將局部推理擴(kuò)展到了全局的方法，因此，僅需對命令所改變的內(nèi)容進(jìn)行驗(yàn)證.

3 分離邏輯的擴(kuò)展

3.1 并發(fā)分離邏輯

并發(fā)分離邏輯是目前較為熱門的研究方向之一.2007年，O′Hearn[15]提出了并發(fā)分離邏輯(concurrent separation logic, 簡稱CSL)，與此同時(shí), Brookes[16]則對CSL做了詳盡的理論分析, 給出了CSL的一個(gè)基于跡模型(trace model)的指稱語義.Brookes和O′Hearn由于對并行分離邏輯的開創(chuàng)性貢獻(xiàn)而獲得了2016年哥德爾獎(jiǎng).本節(jié)將主要描述并發(fā)分離邏輯涉及到的基本想法.

對于驗(yàn)證完全不共享存儲空間的并行程序，分離邏輯提供了一個(gè)可行的規(guī)則如下:

該規(guī)則主要依賴于每個(gè)進(jìn)程完全獨(dú)立的推導(dǎo)，即進(jìn)程間不操作共享的存儲空間.由此，對于上文提到的構(gòu)建循環(huán)鏈表的例子就可以構(gòu)建證明如下.

易知[x]=y和[y]=x不會對共享的存儲空間進(jìn)行操作，因此，該推導(dǎo)可以一步得出最終結(jié)果.

為了靈活起見，對于帶有共享內(nèi)存操作的并行程序，O′Hearn使用了帶有擁有權(quán)的假設(shè)，該假設(shè)指任何代碼片段只能訪問當(dāng)前其所“擁有的”狀態(tài).下面舉例說明該思想，對于如下帶有初始化和資源定義的形式程序：

init;

resourcer1(variablelist),…,resourcerm(variablelist)

C1‖…‖Cn，

通過引入條件臨界語句，用withrthenBdoCendwith來描述代碼段C，只有在其所處進(jìn)程當(dāng)前擁有資源r，并且條件B為真的時(shí)候才可以執(zhí)行.因此就可以將共享空間中的變量，約束在其所屬的進(jìn)程中進(jìn)行單獨(dú)的推理驗(yàn)證，其推理規(guī)則可表示如下：

這里的想法是:代碼C當(dāng)前所處狀態(tài)P，且擁有資源r所處的狀態(tài)(資源不變式RIr),并且可以訪問這些共享狀態(tài),那么程序就以Q狀態(tài)結(jié)束執(zhí)行，且保證資源不變式仍然成立.這條規(guī)則描述了資源共享狀態(tài)擁有權(quán)的遷移.以此并行分離邏輯可以對上述程序定義如下的推理規(guī)則：

其中，RIri*…*RIrm為描述每個(gè)資源的不變式，該規(guī)則表示了對于給定的前置條件P，經(jīng)過初始化程序可建立若干資源不變式RIri*…*RIrm，以及中間狀態(tài)P′，該狀態(tài)執(zhí)行C1‖…‖Cn程序后，須滿足后置條件Q.

不過目前并發(fā)分離邏輯系統(tǒng)，對于并發(fā)程序的驗(yàn)證還需人工提供的很深入的機(jī)制，并且需引入很多共享狀態(tài)使用協(xié)議、幽靈狀態(tài)等作為輔助[17]，因此，最終實(shí)際應(yīng)用還有很長的距離.

3.2 符號執(zhí)行的描述

近幾年陸續(xù)產(chǎn)生了很多使用分離邏輯的同類型邏輯系統(tǒng).“符號堆”(Symbolic Heaps)是描述分離邏輯符號執(zhí)行很常用的方法[18]，其語法形式如下所示

Δ∷=Π∧Σ，

其中Δ中的Π和Σ分別表示“與堆無關(guān)的公式”和“受堆限制的公式”.Δ稱為無量詞的符號堆公式，H即為符號堆公式.而且為了便于描述符號執(zhí)行，符號堆中使用E0[f1:E1,…,fk:Ek]的斷言形式，通過標(biāo)號f0劃分了討論的領(lǐng)域，以上文所提到的

root[l:left,r:right]*tree(left)*tree(right)

來表示根為root，左子為left，右子為right的二叉樹,就是運(yùn)用了這種公式形式.邏輯系統(tǒng)通過引入符號執(zhí)行，能夠提高就地推導(dǎo)的效率.作為第一個(gè)分離邏輯的驗(yàn)證工具，Berdine等[19]就引入了符號堆，通過給定前置/后置條件和循環(huán)不變量，Smallfoot可以構(gòu)造所需的證明序列，也使得其的驗(yàn)證對象從僅限單堆、鏈表、樹的斷言形式，拓展到包括對數(shù)組及算術(shù)等更多的驗(yàn)證方向.近年來基于分離邏輯的斷言語言也大多采用了符號堆模型.數(shù)組分離邏輯(Array Separation Logic)[20]，就是符號堆分離邏輯的一種變體，其驗(yàn)證的數(shù)據(jù)結(jié)構(gòu)包含指針和數(shù)組.

4 輔助證明方法

4.1 分離邏輯的Coq實(shí)現(xiàn)

由于邏輯推導(dǎo)過程的高成本降低了其實(shí)用價(jià)值，因此，近年來很多邏輯都會實(shí)現(xiàn)工具進(jìn)行輔助證明.Coq作為基于高階邏輯(Church′s higher-order logic)的輔助證明工具，被廣泛應(yīng)用到以分離邏輯為基礎(chǔ)的推理系統(tǒng)中.Coq由法國國家信息研究所(INRIA)開發(fā)，以歸納演算為理論基礎(chǔ)，用戶可通過歸納定義進(jìn)行對定理或程序的構(gòu)造性證明.相比Isabelle/HOL[21]等同類型的輔助證明工具，Coq能精確表示程序設(shè)計(jì)語言的語法和語義，并且可以從證明中提取程序，這使得Coq更便于構(gòu)建計(jì)算機(jī)程序相關(guān)證明系統(tǒng).如由134行C語言代碼構(gòu)成的OpenSSL中的HMAC認(rèn)證程序[22]，就由 Beringer等基于分離邏輯的思想，以2 832行Coq代碼實(shí)現(xiàn)了對該程序的正確性驗(yàn)證.另一個(gè)更大規(guī)模的例子是對FSCQ文件系統(tǒng)的證明[23]，相比較該程序的3千行源碼，研究人員對該程序的代碼抽象和證明過程約占用了31 000行Coq代碼.雖然消耗了大量的人力物力，但是實(shí)驗(yàn)表明該工具大大節(jié)省了驗(yàn)證成本，并且實(shí)現(xiàn)了對該文件系統(tǒng)的交互式證明.

4.2 雙向誘導(dǎo)推理方法

雙向誘導(dǎo)推理方法(Bi-Abduction)是支持對系統(tǒng)可拓展證明的新成果.可拓展證明是指對于百萬級別的地址空間，所需引入模塊化分析的思想.現(xiàn)有的證明系統(tǒng)，沒有辦法描述如此巨大的全局系統(tǒng)狀態(tài).這就要求邏輯系統(tǒng)能夠?qū)植看a進(jìn)行分析，其中會涉及到包括代碼未完成，甚至未知系統(tǒng)當(dāng)前狀態(tài)等很多技術(shù)難點(diǎn).理想的模塊化推理技術(shù)，可以接受沒有經(jīng)過任何人工注釋的代碼，自動(dòng)生成前置/后置規(guī)范說明，并將這些規(guī)范依次結(jié)合，最終實(shí)現(xiàn)對整體程序的驗(yàn)證[14].這種分析過程是組合式的，因?yàn)槊恳徊酵评矶伎梢栽诓恢狼疤岬臈l件下進(jìn)行，即每一步都是獨(dú)立的.Distefano等[24]在模塊化分析的拼接上有了新的突破，構(gòu)建了雙向誘導(dǎo)推理(Bi-Abduction)方法，該方法支持組合的形狀分析(Compositional Shape Analysis)技術(shù)，能對前置/后置條件進(jìn)行雙向誘導(dǎo)推理，該方法形式如下:

A*?anti-frameB* ?frame，

當(dāng)前執(zhí)行狀態(tài): {emp} [x]=y;[y]=x{???},

雙向誘導(dǎo)問題:emp* ?anti-frame(x-)*?frame,

解決方案： ?anti-frame=x-; ?frame=emp.

之后，用frame來消除前置條件中的部分公式，并且根據(jù)小公理對當(dāng)前狀態(tài)進(jìn)行推導(dǎo)，以此更新當(dāng)前的執(zhí)行狀態(tài).

當(dāng)前執(zhí)行狀態(tài): {x-} [x]=y{xy}[y]=x{???},

雙向誘導(dǎo)問題: (xy)*?anti-frame(y-)*?frame,

解決方案： ?anti-frame=y-; ?frame=xy.

這時(shí)得到的y-是[y]=x的前置條件，由框架規(guī)則可知，[x]=y并不會對狀態(tài)y-產(chǎn)生更改，因此，可以將其移至整體的前置條件中，并且由小公理可以得到的結(jié)果，也可以由框架規(guī)則移至整體的后置斷言，因此便構(gòu)成了如下推理：

{(x-)*(y-)},
[x]=y,
[y]=x,
{(xy)*(yx)}.

由此，就可以在未知當(dāng)前的系統(tǒng)狀態(tài)下，對指定代碼片段進(jìn)行分析驗(yàn)證.這樣就可以僅提取百萬地址級別的巨大程序中，對想要驗(yàn)證的代碼進(jìn)行模塊化分析，以此拓展到對全部程序的驗(yàn)證.

5 總 結(jié)

分離邏輯的理念在2001年初被提出，由于其對存儲空間的描述更為細(xì)致，分析過程更為全面，因此也體現(xiàn)了它具有更高的應(yīng)用價(jià)值.從該理念的提出到本文寫作完成，也不過經(jīng)歷了20年的時(shí)間，這期間圍繞該模型的相關(guān)研究蓬勃發(fā)展，已經(jīng)從驗(yàn)證操作動(dòng)態(tài)內(nèi)存程序的形式化推理系統(tǒng)，發(fā)展到如今在工具的幫助下，能夠自動(dòng)實(shí)現(xiàn)對未完成代碼以及代碼片段進(jìn)行分析驗(yàn)證，甚至不用額外提供待驗(yàn)證代碼執(zhí)行前的系統(tǒng)狀態(tài).

然而，目前運(yùn)用分離邏輯對計(jì)算機(jī)程序的驗(yàn)證過程還涉及到諸多困難和挑戰(zhàn)，例如對并發(fā)程序的驗(yàn)證目前仍需提供大量的人工機(jī)制、對云存儲等巨大復(fù)雜的存儲結(jié)構(gòu)沒有簡潔的方法描述，以及很難融合人工智能的相關(guān)成果等.因此，將分離邏輯真正應(yīng)用到工商業(yè)的實(shí)際開發(fā)中還有很長的一段路要走.