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

摘要：介紹了一種新的支持算法設(shè)計自動化的形式化方法Designware，詳細(xì)分析了其理論基礎(chǔ)及規(guī)約精化機(jī)理，闡述了其半自動算法設(shè)計支撐系統(tǒng)，并結(jié)合一個開發(fā)實例展示了Designware的具體使用，給出了Designware的兩個實際應(yīng)用項目，最后對Designware進(jìn)行了評述。

關(guān)鍵詞：形式化方法Designware；規(guī)約精化；算法設(shè)計；高可信

中圖分類號：TP311．1文獻(xiàn)標(biāo)志碼：A

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

0引言

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

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

這三種方法統(tǒng)一于同一個可機(jī)械化的形式化框架中，關(guān)注于軟件工程的各個方面：Specware主要涉及到形式化規(guī)約的構(gòu)建；Designware關(guān)注于設(shè)計知識的管理及應(yīng)用；Planware則用于構(gòu)建特定調(diào)度領(lǐng)域的應(yīng)用系統(tǒng)。由于篇幅所限，且算法設(shè)計是軟件開發(fā)中知識高度密集的創(chuàng)造性勞動，本文主要介紹Designware，特別是它的規(guī)約精化機(jī)理。

1形式化方法Designware

1．1理論基礎(chǔ)

1．1．1規(guī)約

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

下面給出的是偏序的規(guī)約[10]，它引進(jìn)了一個類E和一個定義在E上的中綴二元運(yùn)算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

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

1．1．2Specware

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

為了支持規(guī)約的快速構(gòu)建，Specware包含一大型的可重用規(guī)約庫，如包含整數(shù)、序列、棧、集合、數(shù)組等規(guī)約的基本數(shù)據(jù)類型規(guī)約庫，包含偏序、半群、向量空間等規(guī)約的基本數(shù)學(xué)結(jié)構(gòu)規(guī)約庫等。

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

1．1．3分類思想及規(guī)約精化機(jī)理

Designware是Specware在算法設(shè)計、數(shù)據(jù)求精、程序優(yōu)化等算法設(shè)計自動化方面的擴(kuò)充，它包含一個與特定領(lǐng)域無關(guān)的通用設(shè)計知識分類庫，并支持在此分類庫基礎(chǔ)上實施從規(guī)約到算法的求精開發(fā)[20，21]。

Designware能支持算法設(shè)計的關(guān)鍵是將抽象的設(shè)計知識，如數(shù)據(jù)的精化、算法設(shè)計、程序優(yōu)化、軟件體系結(jié)構(gòu)等表示成精化規(guī)則的形式（如表示成圖表態(tài)射），并加以存儲形成可重用設(shè)計知識精化庫。

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

使用Designware開發(fā)算法的兩個關(guān)鍵問題是構(gòu)建規(guī)約和精化。構(gòu)建規(guī)約可以在Specware系統(tǒng)中完成，下面著重分析如何構(gòu)建精化。

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

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

使用Designware開發(fā)程序的步驟是，在Specware系統(tǒng)中完成具體的功能規(guī)約構(gòu)造；然后由Designware對規(guī)約進(jìn)行算法求精、數(shù)據(jù)求精及程序優(yōu)化；再利用Specware完成代碼生成工作，即將上述Specware開發(fā)步驟中的第c）、d)步交由Designware來完成，將引進(jìn)算法代之以設(shè)計算法。

1．2算法設(shè)計系統(tǒng)

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

Designware包含的可重用設(shè)計知識分類庫中涉及算法設(shè)計、數(shù)據(jù)求精以及表達(dá)式優(yōu)化技術(shù)等方面的設(shè)計知識，并將它們表示成精化規(guī)則的形式加以存儲。

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

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

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

2實例研究

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

首先通過Specware構(gòu)建這個排序問題的規(guī)約，構(gòu)建過程如圖4所示。其中：BAGANDSEQ是基本規(guī)約TRIV、BAG和SEQ的余極限(colimit)；BAGANDSEQCONV引入了BAGAND SEQ，可以看成是BAGANDSEQ的擴(kuò)展；而BAGSEQLinOrd又是TRIV、LINEARORDER和BAGANDSEQCONV的余極限；BAGSEQoverLinOrd 包含了BAGSEQLinOrd，在此基礎(chǔ)上構(gòu)建了規(guī)約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用于指導(dǎo)整個開發(fā)過程。首先應(yīng)用一個分治（divideandconquer）精化；然后是數(shù)據(jù)求精（包被實現(xiàn)為序列）；接下來應(yīng)用一條表達(dá)式化簡精化，……每一個方框表示一條精化的應(yīng)用，求精的主線從規(guī)約sorting開始。

2．1算法求精

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

spec problemtheory is

sorts D輸入域

R輸出域

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

endspec

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

首先給出的是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)操作以及對應(yīng)的合并(composei)操作、分解關(guān)系（Odecomposei）以及合并關(guān)系（Ocomposei）；pi表示Odecomposei能夠?qū)⑤斎敕纸獾臈l件；這里的i可取0，1，2，分別表示包為空、只含單元素及兩元素以上這三種情況。Soundness2公理將O、Odecompose2和Ocompose2關(guān)聯(lián)在一起，它斷言如果:a)非原始實例x能被分解為兩個子問題實例x1和x2;b)子問題實例x1和x2分別有可行解z1和z2;c)z1和z2能合并組成z0，那么z0是輸入x0的一個可行解。其他的公理有類似的斷言。操作符>是D上的良序以保證算法的終止性，相應(yīng)的公理被省略。

下面給出的是約束加強(qiáng)的規(guī)約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(xiàn)(x2))

enddefinition

theorem O(x，F(xiàn)(x))

endspec

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

排序分治算法的開發(fā)從構(gòu)建問題理論到規(guī)約sorting的解釋problemtheorysorting開始：

D|→bag

R|→seq

O|→sorted?

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

D|→bag

R|→seq

O|→sorted?

F|→?

E|→?

>|→?

p0|→?

Odecompose0|→?

Ocompose0|→?

……

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

假設(shè)選出構(gòu)建集合{emptybag， singletonbag， bagunion}作為輸入域bag上decompositon關(guān)系的基礎(chǔ)，那么能得到如下的部分分類箭頭：

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操作，引進(jìn)一個新的在z0，z1，z2約束范圍內(nèi)的存在量詞變量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))

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

( 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找到具體的表達(dá)式：

sorted? (x0，z0)=

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

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

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

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

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

seqtobag(z0)

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

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

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

seqtobag(z0)

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

上述分類箭頭的其他未完成部分按類似步驟進(jìn)行構(gòu)建。最后得到的完整分類箭頭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))

在這個分類箭頭的基礎(chǔ)上，如圖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數(shù)據(jù)求精及程序優(yōu)化

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

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

3應(yīng)用項目

這里簡單介紹了Kestrel研究所使用Designware及其精化技術(shù)開發(fā)的兩個應(yīng)用項目[10]。

3．1任務(wù)調(diào)度系統(tǒng)(mission planning system，MPS)

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

3．2Planware

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

4結(jié)束語

由于涉及到創(chuàng)造性工作，開發(fā)算法程序仍然是計算機(jī)科學(xué)領(lǐng)域中最具挑戰(zhàn)性的問題之一。算法程序設(shè)計的自動化對提高軟件可信度具有重要的作用，其最終目標(biāo)是構(gòu)建支持算法程序設(shè)計的系統(tǒng)。該方向越來越受到計算機(jī)科學(xué)工作者的關(guān)注，有關(guān)的大量工作正在展開。

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

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

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

參考文獻(xiàn)：

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

[2]陳火旺，王戟，董威.高可信軟件工程技術(shù)[J].電子學(xué)報，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.

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