形式化方法Ｄｅｓｉｇｎｗａｒｅ及其規約精化機理

摘要：介紹了一種新的支持算法設計自動化的形式化方法Designware，詳細分析了其理論基礎及規約精化機理，闡述了其半自動算法設計支撐系統，并結合一個開發實例展示了Designware的具體使用，給出了Designware的兩個實際應用項目，最后對Designware進行了評述。

關鍵詞：形式化方法Designware；規約精化；算法設計；高可信

中圖分類號：TP311．1文獻標志碼：A

文章編號：1001－3695(2008)03－0721－05

0引言

形式化方法是建立在嚴格數學基礎上的軟件開發方法，其重要目標是以一種嚴格的工程方法進行軟件開發，作為一種思想、方法、技術滲透到軟件開發的各個活動中去。在軟件開發的需求分析、規格說明、設計、編碼、系統集成、測試、文檔生成直至維護的各階段，凡是采用嚴格的數學語言、具有精確的數學語義的方法都稱為形式化方法[1]。統計表明，傳統的非形式化方法對軟件質量的保證具有一個難以逾越的頂點，而形式化方法的實踐證明形式化方法是提高軟件質量的重要途徑[2]。在從高層規范至最終實現的過程中，選用適當的、以形式化方法為基礎的工具進行輔助設計和驗證，對提高安全攸關系統的可信度有很大幫助。20 世紀90 年代以來，在國際上，形式化方法已成為軟件開發中重要的可信軟件技術之一[3]。形式化方法對軟件可信性的獲得和保證有著不可替代的作用。 但至今形式化方法在實際的高可信軟件的開發中仍不多見，基本處于實驗室的試驗階段，并且其使用者多是專家型用戶。軟件開發包括高可信軟件的開發，仍以非形式化軟件開發方法為主流[2]。因此，研究和應用形式化方法及以其為基礎的支撐工具是極有意義的一項工作。

目前公認的在實際開發中得到最成功應用的方法[4~6]是由美國Kestrel研究所D.R.Smith博士主持研究的Specware[7，8]、Designware[9，10]和Planware[11，12]。它們分別帶有支持軟件開發全過程的支撐系統，已成功應用于美國海軍調度系統、波音公司客機設計軟件[13，14]中。

這三種方法統一于同一個可機械化的形式化框架中，關注于軟件工程的各個方面：Specware主要涉及到形式化規約的構建；Designware關注于設計知識的管理及應用；Planware則用于構建特定調度領域的應用系統。由于篇幅所限，且算法設計是軟件開發中知識高度密集的創造性勞動，本文主要介紹Designware，特別是它的規約精化機理。

1形式化方法Designware

1．1理論基礎

1．1．1規約

規約采用代數方法描述，由基調(signature)和公理(axiom)兩部分組成。一個規約的基調定義了類(sort)和運算(op)的集合，它為描述對象、操作和屬性提供了詞匯表；公理給出了運算需要滿足的約束。

下面給出的是偏序的規約[10]，它引進了一個類E和一個定義在E上的中綴二元運算le；此外還包括自反性、傳遞性和反對稱性三條公理，對le的含義加以約束。

spec PartialOrder is

sort E

op _le_ : E， E→Boolean

axiom reflexivity is x le x

axiom transitivity is x le y ^ y le zx le z

axiom antisymmetry is x le y ^ y le xx = z

endspec

規約是進行問題求解的起點，它被看成是一個范疇。通過規約態射(morphism)可進行規約的求精，如態射PartialOrdertoInteger is{E→Integer，le→≤}可將偏序規約轉換為整數規約。利用該態射，偏序規約中的axiom x le x將轉換為整數規約中的axiom x≤x。通過import子句來支持規約的重用，對規約還可進行其他的操作，這些由Specware支持完成。

1．1．2Specware

Specware是Designware的基礎，它是Kestrel研究所為整合其前期開發的三個原型系統KIDS[15，16]、REACTO[17]、DTRE[18]的功能而開發的。在Specware中使用的語言是Slang(Specware language)[19]，它以高階邏輯和范疇論為基礎，支持形式化規約（包括高階規約、參數化規約等）的開發及從規約到可執行代碼的逐步求精，目標是Common Lisp或C++可執行程序代碼。在Slang中的頂層機制包括用于建立規約的規約(specifications)、態射、圖表(diagrams)、用于規約求精的解釋模式(interpretation schemes)及解釋模式態射(interpretation scheme morphisms)。對規約求精的過程就是在滿足公理的約束下通過各種機制對類和操作逐步具體化的過程。

為了支持規約的快速構建，Specware包含一大型的可重用規約庫，如包含整數、序列、棧、集合、數組等規約的基本數據類型規約庫，包含偏序、半群、向量空間等規約的基本數學結構規約庫等。

使用Specware開發程序的步驟是：a）形式化定義需求，通過功能抽象和數據抽象得到抽象的功能規約；b)在規約庫的支持下，對抽象規約求精構造具體的功能規約；c)通過引進算法對功能規約進行求精，得到抽象的設計規約；d)將抽象設計規約進行數據求精，得到具體的設計規約；e)將第d)步的結果轉換成不同的高級語言程序，再編譯成可執行的機器代碼。

1．1．3分類思想及規約精化機理

Designware是Specware在算法設計、數據求精、程序優化等算法設計自動化方面的擴充，它包含一個與特定領域無關的通用設計知識分類庫，并支持在此分類庫基礎上實施從規約到算法的求精開發[20，21]。

Designware能支持算法設計的關鍵是將抽象的設計知識，如數據的精化、算法設計、程序優化、軟件體系結構等表示成精化規則的形式（如表示成圖表態射），并加以存儲形成可重用設計知識精化庫。

為了能高效地應用設計知識，Designware將抽象的可重用精化庫組織成一個分類形式，使得設計者能方便地對精化庫進行訪問以及基于該庫來構建求精。在這里涉及到的關鍵思想是分類[22]，通過將設計知識分類，縮減了可選擇的實現集合的范圍，并且按照分類提供的順序進行逐步精化，將逐漸加強對設計的約束。

使用Designware開發算法的兩個關鍵問題是構建規約和精化。構建規約可以在Specware系統中完成，下面著重分析如何構建精化。

對規約S0求精的過程包含三個基本步驟：a)從精化庫中選擇一條精化AB；b)構建分類箭頭AS0；c)計算BAS0的外推S1，得到的精化結果是余錐(cocone)箭頭S0S1。這個基本的精化過程一直進行下去，直到規約中包含的相關類和操作的定義已經詳盡到可以很容易地轉換成可執行程序代碼為止。其中，構建分類箭頭AS0需要通過人機交互來完成。

圖1刻畫了分類庫中的精化應用于給定規約S0的過程[10]。首先從庫中選擇了精化AB；然后構建AS0的分類箭頭，這個過程通過顯式說明S0至少含有A的結構來完成，從而將S0歸于A結構類；接下來應用精化AB，計算外推S1。

使用Designware開發程序的步驟是，在Specware系統中完成具體的功能規約構造；然后由Designware對規約進行算法求精、數據求精及程序優化；再利用Specware完成代碼生成工作，即將上述Specware開發步驟中的第c）、d)步交由Designware來完成，將引進算法代之以設計算法。

1．2算法設計系統

Designware的目標是給算法設計者提供一個抽象、可重用的設計知識精化庫以及一些自動化操作，幫助設計者完成算法設計。

Designware包含的可重用設計知識分類庫中涉及算法設計、數據求精以及表達式優化技術等方面的設計知識，并將它們表示成精化規則的形式加以存儲。

對于算法設計知識分類庫，包含約束滿足問題（整數線性規劃、線性規劃）、全局結構（全局搜索、二分搜索、回溯、分支限界等）、局部結構（局部搜索、爬山法等）以及問題歸約求解（分治、動態規劃等）等算法模式分類。利用算法設計知識分類庫，可對規約進行算法求精。到目前為止，Kestrel研究所已經開發了一個較全面的算法設計知識分類(taxonomy)庫，如圖2所示[10]。節點描述各條精化的域(domain)，實際上也是規約；節點間的箭頭表示規約間的求精關系；每條精化規則按照節點建立索引，在每個節點處索引到的精化對應于一系列算法模式。在分類中，節點的位置層次越大，它對應的規約含有的約束就越多，包含的結構也越具體。概略地說，范圍窄卻高效的算法模式位于分類中的深層，而應用范圍廣的通用算法在較淺的層次。

對于數據求精分類庫，包含一些常用的數據結構并將它們之間的關系以精化形式表示，形成一些分類。圖3給出了容器類型的一個分類[10]，其組織方式與算法設計分類庫類似。

很多程序優化技術，如表達式化簡、有限差分(finite differencing)、情況分析（case analysis）、部分計值（partial evaluation）等，在Designware中也被描述成精化規則的形式，并且可像使用其他精化規則，如表示算法設計或數據求精的精化規則那樣應用于求精過程。

2實例研究

本文給出一個對存放于包中的數據進行排序的例子[23]，用于說明Designware的具體使用，同時展示其規約精化的機理。限于篇幅，這里僅對算法求精進行詳細闡述，相關的數據求精和程序優化未詳細給出。

首先通過Specware構建這個排序問題的規約，構建過程如圖4所示。其中：BAGANDSEQ是基本規約TRIV、BAG和SEQ的余極限(colimit)；BAGANDSEQCONV引入了BAGAND SEQ，可以看成是BAGANDSEQ的擴展；而BAGSEQLinOrd又是TRIV、LINEARORDER和BAGANDSEQCONV的余極限；BAGSEQoverLinOrd 包含了BAGSEQLinOrd，在此基礎上構建了規約sorting：

spec sorting is

import BagSeqoverLinOrd

op sorted?: Bag， Seq→Boolean

def sorted?(x，z)=(ordered?(z)∧x = seqtobag(z))

op sorting:Bag→Seq

axiom sorted?(x，sorting(x))

end_spec

圖5用于指導整個開發過程。首先應用一個分治（divideandconquer）精化；然后是數據求精（包被實現為序列）；接下來應用一條表達式化簡精化，……每一個方框表示一條精化的應用，求精的主線從規約sorting開始。

2．1算法求精

在使用算法設計知識之前，必須有一個定義良好的問題。問題理論(problem theory)表達了一個問題的抽象結構：給定輸入x:D，找一個可行解z:R，滿足問題的需求約束O(x，z)，如下所示：

spec problemtheory is

sorts D輸入域

R輸出域

op O:D，R→Boolean 輸出條件

endspec

假設用戶首先決定選擇分治類求精divideandconquer－01－2divideandconquer012scheme應用于初始規約，以期得到分治算法。在分類庫中，這條精化對應著的兩個節點分別描述如下：

首先給出的是divideandconquer012：

spec divideandconquer012 is

import DRO

sort E

op F: D→R

op _>_: D， D→Boolean

op p0:D→Boolean

op Odecompose0:D，Unit→Boolean

op Ocompose0:R，Unit→Boolean

axiom Soundness0 is

Odecompose0 (x，〈〉)∧Ocompose0(z，〈〉)O(x，z)

axiom discriminatorofdecompose0 is

p0(x) Odecompose0(x，〈〉)

op p1: D→Boolean

op Odecompose1:D，E→Boolean

op Ocompose1:R，E→Boolean

axiom Soundness1 is

Odecompose1(x，e)∧Ocompose1(z，e)O(x，z)

axiom discriminatorofdecompose1 is

p1(x) (e)Odecompose1(x，e)

op p2:D→Boolean

op Odecompose2:D，D，D→Boolean

op Ocompose2:R，R，R→Boolean

axiom Soundness2 is

Odecompose2(x0，x1，x2)∧O(x1，z1) ∧O(x2，z2)∧Ocompose2(z0，z1，z2)O(x0，z0)

axiom discriminatorofdecompose2 is

p2(x)(x1，x2)Odecompose2(x，x1，x2) ∧x>x1∧x>x2

axiom (x:D) p0(x) x or p1(x) x or p2(x)

endspec

它提供了一個二元分解(decomposei)操作以及對應的合并(composei)操作、分解關系（Odecomposei）以及合并關系（Ocomposei）；pi表示Odecomposei能夠將輸入分解的條件；這里的i可取0，1，2，分別表示包為空、只含單元素及兩元素以上這三種情況。Soundness2公理將O、Odecompose2和Ocompose2關聯在一起，它斷言如果:a)非原始實例x能被分解為兩個子問題實例x1和x2;b)子問題實例x1和x2分別有可行解z1和z2;c)z1和z2能合并組成z0，那么z0是輸入x0的一個可行解。其他的公理有類似的斷言。操作符>是D上的良序以保證算法的終止性，相應的公理被省略。

下面給出的是約束加強的規約divideandconquer012scheme。

spec divideandconquer012scheme is

import divideandconquer012

op C0:→R

axiom Ocompose0 (C0，〈〉)

op C1:E→R

axiom Ocompose1 (C1(e)，e)

op C2: R，R→R

axiom Ocompose2 (C2(x1，x2)，x1，x2)

definition of F is

axiom p0(x) Odecompose0(x，〈〉) ∧F(x)=C0

axiom p1(x)(e)(Odecompose1 (x，e)∧F(x)=C1(e))

axiom p2(x)(x1，x2)(Odecompose2 (x，x1，x2) ∧ F(x) = C2(F(x1)，F(x2))

enddefinition

theorem O(x，F(x))

endspec

它是divideandconquer012divideandconquer 012scheme精化的協域(codomain)，給出了頂層divideandconquer函數的示意性定義以及子算法C0、C1和C2的示意性需求規約。

排序分治算法的開發從構建問題理論到規約sorting的解釋problemtheorysorting開始：

D|→bag

R|→seq

O|→sorted?

因為從problemtheory到divideandconque012的態射是一個包含，所以可以直接構建分類箭頭divideandconquer012sorting 如下：

D|→bag

R|→seq

O|→sorted?

F|→?

E|→?

>|→?

p0|→?

Odecompose0|→?

Ocompose0|→?

……

為了完成這個分類箭頭，必須把剩余的算子變換成sorting中的表達形式，不同的變換會產生不同的排序算法。一種方法是基于從庫中選出的標準decomposition算子集合，然后對soundness公理使用unskolemization操作，推導出composition算子的規約。這種方法會推導出插入排序、合并排序以及多種并行排序算法；另一種方法是從庫中選出標準composition算子集合，再利用soundness公理推導出decomposition算子的規約，這會導致選擇排序、堆排序及快速排序算法的產生。在這個例子中采用前一種方法。

假設選出構建集合{emptybag， singletonbag， bagunion}作為輸入域bag上decompositon關系的基礎，那么能得到如下的部分分類箭頭：

D|→bag

R|→seq

O|→sorted?

F|→sorting

E|→E

>|→bagwfgt

p0|→emptybag?

Odecompose0|→λ(x)x=emptybag

Ocompose0|→?

p1|→singletonbag?

Odecompose1|→λ(x，e)x= singletonbag(e)

Ocompose1|→?

p2|→nonsingletonbag?

Odecompose2|→(x0，x1，x2) x0= bagunion(x1，x2)

Ocompose2|→?

由于此時Ocompose2還沒有完成變換，soundness2公理(x0，x1，x2:D)(z0，z1，z2:R)(Odecompose2(x0，x1，x2) ∧O(x1，z1) ∧O(x2，z2)∧Ocompose2 (z0，z1，z2)O(x0，z0))也不能變換成sorting中的定理。此時使用unskolemization操作，引進一個新的在z0，z1，z2約束范圍內的存在量詞變量y：

( z0，z1，z2:R)(y:Boolean)(x0，x1，x2:D)(Odecompose2 (x0，x1，x2)∧O(x1，z1) ∧O(x2，z2)∧y  O(x0，z0))

這個公式與原來的公式有同樣的可滿足屬性，運用前面得到的部分分類箭頭，有

( z0，z1，z2:seq)(y:Boolean)(x0，x1，x2:bag)

(x0=bagunion (x1，x2)∧sorted?(x1，z1) ∧sorted?(x2，z2) ∧ y sorted?(x0，z0))

接下來通過證明這個式子成立可為y找到具體的表達式：

sorted? (x0，z0)=

{sorted?的定義}ordered(z0) ∧x0= seqtobag(z0)=

{假設x0=bagunion(x1，x2)}

ordered(z0) ∧bagunion(x1，x2)=seqtobag(z0) =

{假設xi=bagunion (zi)，i=1，2}

ordered(z0)∧bagunion(seqtobag(z1)，seqtobag(z2)) =

seqtobag(z0)

由于y必須是一個由變量z0，z1，z2定義的項，為了使soundness2公理成立，運用上面對sorted? (x0，z0)展開得到的結果，得到

Ocompose2 |→λ( z0，z1，z2)ordered(z1) ∧ordered(z2)

ordered(z0)∧bagunion(seqtobag(z1)，seqtobag (z2)) =

seqtobag(z0)

這實際上就是一個合并操作的規約。如果用這個規約作為Ocompose2的翻譯結果，那么soundness2公理也就相應地通過構建的分類被翻譯成sorting中的定理。

上述分類箭頭的其他未完成部分按類似步驟進行構建。最后得到的完整分類箭頭divideandconquer012sorting如下：

D|→bag

R|→seq

O|→sorted?

F|→sorting

E|→E

>|→bagwfgt

p0|→emptybag?

Odecompose0|→λ(x)x=emptybag

Ocompose0|→λ(z)z=emptyseq

p1|→singletonbag?

Odecompose1|→λ(x，e)x= singletonbag(e)

Ocompose1|→λ(z，e)z= singletonseq(e)

p2|→nonsingletonbag?

Odecompose2|→λ(x0，x1，x2)x0= bagunion(x1，x2)

Ocompose2|→λ( z0，z1，z2)ordered(z1) ∧ordered(z2)ordered(z0)∧seqtobag(z0)=bagunion(seqtobag(z1)， seqtobag(z2))

在這個分類箭頭的基礎上，如圖6所示，通過計算外推來獲得sorting的一個精化sortingAlg1。它包含了一個合并排序的定義，如下所示：

spec sorting Alg1 is

import BagSeqoverLinOrd

op sorted?: Bag，Seq→Boolean

definition sorted?(x，z)=(ordered?(z)∧x=seqtobag(z))

op sorting: Bag> Seq

theorem sorted?(x， sorting(x))

definition of sorting is

axiom emptybag?(x)(x=emptybag∧sorting(x)=C0)

axiom singletonbag?(x)(e)(x=singletonbag(e) ∧sorting(x)=C1(e))

axiom nonsingletonbag?(x)(x1，x2)(x=bagunion (x1，x2)∧sorting(x)=C2(sorting(x1)， sorting(x2)))

enddefinition

op C0:→Seq

axiom C0=emptyseq

op C1:E→Seq

axiom C1(e)=singleton(e)

op C2:Seq，Seq→Seq

axiom ordered?(z1)∧ordered?(z2)(ordered?(C2(z1，z2)) ∧ seqtobag(C2(z1，z2)) = bagunion(seqtobag(z1)， seqtobag (z2)))

endspec

2．2數據求精及程序優化

如果要使合并排序算法更接近實現，還需要對其進行數據求精。算法設計和數據求精之后得到的算法中有很多子表達式往往可以進行優化，即程序優化。等式重寫(equational rewriting)、上下文相關的簡化(contextdependent simplification)、有限差分(finite differencing)、部分計值(partial evaluation)等變換規則和優化策略的應用能使最后算法實現復雜度的大幅度降低。這些優化技術可以被表示成精化規則的形式，并與應用算法設計和數據

求精知識的精化規則類似的方式加以應用。限于篇幅，此處將不再贅述。

3應用項目

這里簡單介紹了Kestrel研究所使用Designware及其精化技術開發的兩個應用項目[10]。

3．1任務調度系統(mission planning system，MPS)

大型貨物運輸任務的規劃問題是世界上最復雜的調度問題之一。它涉及到同時調度如飛機、工作人員等一系列資源及燃料等支撐資源的問題，還包括路程安排及外交方面的問題。Kestrel研究所已經為美國空軍開發了一個滿足很多需求的任務規劃系統(MPS)原型。其主要算法的開發就是在Designware的基礎上通過修改需求規約并運用算法設計分類知識、數據求精及優化策略來進行的。到目前為止，還沒有比這個更復雜的算法能夠在這么高的自動化程度下從規約開始通過形式化開發得到。

3．2Planware

Planware是Specware/Designware在運輸規劃和調度問題領域的特定應用，是一個專門產生調度算法的綜合系統。它以Specware/Designware為基礎，增加了關于調度知識方面的理論和精化規則庫以及控制這些設計知識應用的特殊策略。其領域語言涉及到資源、任務、預定等術語及其屬性。其中任務和資源的主要區別在于任務不能提供服務，而需要資源的服務。Planware使用精化規則庫把從用戶那里獲取的信息變換到形式化的需求規約，這通常是一個幾千行的規約文本。在Planware中經算法設計、數據求精及表達式優化等步驟將規約求精到代碼的過程完全自動化。使用Planware時，用戶只要執行一些簡單的操作，根據實際問題從資源類型分類中選取資源的類型，然后在系統提供的表格界面中為任務和資源選擇約束條件，將每一個域限定在恰當的值內。Planware使用這張表來構建面向特定領域的刻畫待求解問題的形式化規約，并且使用該規約作為構建調度算法的起點，整個過程無須用戶再進行輸入。最后得到的輸出是一個領域相關的調度程序，在給定一個具體的調度請求集合時將會輸出一個正確有效的調度方案。

4結束語

由于涉及到創造性工作，開發算法程序仍然是計算機科學領域中最具挑戰性的問題之一。算法程序設計的自動化對提高軟件可信度具有重要的作用，其最終目標是構建支持算法程序設計的系統。該方向越來越受到計算機科學工作者的關注，有關的大量工作正在展開。

本文介紹的形式化方法Designware及其算法設計系統是Kestrel研究所在算法設計自動化方面作出的研究。它將設計知識表示成求精形式并分類存放在數據庫中，借助范疇論工具進行逐步求精式的算法自動化設計。到目前為止，Designware中的精化規則主要集中在描述算法、數據以及優化方面的設計知識上。

通過前面的分析及實例可以看出[24]，Designware的算法設計系統不是完全自動化的，它依賴于與專家級用戶間的交互；作為問題求解起點的規約實際上是代數規約，使用起來很不方便，要求用戶具有相當多的數學知識；在其算法設計分類庫中，存放著與不同算法設計策略對應的不同程序模式，當遇到一個待求解的實際問題時，到底選用哪種合適的算法設計策略來解決問題并沒有一個有效的標準或規則，需要具有較多算法設計知識的用戶來交互選取，這給提高算法設計自動化的程度帶來困難；甚至于優化，用戶也必須知道程序的哪個部分可以用什么方法來進行優化，從而選定需要優化的表達式及恰當的優化規則。

盡管存在上述種種不足， Designware方法無疑在算法設計自動化方面進行了較成功的探索，以其為基礎的支撐工具已在實際開發中發揮了不容置疑的作用，對促進形式化方法在工程界的使用以及軟件自動化的研究具有重大意義，進一步提升了形式化方法及自動化工具在軟件工程中發揮的實際效力。

參考文獻：

［1］鄒盛榮，鄭國梁. B語言和方法與Z、VDM的比較[J]. 計算機科學，2002，29(10):136138.

[2]陳火旺，王戟，董威.高可信軟件工程技術[J].電子學報，2003，31(12A): 19331938.

[3]High Confidence Software and System Coordinating Group. High confidence software and systems research needs[EB/OL].(20010110).http://www.nitrd.gov/pubs/hcss research.pdf.

[4]UPSON S.Computer software that writes itself [N].Newsweek International，200512－26.

[5]ANTHES G H.In the labs:automatic code generators [N].Computer World， 2006－03－20.

[6]McLAUGHLIN L.Automated programming the next wave of developer power tools[J].IEEE Software，2006，5(6)：91－93.

[7]McDONALD J，ANTON J.Specwareproducing software correct by construction KES.U.04.03[R].[S.l.]:Kestrel Institute，2004.

[8][EB/OL].（2007－02）.http://www.specware.org/.

[9]SMITH D R.Designware:software development by refinement[C]//Proc of the 8th Int’l Conf on Category Theory and Computer Science (CTCS’98).Edinburgh:[s.n.]，1999.

[10]PAVLOVIC D，SMITH D R.Software development by refinement[C]//Proc ofthe 10th UNU/IIST Anniversary Colloquium， Formal Methods at the Crossroads: From Panaea to Foundational Support， LNCS 2757.[S.l.]:SpringerVerlag，2003:267－286.

[11]BLAINE L，GILHAM L，LIU J，et al.Planware:domainspecific synthesis of highperformance schedulers[C]//Proc of the 13th Automated Software Engineering Conference.Los Alamitos， California:IEEE Computer Society Press，1998:270－280.

[12]BECKER M，GILHAM L，SMITH D R.Planware II:synthesis of schedulers for complex resource systems， KES.U.03.04[R].[S.l.]:Kestrel Institute，2003.

[13]MARTIN W B，WHITE P D，TAYLOR F S.Creating high confidence in a separation kernel [J].Automated Software Engineering，2002，9(3): 263－284.

[14]WILLIAMSON K.Systems synthesis:towards a new paradigm and discipline for knowledge， software， and system development and maintenance[R].[S.l.]:Mathematics and Computing Technolgy， Boeing Phantom Works，2001.

[15]SMITH D R.KIDS:a knowledgebased software development system [C]//LOWRY M，McCARTNEY R.Automating Software Design.[S.l.]:MIT Press， 1991:483－514.

[16]SMITH D R.KIDS:a semiautomatic program development system [J].IEEE Trans on Software Engineering:Special Issue on Formal Methods，1990，16(9):10241043.

[17]WANG Tiecheng，GOLDBERG A.A mechanical verifier for supporting the design of reliable reactive systems[C]//Proc of International Symposium on Software Reliability Engineering.Austin:[s.n.]，1991.

[18]BLAINE L，GOLDBERG A.DTRE:a semiautomatic transformation system [C]//MLLER B.Constructing Programs from Specifications.North Holland:[s.n.]，1991.

[19]Kestrel Institute，Kestrel Development Corporation. Specware language manual[R].1998.

[20]SMITH D R.Generating programs plus proofs by refinement[C]//Proc of IFIP Working Conference on Verified Software:Theories，Tools，Experiments.Zurich:[s.n.]，2005.

[21]KREMANN T W，MARTIN W B，TAYLOR F S.An avenue for high confidence applications in the 21st century[C]//Proc of the 22nd National Information Systems Security Conference.1999.

[22]SMITH D R.Toward a classification approach to design[C]//Proc of the 5th Int’l Conf on Algebraic Methodology and Software Technology，AMAST’96，LNCS 1101.[S.l.]:SpringerVerlag，1996.

[23]SMITH D R.Mechanizing the development of software[C]//BROY M.Calculational system design.Amsterdam: NATO ASI Series， IOS Press，1999.

[24]SCHMID U.Inductive synthesis of functional programs[M].[S.l.]:SpringerVerlag，2003.

“本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文”