形式化PAR方法及其算法程序規(guī)約精化機(jī)理

蘇 昭

（江西科技學(xué)院 信息工程學(xué)院，江西 南昌 330098）

形式化PAR方法及其算法程序規(guī)約精化機(jī)理

蘇 昭

（江西科技學(xué)院 信息工程學(xué)院，江西 南昌 330098）

用形式化方法開(kāi)發(fā)軟件是提高軟件生產(chǎn)效率和可靠性的革命性途徑，是實(shí)現(xiàn)軟件自動(dòng)化的決定性關(guān)鍵。文章介紹了一種新的支持作為軟件開(kāi)發(fā)核心的算法設(shè)計(jì)的形式化方法PAR，分析了其理論基礎(chǔ)及算法程序規(guī)約精化機(jī)理，并結(jié)合一個(gè)經(jīng)典實(shí)例開(kāi)發(fā)展示了PAR的具體使用，給出PAR的實(shí)際應(yīng)用項(xiàng)目，最后對(duì)PAR進(jìn)行了評(píng)述。

形式化PAR方法；規(guī)約精化；算法程序

1 概述

形式化方法是建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上的軟件開(kāi)發(fā)方法。軟件開(kāi)發(fā)的全過(guò)程中，從需求分析、規(guī)格說(shuō)明、設(shè)計(jì)、編程、系統(tǒng)集成、測(cè)試、文檔生成直至維護(hù)各階段，凡是采用嚴(yán)格的數(shù)學(xué)語(yǔ)言、具有精確的數(shù)學(xué)語(yǔ)義的方法稱為形式化方法。軟件自動(dòng)化在未來(lái)軟件工程中占據(jù)著重要的位置，用形式化方法開(kāi)發(fā)軟件，被當(dāng)今計(jì)算機(jī)界譽(yù)為克服“軟件危機(jī)”、提高軟件可靠性和生產(chǎn)效率的革命性途徑，是實(shí)現(xiàn)軟件自動(dòng)化的關(guān)鍵。

形式化方法的一個(gè)十分重要的研究?jī)?nèi)容就是形式規(guī)約，即應(yīng)用具有精確語(yǔ)義的形式化語(yǔ)言書(shū)寫(xiě)的程序功能描述，它是論證程序正確與否的依據(jù)。在從高層形式規(guī)約至最終代碼實(shí)現(xiàn)的過(guò)程之中,選用恰當(dāng)?shù)?、以形式化方法作為基礎(chǔ)的工具進(jìn)行輔助的驗(yàn)證和設(shè)計(jì),對(duì)提升安全攸關(guān)系統(tǒng)的可信度有著極其巨大的幫助。20世紀(jì)90年代以來(lái),在國(guó)際上,形式化方法已成為軟件開(kāi)發(fā)中重要的可信軟件技術(shù)之一。形式化方法對(duì)軟件可信度的獲得與保證有著不可替代的重大作用，但形式化方法在實(shí)際的高可信軟件的開(kāi)發(fā)中仍十分少見(jiàn)，當(dāng)前，軟件的開(kāi)發(fā)仍以傳統(tǒng)的非形式化軟件開(kāi)發(fā)方法為主流。因而,研究與應(yīng)用形式化方法及其為基礎(chǔ)的支撐工具是一項(xiàng)極有意義的前瞻性、迫切性的現(xiàn)實(shí)工作。

著名的形式化PAR(Partition-and-Recur)[5-11]方法是由中國(guó)知名計(jì)算機(jī)科學(xué)專家、江西師范大學(xué)薛錦云教授及其領(lǐng)銜的軟件形式化與自動(dòng)化團(tuán)隊(duì)研究的一種新型形式化方法學(xué)，其著重研究軟件的核心-算法程序的形式化開(kāi)發(fā)。形式化PAR方法[11]由自定義的泛型算法設(shè)計(jì)語(yǔ)言Radl、泛型抽象程序設(shè)計(jì)語(yǔ)言Apla、系統(tǒng)的形式化開(kāi)發(fā)算法程序技術(shù)及轉(zhuǎn)換工具集構(gòu)成。其中Radl又是形式化規(guī)約描述語(yǔ)言，規(guī)約是形式化軟件開(kāi)發(fā)的邏輯起點(diǎn)，是程序正確性證明、形式化推導(dǎo)的關(guān)鍵，本文主要介紹Radl規(guī)約及規(guī)約精化機(jī)理。

2 形式化PAR方法

2.1 規(guī)約

PAR方法對(duì)從軟件形式規(guī)約說(shuō)明Radl到可執(zhí)行語(yǔ)言程序的軟件(半)自動(dòng)開(kāi)發(fā)提供有力支持。Radl語(yǔ)言不但適應(yīng)傳統(tǒng)數(shù)學(xué)之習(xí)慣,而且具備引用的透明性,十分有利于形式化規(guī)約說(shuō)明的推導(dǎo)。

Radl語(yǔ)言的主要功能在于描述問(wèn)題的形式化規(guī)約說(shuō)明、規(guī)約說(shuō)明變換規(guī)則以及描述算法。Radl提供了足夠抽象的機(jī)制,可集中刻畫(huà)問(wèn)題的功能,而不為設(shè)計(jì)和實(shí)現(xiàn)所涉及的問(wèn)題(如效率)所干擾[12]。

我們采用如下Radl算法規(guī)約說(shuō)明的刻畫(huà)形式[11]:

|[標(biāo)識(shí)符說(shuō)明]|

AQ:謂詞表達(dá)式；

AR:謂詞表達(dá)式。

其中,標(biāo)識(shí)符說(shuō)明部分主要用于聲明在前、后置斷言中出現(xiàn)的變量和函數(shù)的屬性及類型。屬性有 3種[11]:一是輸入變量,用關(guān)鍵字IN標(biāo)識(shí)；二是輸出變量,用關(guān)鍵字OUT標(biāo)識(shí)；三是輔助變量,用關(guān)鍵字AUX標(biāo)識(shí)。類型可以是Radl語(yǔ)言中的標(biāo)準(zhǔn)數(shù)據(jù)類型(integer,real,char,string,boolean)、自定義簡(jiǎn)單類型(數(shù)組類型，記錄類型，子界類型，枚舉類型)、預(yù)定義ADT類型(序列類型，集合類型，樹(shù)類型，圖類型)和自定義ADT類型。

以AQ和AR開(kāi)頭的謂詞表達(dá)式分別稱為算法程序的前置斷言和后置斷言,用于表示算法程序的輸入?yún)?shù)必須滿足的條件、輸出參數(shù)必須滿足的條件,均為一階謂詞邏輯公式[11-13],其中AQ是一般的一階謂詞表達(dá)式，AR有兩種表達(dá)形式:

一般形式:問(wèn)題的定義式。

標(biāo)準(zhǔn)形式:(Qi:r(i):f(i))),表示“在范圍r(i)上,對(duì)函數(shù)f(i)施行 q運(yùn)算所得到的量”,其中,Q是q運(yùn)算的一般化,可以是?(存在量詞),?(全稱量詞),MAX(求最大值量詞),MIN(求最小值量詞),∑(求和量詞),∏(求積量詞)等,所分別對(duì)應(yīng)的q運(yùn)算分別是∨,∧,max,min,+,*等，標(biāo)準(zhǔn)形式是對(duì)問(wèn)題的更進(jìn)一步的邏輯抽象[11]。

選取一般形式亦或標(biāo)準(zhǔn)形式來(lái)刻畫(huà)描述問(wèn)題的原則是:刻畫(huà)問(wèn)題直觀簡(jiǎn)潔和有利于探尋隱含在問(wèn)題之中的深層遞推關(guān)系。

下例是一個(gè)使用標(biāo)準(zhǔn)形式(Qi:r(i):f(i))描述的計(jì)算圖單源最短路徑問(wèn)題的形式化Radl規(guī)約說(shuō)明[7,12]:

2.2 分化遞推思想及規(guī)約精化機(jī)理

根據(jù)PAR方法,解決問(wèn)題是通過(guò)分劃出子問(wèn)題并對(duì)子問(wèn)題求解的基礎(chǔ)上來(lái)完成的。在構(gòu)造遞推關(guān)系時(shí)，必須將子問(wèn)題分劃出來(lái)并揭示出它們之間的邏輯關(guān)系。規(guī)約是對(duì)問(wèn)題的形式化描述,問(wèn)題的分劃體現(xiàn)在規(guī)約變換上即為分劃規(guī)約。

2.2.1 分化遞推

為了構(gòu)造問(wèn)題的遞推關(guān)系，首先必須對(duì)問(wèn)題進(jìn)行科學(xué)合理的劃分。

石海鶴[14]深入研究了子問(wèn)題規(guī)模間的關(guān)系,將問(wèn)題分劃成兩種方式：平衡分劃與非平衡分劃,并定義如下（P(n)表示問(wèn)題,n為問(wèn)題規(guī)模）：

定義1.平衡分劃是指將問(wèn)題P(n)分成k個(gè)

規(guī)模相等或相差最多不超過(guò)1的子問(wèn)題,這里1〈k≤n/2，具體地說(shuō),設(shè)n mod k=s,則平衡分劃時(shí)將P(n)分成k-s個(gè)規(guī)模為的子問(wèn)題和s個(gè)規(guī)模為的子問(wèn)題；

不符合定義1的分劃稱為非平衡分劃。

人們對(duì)于原問(wèn)題的劃分往往蘊(yùn)含算法設(shè)計(jì)的策略,并為進(jìn)行后續(xù)的規(guī)約變換以構(gòu)造遞推關(guān)系提供整體方向。通過(guò)推導(dǎo)大量算法程序的實(shí)踐發(fā)現(xiàn),影響算法效率的首要因素在于對(duì)問(wèn)題的分化,提高問(wèn)題求解的效率往往可以通過(guò)改變問(wèn)題分劃的方式而輕易獲得，如排序問(wèn)題,從相同的形式化規(guī)約出發(fā),經(jīng)不同的分劃方式變換,可開(kāi)發(fā)出多個(gè)復(fù)雜度不同的算法。

由于對(duì)算法問(wèn)題求解時(shí),已知的內(nèi)容僅有問(wèn)題及其形式化規(guī)約,我們就必須從問(wèn)題特征以及問(wèn)題的形式化規(guī)約入手,采用具體分劃方式以獲取較高效率的算法。石海鶴[14]通過(guò)大量問(wèn)題分劃的深入研究,提出了從問(wèn)題形式化規(guī)約確定分劃方式的問(wèn)題分劃法則(Partition Rules,PR),用來(lái)指導(dǎo)面向效率的問(wèn)題分劃，并有以下兩個(gè)重要定理：

定理1.問(wèn)題分解出的子問(wèn)題相互獨(dú)立時(shí),對(duì)問(wèn)題做平衡分劃所設(shè)計(jì)出的算法效率要比非平衡分劃時(shí)高；

定理2.問(wèn)題分解出的子問(wèn)題存在相互重疊時(shí),對(duì)問(wèn)題做非平衡分劃所設(shè)計(jì)出算法的效率要比平衡分劃時(shí)高。

2.2.2 基本規(guī)約變換法則[11]

2.2.3 規(guī)約精化

記問(wèn)題為P(n),它的解記為SP(n)，n為問(wèn)題

2.若CSp包含有(Qi:r(i):f(i))的部分,即量詞Q僅含一個(gè)約束變量i,則根據(jù)分劃之形式對(duì)r(i)運(yùn)用范圍分裂變換法則,將CSp盡量展開(kāi)；

3.范圍為單點(diǎn)時(shí)，運(yùn)用單一范圍變換規(guī)則；

4.據(jù)上下文對(duì)CSp進(jìn)行謂詞演算或運(yùn)用與量詞函數(shù)相關(guān)的性質(zhì)進(jìn)行變換；

7.根據(jù)再做深入分析：

3 實(shí)例研究

應(yīng)用本文結(jié)果,我們?yōu)榍蠼鈭A周率問(wèn)題開(kāi)發(fā)一個(gè)算法程序，闡述的重點(diǎn)放在問(wèn)題的規(guī)約及其規(guī)約精化上，即問(wèn)題分化、遞推關(guān)系構(gòu)造上,對(duì)于生成可執(zhí)行程序的過(guò)程僅做簡(jiǎn)要敘述。問(wèn)題[13,16-17]：求解圓周率π

(1)問(wèn)題形式化規(guī)約的構(gòu)造

(2)原問(wèn)題分劃

根據(jù)數(shù)列知識(shí)，采用非平衡分劃:

把初始條件(2)與遞推關(guān)系(1)結(jié)合,得求解問(wèn)題的Radl算法:

(4)循環(huán)不變式的開(kāi)發(fā)

根據(jù)循環(huán)不變式的新定義及新的開(kāi)發(fā)策略[11],變量P存放Sm的值,則可機(jī)械地寫(xiě)出循環(huán)不變式:

(5)抽象算法程序（Apla）

在轉(zhuǎn)換工具Radl-Apla的支持下可自動(dòng)生成Apla抽象程序 (核心代碼)：

(6)算法程序代碼

把上述程序加上輸入語(yǔ)句和輸出語(yǔ)句,用PAR方法轉(zhuǎn)換工具可將其自動(dòng)地生成C++或Java等語(yǔ)言程序,這里不再贅述。

4 應(yīng)用項(xiàng)目

這里簡(jiǎn)單介紹使用形式化PAR方法及其規(guī)約精化技術(shù)開(kāi)發(fā)的一個(gè)實(shí)際應(yīng)用項(xiàng)目[18]。

裝備保障決策支持系統(tǒng)用于對(duì)裝備保障數(shù)據(jù)庫(kù)中的大數(shù)據(jù)及其它可用的情報(bào)數(shù)據(jù)進(jìn)行實(shí)時(shí)、迅速地在線整合分析，使裝備保障內(nèi)外的大數(shù)據(jù)轉(zhuǎn)化為科學(xué)的管理決策信息。構(gòu)建裝備保障決策支持系統(tǒng)，對(duì)平時(shí)和戰(zhàn)時(shí)裝備保障數(shù)據(jù)的存儲(chǔ)與分析，為裝備指揮決策提供科學(xué)支撐，是實(shí)現(xiàn)現(xiàn)代化裝備保障的需要。系統(tǒng)的效率、智能化水平和可靠性，將對(duì)決策的效果產(chǎn)生重大影響。在裝備保障智能決策支持的開(kāi)發(fā)過(guò)程中引入形式化方法，能夠?qū)崿F(xiàn)部分開(kāi)發(fā)過(guò)程的自動(dòng)化，并有助于從根本上提高軟件系統(tǒng)的質(zhì)量，提高我軍裝備保障工作的整體水平[19-20]。進(jìn)而，文獻(xiàn)[18]基于形式化PAR方法，提出一類離散最優(yōu)化問(wèn)題的結(jié)構(gòu)模型和算法推演技術(shù),形式化求解了一系列典型的裝備保障算法。

5 結(jié)束語(yǔ)

本文介紹的形式化PAR方法是薛錦云教授及其領(lǐng)銜的軟件形式化與自動(dòng)化團(tuán)隊(duì)在算法程序設(shè)計(jì)自動(dòng)化方面作出的研究。PAR方法將分化遞推思想巧妙地運(yùn)用到算法程序自動(dòng)化設(shè)計(jì)之中，具有嚴(yán)格的數(shù)學(xué)理論基礎(chǔ)和平臺(tái)支撐。本文結(jié)合PAR的最新研究成果[10,12,14-15]，著重介紹了形式化PAR方法的規(guī)約及其規(guī)約精化機(jī)理，并通過(guò)對(duì)簡(jiǎn)明經(jīng)典實(shí)例的開(kāi)發(fā)展示了使用PAR求解算法問(wèn)題時(shí)分劃問(wèn)題、構(gòu)造遞推關(guān)系的特征。整個(gè)推導(dǎo)過(guò)程采用通俗易懂的數(shù)學(xué)知識(shí)、嚴(yán)謹(jǐn)?shù)牧吭~等價(jià)變換,體現(xiàn)了遞推關(guān)系構(gòu)造的簡(jiǎn)明性與嚴(yán)謹(jǐn)性,提高了基于遞推關(guān)系所生成的算法程序的正確性，用支持算法程序形式化開(kāi)發(fā)的PAR方法與PAR平臺(tái)求解算法問(wèn)題的過(guò)程,也自然地、科學(xué)地揭示出了算法程序的來(lái)源問(wèn)題[13]。

[1]鄒盛榮,鄭國(guó)梁.B語(yǔ)言和方法與Z、VDM的比較[J].計(jì)算機(jī)科學(xué),2002,29(10):136-138.

[2]Batory D.Thoughts on automated software design and synthesis.In:Proc.of the FSE/SDP Workshop,Future of Software Engineering Research(FoSER 2010).New York:ACM Press,2010.29-32.

[3]周之英.現(xiàn)代軟件工程[M].北京:科學(xué)出版社，2000.

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

[5]Xue JY.Two new strategies for developing loop invariants and their applications. Journal of Computer Science and Technology,1993,8(2):147-154.

[6]Xue JY.A unified approach for developing efficient algorithmic programs.JournalofComputerScience and Technology,1997,12(4):314-329.

[7]Xue JY.Formal derivation of graph algorithmic programs using partition-and- recur.JournalofComputerScience and Technology,1998,13(6):553-561.

[8]Xue JY,Yang B,Zuo ZK.A linear in-situ algorithm for the power of cyclic permutation.In:Proc.of the 2nd Int'l Frontiers of Algorithmics Workshop.Berlin:Springer-Verlag,2008.113-123.

[9]Xue JY.PAR method and its supporting platform.In:Proc.of the 1st Int'l Workshop on Asian Working Conf.on Verified Software.Macao:UNU-IIST,2006.10-20.

[10]DengXiaotie,HopcroftJohn E,Xue Jinyun.Frontiersin Algorithmics[M].Berlin and Heidelberg GmbH&Co.K:Springer-Verlag,2009.

[11]薛錦云,楊慶紅,等.程序設(shè)計(jì)方法學(xué)[M].北京:高等教育出版社,2002.

[12]王昌晶,薛錦云.Radl形式規(guī)格說(shuō)明相對(duì)正確性研究[J].軟件學(xué)報(bào),2013,24(4):715-729.

[13]蘇昭,薛錦云,楊晨.形式化方法在高中算法教學(xué)中的應(yīng)用研究[J].計(jì)算機(jī)與現(xiàn)代化,2010(7):87-92.

[14]石海鶴,薛錦云.基于PAR的算法形式化開(kāi)發(fā)[J].計(jì)算機(jī)學(xué)報(bào),2009,32(5):982-991.

[15]石海鶴,薛錦云.基于 PAR的排序算法自動(dòng)生成研究[J].軟件學(xué)報(bào),2012,23(9):2248-2260.

[16]蘇昭.關(guān)系代數(shù)→關(guān)系演算轉(zhuǎn)換系統(tǒng)的研制[D].南昌:江西師范大學(xué)碩士學(xué)位論文,2010.

[17]冉小曉.Radl-Apla自動(dòng)程序轉(zhuǎn)換系統(tǒng)研究與實(shí)現(xiàn)[D].南昌:江西師范大學(xué)碩士學(xué)位論文,2005.

[18]鄭宇軍.基于PAR的高可信裝備保障算法形式化推演[博士學(xué)位論文].北京:中國(guó)科學(xué)院軟件研究所,2009.

[19]張子丘,鄭宇軍,王侃.形式化方法在裝備保障決策支持系統(tǒng)中的應(yīng)用[J].裝甲兵工程學(xué)院學(xué)報(bào),2005,19(4):13-16.

[20]鄭宇軍,王連來(lái),薛錦云.面向裝備聯(lián)勤保障的約束程序設(shè)計(jì)框架[J].南京大學(xué)學(xué)報(bào)（自然科學(xué)）,2005,41(z1):30-34.

（責(zé)任編輯：陳 輝）

Formal Method PAR and Its Algorithmic Program Specification Refinement Mechanism

SU Zhao
（College of Information Science and Engineering,Jiangxi University of Technology，Nanchang 330098,China）

Developing software using formal method is a revolutionary way to develop software efficiently and reliably，and is key to realize software automation.This paper introduces a new formal method PAR that supported automatic algorithm design,analyzes its theoretical foundation and specification refinement theory,then presents a detailed example of using PAR is and illustrated one practical application.Finally gave the discussions and conclusions.

formal method PAR；specification refinement；algorithmic program

TP312

A

123（2014）03-0053-05

2014-03-03

蘇昭(1984－)，男，安徽亳州人，江西科技學(xué)院信息工程學(xué)院，講師，碩士。研究方向：軟件形式化與自動(dòng)化。

江西科技學(xué)院自然科學(xué)基金項(xiàng)目“基于項(xiàng)目反應(yīng)理論的成人高考數(shù)學(xué)模塊化訓(xùn)練系統(tǒng)的研制”(NO.XYKJ2011012)；江西科技學(xué)院協(xié)同創(chuàng)新基金項(xiàng)目“面向車聯(lián)網(wǎng)的智能交通最短路徑算法的優(yōu)化及其應(yīng)用研究”(NO.xtcx201318)。