陳飛揚(yáng)，徐文濤，孫紹山，朱 浩，錢(qián)振江

（常熟理工學(xué)院 計(jì)算機(jī)科學(xué)與工程學(xué)院，江蘇 常熟 215500）

1 引言

堆棧機(jī)器（stack machine）是計(jì)算機(jī)科學(xué)的一種計(jì)算模型，它利用“后進(jìn)先出”的堆棧來(lái)存儲(chǔ)臨時(shí)變量，在執(zhí)行相關(guān)指令時(shí)，指令操作數(shù)從堆?！皬棾觥?，然后把計(jì)算結(jié)果“推進(jìn)”堆棧. 因?yàn)榇蟛糠炙阈g(shù)表達(dá)式可以較為容易地轉(zhuǎn)換為后綴表示法，所以用堆棧形式執(zhí)行部分高級(jí)語(yǔ)言的效率很高. 由于堆棧機(jī)器的特點(diǎn)，其編譯器（compiler）也相比其他結(jié)構(gòu)機(jī)器的編譯器要簡(jiǎn)單、快速.

形式化方法（formal methods）是用于計(jì)算機(jī)軟件工程和硬件工程的開(kāi)發(fā)和驗(yàn)證技術(shù). 基于數(shù)學(xué)分析，它有助于保證設(shè)計(jì)的可靠性和魯棒性. 如今，借助內(nèi)置的決策程序和定理證明器，越來(lái)越多的人開(kāi)始使用交互式定理證明（Interactive Theorem Proving）工具來(lái)對(duì)設(shè)計(jì)進(jìn)行形式化驗(yàn)證.

本文基于Isabelle/HOL對(duì)堆棧機(jī)器的簡(jiǎn)單編譯器進(jìn)行形式化驗(yàn)證，證明對(duì)于由算術(shù)類(lèi)型表達(dá)式和布爾類(lèi)型表達(dá)式構(gòu)成的語(yǔ)言，堆棧機(jī)器編譯器的正確性.

2 相關(guān)研究

目前在形式化領(lǐng)域，要驗(yàn)證模型的正確性，有不少定理證明器（theorem provers）可供使用，如Isabelle［1］、HOL-light［2］和HOL4［3］等. 較為相關(guān)的是許多操作系統(tǒng)安全驗(yàn)證，如Walker等人對(duì)UCLA Secure Data Unix內(nèi)核的驗(yàn)證［4］，Bevier博士對(duì)KIT的形式化驗(yàn)證［5-8］，由澳大利亞國(guó)家ICT實(shí)驗(yàn)室（NICTA）在2004—2006年實(shí)施發(fā)起的L4.verified項(xiàng)目［9］.

3 編譯表達(dá)式簡(jiǎn)介

3.1 表達(dá)式簡(jiǎn)介

為了便于模擬，把表達(dá)式分為兩類(lèi)：布爾類(lèi)型表達(dá)式由變?cè)⒊Ｔ?、布爾?lèi)型一元運(yùn)算符、布爾類(lèi)型二元運(yùn)算符構(gòu)成；算術(shù)表達(dá)式由變?cè)?、常元、算術(shù)類(lèi)型一元運(yùn)算符、算術(shù)類(lèi)型二元運(yùn)算符、條件表達(dá)式構(gòu)成.其中，條件表達(dá)式特指根據(jù)布爾表達(dá)式的真假，計(jì)算第一或第二個(gè)算術(shù)表達(dá)式的值.

3.2 堆棧機(jī)器指令簡(jiǎn)介

把堆棧機(jī)器的指令分為兩類(lèi)：布爾表達(dá)式相關(guān)的指令和算術(shù)表達(dá)式相關(guān)的指令.

布爾表達(dá)式相關(guān)的指令包括：（1）載入布爾類(lèi)型常量；（2）載入布爾類(lèi)型地址內(nèi)容；（3）對(duì)一個(gè)棧頂元素應(yīng)用布爾類(lèi)型一元運(yùn)算并以計(jì)算結(jié)果代替它；（4）對(duì)兩個(gè)棧頂元素應(yīng)用布爾類(lèi)型二元運(yùn)算并以結(jié)果代替它們.

算術(shù)表達(dá)式相關(guān)的指令包括：（1）載入算術(shù)類(lèi)型常量；（2）載入算術(shù)類(lèi)型地址內(nèi)容；（3）對(duì)一個(gè)棧頂元素應(yīng)用算術(shù)類(lèi)型一元運(yùn)算并以計(jì)算結(jié)果代替它；（4）對(duì)兩個(gè)棧頂元素應(yīng)用算術(shù)類(lèi)型二元運(yùn)算并以結(jié)果代替它們；（5）根據(jù)棧頂布爾類(lèi)型的值來(lái)決定選取兩個(gè)算術(shù)表達(dá)式中哪一個(gè)的值，如果為真則取第一個(gè)的值，反之取第二個(gè)的值.

3.3 編譯器簡(jiǎn)介

根據(jù)要生成的指令類(lèi)型，把編譯器分為布爾表達(dá)式編譯器和算術(shù)表達(dá)式編譯器. 對(duì)布爾類(lèi)型表達(dá)式，用布爾表達(dá)式編譯器把相關(guān)操作編譯為布爾表達(dá)式相關(guān)的指令，并存放于布爾表達(dá)式相關(guān)指令的指令表中. 同理，對(duì)于算術(shù)類(lèi)型表達(dá)式，用算術(shù)表達(dá)式編譯器把相關(guān)操作編譯為執(zhí)行算術(shù)表達(dá)式相關(guān)的指令，并存放于算術(shù)表達(dá)式相關(guān)指令的指令表中.

3.4 堆棧機(jī)器運(yùn)行行為簡(jiǎn)介

堆棧機(jī)器運(yùn)行需要依靠指令表、存儲(chǔ)器、堆棧3個(gè)部分. 處理器執(zhí)行指令表中的指令，存儲(chǔ)器保存表達(dá)式地址，堆棧存儲(chǔ)程序運(yùn)行時(shí)的數(shù)據(jù). 其中，存儲(chǔ)器堆棧用表來(lái)模擬，而對(duì)于布爾表達(dá)式相關(guān)的指令和算術(shù)表達(dá)式相關(guān)的指令，分別由兩個(gè)函數(shù)來(lái)模擬處理器的行為.

4 編譯器在Isabelle/HOL中的形式化

4.1 表達(dá)式形式化

因?yàn)樗阈g(shù)表達(dá)式的條件表達(dá)式依賴布爾表達(dá)式，所以需要先形式化布爾表達(dá)式，如圖1所示.

參照布爾表達(dá)式，形式化算術(shù)表達(dá)式，如圖2所示.

為了得到表達(dá)式計(jì)算的結(jié)果，需要對(duì)兩類(lèi)表達(dá)式的求值進(jìn)行形式化，如圖3所示.

4.2 堆棧機(jī)器指令形式化

同樣，先形式化布爾表達(dá)式相關(guān)的指令，再形式化算術(shù)表達(dá)式相關(guān)的指令，如圖4所示.

4.3 編譯器形式化

編譯器的行為可以用函數(shù)來(lái)模擬，根據(jù)表達(dá)式的類(lèi)型，分別用兩個(gè)函數(shù)來(lái)模擬編譯布爾表達(dá)式和算術(shù)表達(dá)式的行為，如圖5所示.

圖1 布爾表達(dá)式形式化

圖2 算術(shù)表達(dá)式形式化

圖3 表達(dá)式求值形式化

4.4 處理器形式化

為了驗(yàn)證編譯器的正確性，需要模擬處理器來(lái)執(zhí)行編譯過(guò)的表達(dá)式. 同樣，用兩個(gè)函數(shù)分別模擬處理器執(zhí)行布爾表達(dá)式相關(guān)指令的行為和處理器執(zhí)行算術(shù)表達(dá)式相關(guān)指令的行為，如圖6所示.

圖4 堆棧機(jī)器指令形式化

圖5 編譯器形式化

4.5 編譯器正確性證明

要證明編譯器的正確性，即證明處理器執(zhí)行編譯器編譯過(guò)的表達(dá)式能得到正確的值.

首先，證明編譯器編譯布爾表達(dá)式的正確性. 為了證明處理器能正確執(zhí)行編譯過(guò)的多條表達(dá)式，需要證明布爾表達(dá)式相關(guān)指令是可以合并的（引理1）.

引理1append_bool： "?bs. execute_bool （xs @ ys） s bs = execute_boolys s （execute_boolxs s bs）"

根據(jù)引理1，可以證明處理器執(zhí)行布爾表達(dá)式相關(guān)指令能得到正確的值（定理1）.

定理1correct_bool： "?bs. execute_bool （compile_bool e） s bs = （value_bool e s） # bs"

然后，證明編譯算術(shù)表達(dá)式的正確性. 同理，先證明算術(shù)表達(dá)式相關(guān)指令可以合并（引理2）.

引理2append_arith："? vs. execute_arith （xs @ ys） env s vs = execute_arithysenv s （execute_arithxsenv s vs）"

根據(jù)引理2和定理1，可以證明處理器執(zhí)行算術(shù)表達(dá)式相關(guān)指令也能得到正確的值（定理2）.

定理2correct_arith： "? vs. execute_arith （compile_arith e） env s vs = （value_arith e env s） # vs"

綜上，編譯器能正確編譯布爾表達(dá)式和算術(shù)表達(dá)式，完成編譯器正確性證明，引理1、定理1、引理2、定理2的證明過(guò)程見(jiàn)圖7.

最終的證明結(jié)果如圖8所示，“No subgoals!”表示證明完成.

圖6 處理器形式化

圖7 引理1、定理1、引理2和定理2的證明腳本

5 結(jié)語(yǔ)

本文借助定理證明器Isabelle/HOL，對(duì)布爾表達(dá)式和算術(shù)表達(dá)式、堆棧機(jī)器指令、編譯器、堆棧機(jī)器運(yùn)行行為進(jìn)行形式化，驗(yàn)證了堆棧機(jī)器簡(jiǎn)單編譯器的正確性. 目前對(duì)于編譯器形式化驗(yàn)證的工作較少，本文僅對(duì)堆棧機(jī)器的簡(jiǎn)單編譯器進(jìn)行驗(yàn)證，考慮到實(shí)際應(yīng)用中編譯器的復(fù)雜度，仍有大量的課題有待研究.

圖8 證明結(jié)果