堆棧機器簡單編譯器在Isabelle/HOL中的驗證

陳飛揚，徐文濤，孫紹山，朱 浩，錢振江

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

1 引言

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

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

本文基于Isabelle/HOL對堆棧機器的簡單編譯器進行形式化驗證，證明對于由算術(shù)類型表達式和布爾類型表達式構(gòu)成的語言，堆棧機器編譯器的正確性.

2 相關(guān)研究

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

3 編譯表達式簡介

3.1 表達式簡介

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

3.2 堆棧機器指令簡介

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

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

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

3.3 編譯器簡介

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

3.4 堆棧機器運行行為簡介

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

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

4.1 表達式形式化

因為算術(shù)表達式的條件表達式依賴布爾表達式，所以需要先形式化布爾表達式，如圖1所示.

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

為了得到表達式計算的結(jié)果，需要對兩類表達式的求值進行形式化，如圖3所示.

4.2 堆棧機器指令形式化

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

4.3 編譯器形式化

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

圖1 布爾表達式形式化

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

圖3 表達式求值形式化

4.4 處理器形式化

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

圖4 堆棧機器指令形式化

圖5 編譯器形式化

4.5 編譯器正確性證明

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

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

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

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

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

然后，證明編譯算術(shù)表達式的正確性. 同理，先證明算術(shù)表達式相關(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ù)表達式相關(guān)指令也能得到正確的值（定理2）.

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

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

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

圖6 處理器形式化

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

5 結(jié)語

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

圖8 證明結(jié)果