操作系統(tǒng)形式化驗證實踐教程(1) - 證明第一個定理
形式化方法分為三個主要部分：系統(tǒng)建模(System Modeling)、形式規(guī)約(Formal Specification)和形式化驗證(Formal Verification)。
其中系統(tǒng)建模用形式化的模型來描述系統(tǒng)及其行為模式。建模完成后，需要用形式規(guī)約來精確描述建模出來的需求。有了規(guī)約，如何檢驗是否符合規(guī)約呢?這就需要形式化驗證方法。
形式化驗證方法主要分為兩類：一類是以窮盡搜索為基礎(chǔ)的模型檢測，另一類是以邏輯推理為基礎(chǔ)的演繹邏輯。相對于前者，后者既可以驗證有窮的狀態(tài)系統(tǒng)，也可以使用歸納法來處理無限狀態(tài)的問題。
演繹邏輯在早期發(fā)展很快，但是后來在大規(guī)模軟件驗證上成本較高，所以發(fā)展一直不快。但是，最近十幾年，以seL4為代表的操作系統(tǒng)和CompCert為代表的編譯器的正確性證明的完成，給形式化驗證帶來了重要的突破性進展。
這也帶來了兩大流派：seL4所使用的Isabelle/HOL工具和CompCert所使用的Coq工具。
Isabelle是基于Standard ML語言開發(fā)的，支持生成Standard ML, ocaml, Haskell和Scala語言的代碼。而Coq是基于ocaml語言的。
波瀾壯闊的操作系統(tǒng)級的驗證全景，我們后面會徐徐展開。做為一個落地的教程，我們千里之行始于足下，先從Isabelle/HOL工具的使用開始說起。
Isabelle/HOL簡介
Isabelle/HOL可以通過下面的網(wǎng)址下載和安裝：https://www.cl.cam.ac.uk/research/hvg/Isabelle/installation.html。支持Linux/mac/Windows平臺。
以Linux為例，我們可以先通過wget工具下載tar.gz包：
wget -c https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2020_linux.tar.gz
HOL是High Order Logic，即高階邏輯的縮寫。
廢話不多說，Isabelle封裝在jEdit中，有完整的集成開發(fā)環(huán)境。我們安裝好了之后直接打開看一眼：
有幾點不跟普通編程語言的不同之處：
- HOL的代碼以theory組織在一起
- theory之下有函數(shù)fun,值value, 有公式lemma, theorem等
- 當(dāng)我們把光標(biāo)放到lemma或theorem中時，發(fā)現(xiàn)系統(tǒng)可以自動幫我們做一些推理的驗證
- HOL代碼中大量使用非ASCII符號，可能給用慣了ASCII字符的程序員們帶來一定的不適應(yīng)，但是可讀性絕對比用ASCII表示要上一個層次
自動證明第一個定理
同其它編程語言類似，HOL也有自己的數(shù)據(jù)類型系統(tǒng)。我們先從最簡單的布爾類型開始。
HOL支持bool來表示布爾類型。用True表示真值，F(xiàn)alse表示假值。
取反為, 取交為
，取并為
。
下面我們寫一個求布爾交的函數(shù)。
交函數(shù)的輸入為兩個bool，輸出也是一個bool.
我們用"bool ? bool ? bool"來描述這個函數(shù)的類型。
“?”的輸入方法是用TeX值：<\Rightarrow>.
HOL語句要用字符串符號""來括起來，原理我們后面再講。
代碼邏輯上，除了輸入為True和True返回True之外，其它都返回False:
fun conj2 :: "bool ? bool ? bool" where
"conj2 True True = True"|
"conj2 _ _ = False"
下面高光時刻來了，我們來用Isabelle/HOL證明我們學(xué)習(xí)之旅中的第一個定理False與另一個布爾值取conj2操作，結(jié)果一定為False。
lemma conj_02: "conj2 False m = False"
apply(induction m)
apply(auto)
done
apply(induction m)和apply(auto)的作用是讓HOL自動幫我們推斷證明。
把光標(biāo)放到apply(auto)語句，我們從output窗口看到：
proof (prove)
goal (2 subgoals):
1. conj2 False True = False
2. conj2 False False = False
如圖所示：
趁熱打鐵，我們再寫一個練習(xí)下：
fun not2 :: "bool ? bool" where
"not2 True = False" |
"not2 False = True"
lemma not02 : "not2 x = (? x)"
apply(induction x)
apply(auto)
done
從有限到無限
恭喜大家，已經(jīng)學(xué)會證明有限情況下的定理證明了。但是這還不夠，我們還要能證明無限的情況。
下面我們就從有限的布爾類型，前進到自然數(shù)類型nat和整數(shù)類型int.
自然數(shù)的定義帶著濃濃的數(shù)學(xué)歸納法的味道。這里用到了求后繼函數(shù)Suc：自然數(shù)nat = 0 或 Suc nat。也就是說，自然數(shù)定義為0，Suc(0), Suc(Suc(0))...
有了這個定義，我們可以重新定義一個加法了：
fun add2 ::"nat ? nat ?nat" where
"add2 0 n = n" |
"add2 (Suc m) n = Suc(add2 m n)"
首先是0和n進行add2等于n，然后是m的后繼與n進行add2操作，等于m與n進行add2操作后再求后繼。
這么說有點抽象，我們來看例子。
第一個例子：add2 0 1，根據(jù)定義，這個就等于1。這個容易理解。
第二個例子：add2 1 2。1是Suc 0，于是這個式子為Suc(add2 0 2)，add2 0 2根據(jù)第一條定義式結(jié)果為2。
第三個例子：add2 2 3。2是Suc 1，于是式子為Suc(add2 1 3)，再遞推為Suc(Suc(add2 0 3)，結(jié)果為5.
這樣，通過這樣一種遞推關(guān)系，我們重新定義了加法。
那么，這個我們新定義的加法，歸納出來的加法，跟真實的加法是不是一致呢？我們寫個定理去進行自動證明：
lemma add_02: "add2 m n = m+n"
apply(induction m)
apply(auto)
done
下面是證明的結(jié)果：
proof (prove)
goal (2 subgoals):
1. add2 0 n = 0 + n
2. ?m. add2 m n = m + n ? add2 (Suc m) n = Suc m + n
根據(jù)兩個初始條件，有兩個子目標(biāo)需要證明：
第一個是初始條件，add2 0 n = 0+n。
第二個是基于后繼的遞推條件。
皮亞諾公理
上面的證明方法叫做歸納原理，也叫做皮亞諾第五公理。
我們來從頭看下這5條公理：
- 0是一個自然數(shù)
- 任何自然數(shù)n都有一個自然數(shù)Suc(n)作為它的后繼
- 0不是任何自然數(shù)的后繼
- 后繼函數(shù)是單一的，即，如果Suc(m)=Suc(n)，則m=n.
- 令Q為關(guān)于自然數(shù)的一個性質(zhì)。如果
- 0具有性質(zhì)Q
- 并且 如果自然數(shù)n具有性質(zhì)Q，則Suc(n)也具有性質(zhì)Q
- 那么所有自然數(shù)n都有性質(zhì)Q
在此基礎(chǔ)上，我們可以定義加法和乘法。
- 加法：對于任何自然數(shù)n和m：
- n + 0 = n
- 并且 n + Suc(m) = Suc(n + m)
- 乘法：對任何自然數(shù)n和m:
- n * 0 = 0
- n * Suc(m) = (n * m) + n
乘法的定理證明如下：
fun mul2 ::"nat ? nat ?nat" where
"mul2 0 n = 0" |
"mul2 (Suc m) n = n * m + n"
lemma add_02: "mul2 m n = m * n"
apply(induction m)
apply(auto)
done
求值
在過程中，難免有些值我們希望看到輸出結(jié)果，這時可以通過value語句來實現(xiàn)。
例：
value "Suc(0)"
輸出結(jié)果為：
"1"
:: "nat"
1為結(jié)果的值，nat是類型。
調(diào)用我們自己定義的函數(shù)也沒有問題：
value "add2 1 (Suc 4)"
輸出結(jié)果為：
"6"
:: "nat"
恭喜你，我們已經(jīng)在定理證明的世界里證明了第一個定理。
后面的路很長，坡也有點陡，我們繼續(xù)前進。
