同步數(shù)據(jù)流語言時態(tài)消去的可信翻譯

張玲波，甘元科，石 剛，王生原，董 淵，張智慧，王沿海

（1.清華大學 計算機科學與技術(shù)系，北京100084；2.北京廣利核系統(tǒng)工程有限公司，北京100094））

0 引 言

同步數(shù)據(jù)流語言Lustre［1］廣泛應用于航空航天、醫(yī)療衛(wèi)生、高速鐵路和核電能源等領(lǐng)域的安全關(guān)鍵系統(tǒng) （safety－critical system，SCS），但是此類語言的相關(guān)開發(fā)工具本身的安全性已成為被高度關(guān)注的安全隱患之一，同步數(shù)據(jù)流語言到串行命令式語言的可信編譯器的是開發(fā)工具的典型代表。普通編譯器的確保安全的方法一般有兩種，一是通過大量的測試來減少錯誤，二是通過人工的方法進行檢查，這兩種方法都是不可靠的，測試的方法無法做到完全覆蓋，而人工的方法存在大量不確定因素，因此普通的編譯器存在著大量的 “誤編譯”問題。而采用形式化的方法進行常規(guī)編譯器的構(gòu)造和驗證已經(jīng)被證明是成功的，有望最大限度地解決 “誤編譯”問題。為了實現(xiàn)同步數(shù)據(jù)流語言可信編譯器的形式化驗證工作，必須要完成同步數(shù)據(jù)流語言時態(tài)運算向C語言翻譯的證明，因此需要采用形式化的方法，從邏輯上對同步數(shù)據(jù)流語言編譯器時態(tài)翻譯的正確性進行驗證，最終將程序的翻譯正確性歸結(jié)到語法抽取和語義定義的正確性上，而成熟的同步數(shù)據(jù)流語言的語法語義有統(tǒng)一的標準可以借鑒，從而最終在嚴格的數(shù)學邏輯上給出了程序翻譯的正確性證明。查，拓撲排序，語言簡化，時態(tài)消去，最終翻譯到Comp－Cert的C前端子集，L2C項目是國際首次對Lustre到C的可信翻譯進行的開創(chuàng)性的成功探索。

1 相關(guān)研究

Lustre作為一種同步語言［2］，有著嚴格可靠的數(shù)學定義，對于同步范型有著友好的工程設計方法，廣泛應用于安全關(guān)鍵系統(tǒng)。同步流語言發(fā)展成熟，比較著名的有Lustre，Esterel，Signal，同步語言的一個共同特征是遵循同步假設：當前周期的輸入事件出現(xiàn)時，系統(tǒng)能夠在下一周期的輸入事件出現(xiàn)之前足夠快地產(chǎn)生相應于當前周期的輸出。Lustre作為同步語言的代表，具有時鐘同步和數(shù)據(jù)流對象的特征，是陳述式語言，具有確定的語義［3］。

Lustre到C語言的翻譯已經(jīng)有比較成功的商用用例，國際著名編譯器SCADE［4］已通過多個安全級工業(yè)標準 （如軍事和航空領(lǐng)域的DO178B）的認證，SCADE成功運用于航空等重要領(lǐng)域，但是SCADE的成功在于對Lustre語言執(zhí)行的正確性的檢測，而對于其中的編譯器部分的翻譯工作的正確性的驗證，仍然是一個急需解決的安全隱患［5］。我們的做法是將Lustre到C語言的翻譯，使用Coq［6］定理證明器，通過形式化的定義和證明來機械化的確定程序運行的正確，而Coq除了基本的歸納推導和常規(guī)的一階邏輯外還包含高階邏輯和依賴類型等高級功能［7］。

形式化的定義和證明有很多成功的例子。學術(shù)上著名的CompCert［8］編譯器，將C的一個完備子集翻譯到Power－PC匯編代碼，其正確性證明經(jīng)過機械化檢查，達到了我們所能期望的最高可信程度［9］。X.Yang等關(guān)于Csmith的研究工作［10］表明：CompCert在正確性方面的表現(xiàn)明顯優(yōu)于常用的開源或商用C編譯器。另一個成功案例是經(jīng)過驗證的內(nèi)核操作系統(tǒng)seL4［11］，系統(tǒng)在抽象層specification保證了系統(tǒng)運行的內(nèi)部邏輯正確性，從而提高了系統(tǒng)安全性，進而能有效防止漏洞溢出等攻擊手段。

本文源于清華大學軟件所Lustre to C（L2C）項目工程。L2C項目的目的是將Lustre語言翻譯到C語言的一個完備子集［12］并對翻譯進行形式化的驗證，保證翻譯的正確性。該項目將Lustre語言使用Coq工具定義與驗證，由于Lustre語言到C語言跨度較大，因此該項目將劃分成多個階段，保證每個階段語法或語義跨度不大，用來解決特定的問題。實際上在證明過程中，我們發(fā)現(xiàn)本質(zhì)的問題是無法回避的，但是如果問題疊加在一起，證明的難度將大大增加。圖1是L2C項目的階段圖，L2C項目的Lustre語義參考了Lustre v6標準，翻譯經(jīng)歷多個階段，分別是靜態(tài)檢

圖1 L2C項目階段

本文的工作是處于folding層，即將多層周期折疊到一個周期，同時消去時態(tài)算子，本層的工作相對獨立又非常關(guān)鍵，解決Lustre語言的時態(tài)特性，因此翻譯相對簡單，但是語義跨度較大，證明難度較大，證明是采用構(gòu)造的方法將中間信息完整的同步到語義分支，并最終完成證明。Lustre語言向C語言翻譯的一大障礙就是Lustre的時態(tài)特性，這決定Lustre向C翻譯的可能性。本文的工作就是將經(jīng)過簡化的Lustre語言的時態(tài)特性去掉，即消除Lustre的時鐘周期特性，同時還有Lustre的時態(tài)操作運算，最終證明時態(tài)消去的可行性。

2 Lustre的時鐘周期特性

Lustre語言的一個重要特性就是Lustre具有時鐘特性，即Lustre語言是一個流語言，具有周期性，并且可以對周期進行操作，比如可以求一個變量的前一個周期的值，而且操作可以互相疊加，因此任意前n個周期的值都是可以求得的，在時鐘特性疊加上函數(shù)調(diào)用就會使得程序比較復雜，但是這在L2C項目S－Lustre＊到Lustre－中已經(jīng)由化簡得到解決。在Lustre－中的變量的表現(xiàn)形式及時態(tài)操作運算可以在圖2中看到，x在不同周期值可以不同，是一個流數(shù)據(jù)，arrow操作可以在第一周期賦予表達式不同的值，fby的操作相當于整體往后平移一個周期。

圖2 時鐘變量及操作

3 Lustre－到LustreF翻譯及證明

下面給出Lustre－到LustreF形式化定義和證明的具體做法，為了描述的方便，我們使用M代替Lustre－，F(xiàn)代替LustreF。

3.1 Lustre－和LustreF程序示例

圖3 中是M程序的示例，定義了兩個節(jié)點arrowcall和fbycall，節(jié)點中分別使用了arrow和fby的時態(tài)操作運算。在arrowcall節(jié)點中，輸出值y在第一周期的值是0，在后續(xù)周期中的值等于輸入變量x的值。在fbycall中，輸出值z完全等于輸入值x，輸出值y第一周期值為0，第二周期值為第一周期x的值，第n周期值為第n－1周期x的值：

圖3 Lustre程序示便

圖4 是圖3的M程序翻譯對應的F程序，在F中新增加了標志位flagid，每個節(jié)點node都有一個flagid，用于區(qū)別是否是第一周期，flagid第一周期為false，后續(xù)為true，F(xiàn)中節(jié)點的調(diào)用意義與M是不同的，M是無限流程序，F(xiàn)中對應的就是一個無限循環(huán)調(diào)用，負責調(diào)用節(jié)點的外圍程序一般調(diào)用方法如下：

while（true）

｛

call arrowcall；

call fbycall；

｝

并且在調(diào)用之前將會將flagid初始為false。

在圖4中，變量p需要特別注意，變量p在最后賦值后，下一輪新的循環(huán)開始時，p的值相當于x前一周期的值，從而p起到了 “緩存”的作用，我們稱p是自定義變量。

3.2 Lustre－和LustreF的語法和語義

M是經(jīng)過簡化的Lustre，一個完整的M程序主要包含一系列的節(jié)點node和指定的主節(jié)點node名，主函數(shù)作為最初的入口函數(shù)，其它節(jié)點可以被調(diào)用。節(jié)點node主要包含參數(shù)，返回值，及函數(shù)主體，函數(shù)主體是有一系列的等式構(gòu)成，在M中，等式列表中的每個等式都是簡化的，僅包含兩種基本情況，簡單表達式的賦值和函數(shù)調(diào)用。

圖4 LustreF程度示例

簡單表達式可以大概的分為兩種情況，一種是非時態(tài)操作的表達式，包含基本原子，基本原子是指bool、int、real、char等常值或變量，一些基本的運算操作，比如一元運算，二元運算，數(shù)據(jù)結(jié)構(gòu)，比如結(jié)構(gòu)體，數(shù)組，選擇表達式，比如if和case，這些表達式是當前時鐘當前環(huán)境操作，一種是時態(tài)操作的表達式，在M中包含arrow和fby兩個基本操作，并且操作的元素都是基本原子單元。

F的語法與M的大部分相同，但是沒有arrow和fby兩個操作，但是在后面可以看到，在新定義的環(huán)境下他們的意義將是一樣的。這樣就是在等價的情況下，去掉了Lustre中時態(tài)的部分。

M的語義是用操作語義的形式定義的，在語法基礎上進行定義，即判斷每一條語法規(guī)則所定義內(nèi)容的語義值，在M的語法大大簡化的情況下，M的語義相對比較簡單，但由于時態(tài)的關(guān)系，M的環(huán)境仍然是比較復雜的，需要定義保存歷史信息的時態(tài)環(huán)境。

M環(huán)境的由全局環(huán)境，局部環(huán)境組成，每一個節(jié)點在每一個周期對應一個局部環(huán)境。全局環(huán)境存儲所有節(jié)點node列表，可以通過函數(shù)名在全局環(huán)境中查找具體的函數(shù)。

M局部環(huán)境包含時態(tài)環(huán)境和子環(huán)境。本地環(huán)境存儲一個節(jié)點中當前周期的局部變量的信息，這些變量是不重復的，存儲的過程也不會出現(xiàn)覆蓋的情況，存儲的結(jié)構(gòu)體的性質(zhì)也是經(jīng)過證明的，保證存和取的都是正確的值，時態(tài)環(huán)境存儲運行至當前周期時所有的本地環(huán)境，因此時態(tài)環(huán)境是一個不斷增加的流序列。子環(huán)境按照順序?qū)⒈徽{(diào)用函數(shù)的環(huán)境依照鏈式結(jié)構(gòu)保存下來，節(jié)點中被調(diào)用函數(shù)個數(shù)是n，子環(huán)境的鏈式結(jié)構(gòu)長度就是n，而且這個子環(huán)境的每個節(jié)點都是完整的環(huán)境，是遞歸定義的，因此整個局部環(huán)境是復雜的樹狀結(jié)構(gòu)。

F的環(huán)境與M不同的地方在于F沒有時態(tài)環(huán)境，只由本地環(huán)境和子環(huán)境組成。在F中，子環(huán)境需要保存函數(shù)調(diào)用的情況，因此所有函數(shù)的調(diào)用，以及被調(diào)用函數(shù)的函數(shù)體的信息都在子環(huán)境中定義。

在圖5中顯示了A調(diào)用兩次B，一次C，并且C調(diào)用B的情況下A的M的環(huán)境。A的環(huán)境包含歷史時態(tài)環(huán)境te，由本地環(huán)境的流序列構(gòu)成，當需要提取歷史信息時，可以通過這個te獲得，在本文中我們需要將這個te消除掉，折疊到一個本地環(huán)境。函數(shù)調(diào)用對環(huán)境定義的影響也是很大，e＊表示A的子環(huán)境，子環(huán)境也是一個序列，但是固定長度的序列，長度就是調(diào)用node的次數(shù)，調(diào)用兩次B，將會有兩個子環(huán)境成員，并且兩次B的局部環(huán)境和子環(huán)境都是包含在A的子環(huán)境中的，在被調(diào)用節(jié)點C中也可以調(diào)用其它node，比如C調(diào)用B，C的子環(huán)境將包含被其調(diào)用的B的環(huán)境，這些都組成了A的環(huán)境，可以在上面看到，A的環(huán)境是一個復雜并且很完整的信息。在M向F轉(zhuǎn)換的過程中其中的一個目標就是簡化這種樹狀環(huán)境，向C語言的扁平的環(huán)境靠攏。

圖5 環(huán)境定義演示

其中arrow和fby的具體語義形式可以在圖6中清楚看到，eh表示本地環(huán)境，對于arrow來說，第一周期情況下，arrow a1a2的值是a1的值，后續(xù)周期情況下是a2的值，對fby來說，fby a1a2的值，第一周期周期情況下為a1的值，后續(xù)周期情況下為前一周期局部環(huán)境下a2的值。

圖6 arrow和fby語義規(guī)則

圖7 簡示函數(shù)語義規(guī)則

圖7 中顯示的是F的函數(shù)定義的形式描述，函數(shù)調(diào)用的定義包含了外層調(diào)用初始化的情況，在第一周期情況下，第二步flagid初始化是循環(huán)外層保證的，下面的三步都是正常的函數(shù)調(diào)用的基本形式，根據(jù)輸入執(zhí)行函數(shù)體，得到輸出結(jié)果，第一步初始化的局部變量locals是M階段以前翻譯過程中形成的變量，在后續(xù)周期中，由于只是將局部變量locals初始化，新生成的自定義變量保存了上一個周期的值，fby的上一周期的值能從自定義變量這些 “緩存值”中得到，從而保證能夠從M翻譯到F中得語義等價，當然這些 “緩存值”在每一次循環(huán)中都是不停覆蓋的。

3.3 Lustre－與LustreF的翻譯

在前面提過M和F的語法相近，但是arrow和fby在語義相同的情況下被替換了，所以重點關(guān)注arrow和fby的翻譯，為此F的node的形式有了改變，引進兩種變量，一種是自定義變量，作為緩存變量存在，用來保存上個周期的值，一種是標志變量，區(qū)別是否是第一個周期。有了上面的知識，就可以進行arrow和fby的翻譯。

arrow的翻譯相對簡單，通過選擇表達式進行替換，標志變量是分支判斷條件，具體形式如下：

｜EarrowM a1a2＝＞

let flag＿atom：＝Avar flagid Tbool in

let clk＿desc：＝EifF flag＿atom a2a1in

let eq：＝EquationF（LhsID lid lty）（ExprF clk＿desc rty）in

（pid，nil，eq，nil）

arrow雖然是時態(tài)操作運算，但實際上并不會需要歷史周期的值，所以翻譯也較為簡單，使用EifF語句替換即可。

fby需要保存上一周期值，因此有兩個等式來對應翻譯，具體如下翻譯：

｜EfbyM a1a2＝＞

let flag＿atom：＝Avar flagid Tbool in let pre＿atom：＝Avar pid lty in

let pre＿var：＝VarDeclL pid lty in

let desc1：＝EifF flag＿atom pre＿atom a1in

let eq1：＝EquationF（LhsID lid lty）（ExprF desc1 rty）in

let eq2：＝PequationF（LhsID pid lty）a2in

（Nextpid pid，pre＿var：：nil，eq1，eq2：：nil）

fby需要歷史周期的值，所以除了使用EifF語句替換外，還要保存歷史周期的值pre＿var。其中第二類等式eq2是特殊等式PequationF，將放在所有其它等式的后面，作為一種新的等式形式，形成的這種新的等式列表的作用主要是用來保存上一個周期的值，這樣的翻譯也帶來了證明的困難，翻譯不再是線性的到線性的對應翻譯，而是線性的翻譯到兩段隔開的程序，因此在證明這種非線性映射的需要使用構(gòu)造的方法，利用構(gòu)造的定義來描述分割的程序的性質(zhì)，將在證明階段給出。

3.4 語義等價的標準

在L2C項目整個翻譯的過程中我們進行了多個階段的分層劃分，對于等價的定義我們有比較統(tǒng)一的做法，就是要求程序在輸入值相同的情況下，輸出結(jié)果是一致的，這樣在外界調(diào)用node將會是一樣的效果，從而保證程序的等價。M的語義是一個無限流式的語義，自然在每個周期就會有一組程序輸出值，對應的，F(xiàn)的語義將定義成一個無限循環(huán)的程序語義，每次循環(huán)也將給出一組輸出值，然后輸入值相同的情況下，M正確執(zhí)行后的輸出值為vrets，推出F正確執(zhí)行并且輸出值為vrets。

語義等價的標準的確定，就是證明目標的確立，證明的過程就從此目標開始一步步證明，因此，等價的標準需要仔細考量，我們對于翻譯中統(tǒng)一的標準的也是經(jīng)過推敲考慮的，一是可以通過這個目標逐步細化到具體的語義定義，第二是能夠清楚的反映Lustre程序的特性。具體語義等價的形式如下：

Theorem trans＿programM＿correct：

forall eM eF mainM mainF vargss vretss maxn，

initial＿stateM progM eM mainM－＞

initial＿stateF progF eF mainF－＞

iter＿exec＿programM progM mainM eM 1（S maxn）vargss vretss－＞

iter＿exec＿programF progF mainF eF 1maxn vargss vretss.

這是全時鐘周期的等價形式，當化歸為每一周期的估值函數(shù)時，F(xiàn)中語義的周期數(shù)被消除，同時F的語義也消除了時態(tài)操作運算?？梢栽谡Z義等價定義中看到M中的語義是 （S maxn）（即maxn＋1）周期的，而F是執(zhí)行maxn次的，我們是使用有窮的列表反映周期運行的，在前提對任意maxn而言，既有 （∞＋1）對應∞，具體原因在證明中描述。

3.5 語義等價的證明

上文描述的語義和語義等價是證明的基礎，也是問題本質(zhì)的描述，接下來就是機械化的邏輯證明，而證明的部分也是工作量主要體現(xiàn)的部分和全文難點所在。邏輯證明的過程是分拆的過程，將一些困難的不是顯然的大定理拆分成比較容易理解的小定理，證明的過程也是分析的過程，將具體的語義代入到翻譯過程中，通過邏輯上推理得出翻譯是否正確，證明的最終將分解成最簡單的邏輯判斷，比如判斷id是否相同，結(jié)論與條件是否一樣等等，而這些都是顯而易見的，也是邏輯的基礎，Coq也提供了很多的庫文件可供使用，而且提供了很多實用的定理，合理的調(diào)用能大大的簡化證明的過程?？傊?，證明的方法可以總結(jié)為歸納和演繹，歸納是用歸納法從特殊證一般性質(zhì)，演繹是擴充推廣定理，使定理更有普適性，具體證明方法在下面所示。

3.5.1 周期分類證明

在語義中可以看到，M的語義對于第一周期和第二以后的周期是不同的，需要不同的證明處理方法，而第二以后的周期是類似的，證明也可以使用同樣的方法，通過這樣的觀察，我們將證明的過程分兩步走，第一步是證明第一周期翻譯的正確性，第二步是證明后續(xù)周期翻譯的正確性，第一周期的正確性證明所需的條件可以在初始化過程中得到，而第二周期后續(xù)的證明所缺的條件可以從第一周期中得到。第一周期的執(zhí)行的過程也是需要注意的，第一周期子環(huán)境長度隨著代碼執(zhí)行可能會增加 （碰到函數(shù)調(diào)用增加），其中一些小定理分拆的過程中就需要嚴格需要這類條件，因此在周期中都是需要仔細的尋找子環(huán)境長度這類條件。周期分類最大的作用是區(qū)分不同類周期時時態(tài)操作運算的前提條件，從而能夠成功抽取出不同的條件代入到定理中。

3.5.2 互歸納方法

在語義定義中，函數(shù)體執(zhí)行定義需要使用等式列表執(zhí)行定義，等式列表執(zhí)行定義調(diào)用了等式執(zhí)行定義，等式執(zhí)行定義可能調(diào)用了函數(shù)而包含了函數(shù)體執(zhí)行定義，所以語義定義是互歸納的方式定義的，證明也必須要用到最小互歸納原理，使用關(guān)鍵詞Scheme，即同時假定3個定理原有都是正確的情況下，每次增加特定定理的步長，得到特定定理的增量條件，然后進行證明。由于定理證明的條件較多，因此互歸納增量條件的同步問題是很重要并且富有挑戰(zhàn)性的問題，需要對于語義的確切執(zhí)行有很清楚的認識和預見，增量條件的同步性是很難一步到位的，一般來說，對于互歸納定義的互相調(diào)用次數(shù)相關(guān)，而這種互相調(diào)用次數(shù)最多可以到是n＊n（n是平行定義個數(shù)），所以需要在證明的過程中不斷的修改完善增量條件直至證明完成。

3.5.3 構(gòu)造伴隨式定義

在前面已經(jīng)說明arrow和fby的翻譯過程，M與F證明最大的困難來自描述一段代碼與對應在兩部分不同的位置的代碼的信息是一樣的，從而M中得一段代碼對應F中的一段代碼后還有額外的信息，因此在證明中關(guān)鍵是要找一個中間條件，將這額外的信息表述出來，并且傳遞到第二段代碼的證明中。將這個額外的信息傳遞下去就需要中間條件的定義，這個定義比較復雜，主體的思路是證明F與M的值匹配，這就需要求F的自定義變量在M中的對應表達式，然后再用M中的對應表達式與M中的值進行比對匹配證明，這個定義有兩個好處，第一是將F中的自定義變量求值轉(zhuǎn)換為M的表達式的求值，匹配的證明相對容易，第二是定義中間條件將證明的難度拆分開來，分部進行相對容易。而且這個定義也是必須的，缺少中間條件的分支證明條件由于信息缺失而不充分。

下面的伴隨式定義就是結(jié)合語義構(gòu)造的給出的解決中間條件問題的方法，而伴隨式也是增量條件之一，所以對于不同的定義對應不同的形式，由于F中新定義了一種特殊等式PequationF，所以這種等式不需要互歸納定義。

等式定義對應形式如下：

Definition prevar＿consistance＿peql（ehm ehf：localenvL）（peql：list pequationF）：Prop：＝

forall peq v，

In peq peql－＞

eval＿atomL ehm （atomOfpeq peq）v－＞

ehf！（pidOfpeq peq）＝Some（v，typeOfpeq peq）.

等式定義雖然對應的是當前周期的值，結(jié)合M函數(shù)體執(zhí)行定義可知，每次M的歷史環(huán)境都會增加一個，所以在下一周期中得到了前一個周期的值，這也是恰好能夠證明fby算子消去的關(guān)鍵！W函數(shù)執(zhí)行和子函數(shù)調(diào)用執(zhí)行對應形式采用互歸納定義，同時函數(shù)執(zhí)行定義對應形式調(diào)用等式定義對應形式。

這些伴隨式定義在證明的過程中起到了橋梁的作用，自然而然的會在使用的時候需要它們的很多性質(zhì)作為保證，所以如果定義復雜的伴隨式將會極大的增加證明的困難，這也是構(gòu)造的難點之一，因此伴隨式需要在基于語法語義和翻譯的觀察基礎上不停地簡化。

3.5.4 消除周期的代價

M時態(tài)周期的消除并不是沒有代價的，這加大了F中環(huán)境的定義信息，F(xiàn)的環(huán)境中包含了函數(shù)體的信息，這才能完成伴隨式函數(shù)定義和構(gòu)造。從而F中子環(huán)境定義比較復雜，保存了子函數(shù)調(diào)用的情況，而子函數(shù)調(diào)用在等式列表的位置是未知的，需要搜索才能得知，所以在證明的過程中還需要保證子環(huán)境與函數(shù)體信息的一致性匹配，為此專門定義了F的子環(huán)境調(diào)用函數(shù)的一致性匹配性質(zhì)，在證明的過程中始終貫穿了這個一致性匹配性質(zhì)，并且這個性質(zhì)對證明過程中函數(shù)調(diào)用情況的也提供了必要的條件信息。實際上最小互歸納原理的其中一個必要條件就是子環(huán)境與函數(shù)的一致性匹配。

3.5.5 周期的對應

大定理周期是 （maxn＋1）個 M周期對應F中maxn次循環(huán)，原因是M中fby時態(tài)運算操作中取前一個周期值的原子是不符合拓撲排序關(guān)系的，即EfbyM a1a2中得a2可能沒有在前面被賦值，而伴隨式又需要a2當前周期存在值，解決方法是加入下一個周期的函數(shù)執(zhí)行作為條件，下一個周期函數(shù)執(zhí)行時，對于前一周期的a2有值，而下一周期的前一周期即是當前周期隊尾，就滿足了伴隨式的條件，所以證明是兩個周期對應一次循環(huán)，即M的一二周期對應F的第一次循環(huán)，M的二三周期對應F的第二次循環(huán)，以此類推。

總之，證明的過程是個逐步細分的過程，證明的過程中直觀的判斷往往是正確的證明方向，但是也可能會在細節(jié)出現(xiàn)問題，這種情況就是直覺的疏忽錯誤導致的，也有可能對語義定義的理解雖然相同，但定義方法不同，使程序證明的難度加大，這都需要回溯修改，直至證明完成。證明的最終都是對語法語義的邏輯推理，因此語法語義也是重要和基礎的，是對程序運行的理解，而證明的過程是對理解的細化推理，而程序運行的復雜性也將加倍的反映在證明中。證明最重要的結(jié)果是邏輯上保證程序翻譯的等價性，從而在M程序執(zhí)行正確的情況下，保證F程序也會正確執(zhí)行，并輸出正確結(jié)果。

4 結(jié)束語

本文是從一個編譯器的時態(tài)翻譯層出發(fā)，演繹了使用Coq程序證明翻譯的一般方法，形式化證明了Lustre時態(tài)特性與C循環(huán)特性的一致性問題，從而保證了Lustre程序向C程序轉(zhuǎn)化過程中時鐘可消除的特點。本文使用Coq證明工具實現(xiàn)，Lustre－語法語義定義約140行，LustreF語法語義定義約170行，翻譯工作約100行，等價性的證明過程約2500行。

隨著計算機軟件業(yè)務發(fā)展，人們對軟件的安全可靠的標準越來越高，形式化定義與證明驗證為解決這個問題的提供了一個高標準的實現(xiàn)方法，能夠從程序本質(zhì)上進行邏輯推斷，從而達到高可靠性，而形式化的方法的工作量相對比較大，因為證明的工作需要從邏輯上遍歷程序執(zhí)行所有可能出現(xiàn)的情況，從而得出程序正確執(zhí)行的結(jié)論，因此在關(guān)鍵代碼上使用形式化驗證的方法能有效提高整個系統(tǒng)的可靠性。

［1］Pouzet M，Raymond P，Cohen A，et al.Synchronous objects with scheduling policies ［C］／／ACM International Conference on Languages，Compilers，and Tools for Embedded Systems.Springer，2009：11－20.

［2］Benveniste A，Caspi P，Edwards S A，et al.The synchronous languages 12years later［J］.Proceedings of the IEEE，2003，91 （1）：64－83.

［3］Papailiopoulou V，Seljimi B，Parissis I.Automatic testing of LUSTRE／SCADE programs ［J］.Model－Based Testing for Embedded Systems，2012，13：171－194.

［4］Dormoy F X.Scade 6：A model based solution for safety critical software development ［C］／／Proceedings of the 4th European Congress on Embedded Real Time Software，2008：1－9.

［5］Leroy X.Verified squared：Does critical software deserve verified tools？ ［J］.ACM SIGPLAN Notices.ACM，2011，46（1）：1－2.

［6］Paulin－Mohring C.Introduction to the Coq proof－assistant for practical software verification ［G］.LNCS 7682：Tools for Practical Software Verification.Berlin：Springer Berlin Heidelberg，2012：45－95.

［7］Bertot Y.A short presentation of Coq ［G］.Lecture Notes in Computer Science 5170：Theorem Proving in Higher Order Logics.Berlin：Springer Berlin Heidelberg，2008：12－16.

［8］Le Sergent T.SCADE：A comprehensive framework for critical system and software engineering ［G］.Lecture Notes in Computer Science 7083：Integrating System and Software Mode－ling.Berlin：Springer Berlin Heidelberg，2012：2－3.

［9］Morrisett G.Technical perspective a compiler’s story ［J］.Communications of the ACM，2009，52 （7）：106－106.

［10］Yang X，Chen Y，Eide E，et al.Finding and understanding bugs in C compilers［J］.ACM SIGPLAN Notices，2012，47（6）：283－294.

［11］Klein G，Elphinstone K，Heiser G，et al.SeL4：Formal verification of an OS kernel［C］／／Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles.ACM，2009：207－220.

［12］Blazy S，Leroy X.Mechanized semantics for the Clight subset of the C language ［J］.Journal of Automated Reasoning，2009，43 （3）：263－288.