形式化PAR方法及其算法程序規約精化機理

蘇 昭

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

形式化PAR方法及其算法程序規約精化機理

蘇 昭

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

用形式化方法開發軟件是提高軟件生產效率和可靠性的革命性途徑，是實現軟件自動化的決定性關鍵。文章介紹了一種新的支持作為軟件開發核心的算法設計的形式化方法PAR，分析了其理論基礎及算法程序規約精化機理，并結合一個經典實例開發展示了PAR的具體使用，給出PAR的實際應用項目，最后對PAR進行了評述。

形式化PAR方法；規約精化；算法程序

1 概述

形式化方法是建立在嚴格數學基礎上的軟件開發方法。軟件開發的全過程中，從需求分析、規格說明、設計、編程、系統集成、測試、文檔生成直至維護各階段，凡是采用嚴格的數學語言、具有精確的數學語義的方法稱為形式化方法。軟件自動化在未來軟件工程中占據著重要的位置，用形式化方法開發軟件，被當今計算機界譽為克服“軟件危機”、提高軟件可靠性和生產效率的革命性途徑，是實現軟件自動化的關鍵。

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

著名的形式化PAR(Partition-and-Recur)[5-11]方法是由中國知名計算機科學專家、江西師范大學薛錦云教授及其領銜的軟件形式化與自動化團隊研究的一種新型形式化方法學，其著重研究軟件的核心-算法程序的形式化開發。形式化PAR方法[11]由自定義的泛型算法設計語言Radl、泛型抽象程序設計語言Apla、系統的形式化開發算法程序技術及轉換工具集構成。其中Radl又是形式化規約描述語言，規約是形式化軟件開發的邏輯起點，是程序正確性證明、形式化推導的關鍵，本文主要介紹Radl規約及規約精化機理。

2 形式化PAR方法

2.1 規約

PAR方法對從軟件形式規約說明Radl到可執行語言程序的軟件(半)自動開發提供有力支持。Radl語言不但適應傳統數學之習慣,而且具備引用的透明性,十分有利于形式化規約說明的推導。

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

我們采用如下Radl算法規約說明的刻畫形式[11]:

|[標識符說明]|

AQ:謂詞表達式；

AR:謂詞表達式。

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

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

一般形式:問題的定義式。

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

選取一般形式亦或標準形式來刻畫描述問題的原則是:刻畫問題直觀簡潔和有利于探尋隱含在問題之中的深層遞推關系。

下例是一個使用標準形式(Qi:r(i):f(i))描述的計算圖單源最短路徑問題的形式化Radl規約說明[7,12]:

2.2 分化遞推思想及規約精化機理

根據PAR方法,解決問題是通過分劃出子問題并對子問題求解的基礎上來完成的。在構造遞推關系時，必須將子問題分劃出來并揭示出它們之間的邏輯關系。規約是對問題的形式化描述,問題的分劃體現在規約變換上即為分劃規約。

2.2.1 分化遞推

為了構造問題的遞推關系，首先必須對問題進行科學合理的劃分。

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

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

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

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

人們對于原問題的劃分往往蘊含算法設計的策略,并為進行后續的規約變換以構造遞推關系提供整體方向。通過推導大量算法程序的實踐發現,影響算法效率的首要因素在于對問題的分化,提高問題求解的效率往往可以通過改變問題分劃的方式而輕易獲得，如排序問題,從相同的形式化規約出發,經不同的分劃方式變換,可開發出多個復雜度不同的算法。

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

定理1.問題分解出的子問題相互獨立時,對問題做平衡分劃所設計出的算法效率要比非平衡分劃時高；

定理2.問題分解出的子問題存在相互重疊時,對問題做非平衡分劃所設計出算法的效率要比平衡分劃時高。

2.2.2 基本規約變換法則[11]

2.2.3 規約精化

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

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

3.范圍為單點時，運用單一范圍變換規則；

4.據上下文對CSp進行謂詞演算或運用與量詞函數相關的性質進行變換；

7.根據再做深入分析：

3 實例研究

應用本文結果,我們為求解圓周率問題開發一個算法程序，闡述的重點放在問題的規約及其規約精化上，即問題分化、遞推關系構造上,對于生成可執行程序的過程僅做簡要敘述。問題[13,16-17]：求解圓周率π

(1)問題形式化規約的構造

(2)原問題分劃

根據數列知識，采用非平衡分劃:

把初始條件(2)與遞推關系(1)結合,得求解問題的Radl算法:

(4)循環不變式的開發

根據循環不變式的新定義及新的開發策略[11],變量P存放Sm的值,則可機械地寫出循環不變式:

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

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

(6)算法程序代碼

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

4 應用項目

這里簡單介紹使用形式化PAR方法及其規約精化技術開發的一個實際應用項目[18]。

裝備保障決策支持系統用于對裝備保障數據庫中的大數據及其它可用的情報數據進行實時、迅速地在線整合分析，使裝備保障內外的大數據轉化為科學的管理決策信息。構建裝備保障決策支持系統，對平時和戰時裝備保障數據的存儲與分析，為裝備指揮決策提供科學支撐，是實現現代化裝備保障的需要。系統的效率、智能化水平和可靠性，將對決策的效果產生重大影響。在裝備保障智能決策支持的開發過程中引入形式化方法，能夠實現部分開發過程的自動化，并有助于從根本上提高軟件系統的質量，提高我軍裝備保障工作的整體水平[19-20]。進而，文獻[18]基于形式化PAR方法，提出一類離散最優化問題的結構模型和算法推演技術,形式化求解了一系列典型的裝備保障算法。

5 結束語

本文介紹的形式化PAR方法是薛錦云教授及其領銜的軟件形式化與自動化團隊在算法程序設計自動化方面作出的研究。PAR方法將分化遞推思想巧妙地運用到算法程序自動化設計之中，具有嚴格的數學理論基礎和平臺支撐。本文結合PAR的最新研究成果[10,12,14-15]，著重介紹了形式化PAR方法的規約及其規約精化機理，并通過對簡明經典實例的開發展示了使用PAR求解算法問題時分劃問題、構造遞推關系的特征。整個推導過程采用通俗易懂的數學知識、嚴謹的量詞等價變換,體現了遞推關系構造的簡明性與嚴謹性,提高了基于遞推關系所生成的算法程序的正確性，用支持算法程序形式化開發的PAR方法與PAR平臺求解算法問題的過程,也自然地、科學地揭示出了算法程序的來源問題[13]。

[1]鄒盛榮,鄭國梁.B語言和方法與Z、VDM的比較[J].計算機科學,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]周之英.現代軟件工程[M].北京:科學出版社，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]薛錦云,楊慶紅,等.程序設計方法學[M].北京:高等教育出版社,2002.

[12]王昌晶,薛錦云.Radl形式規格說明相對正確性研究[J].軟件學報,2013,24(4):715-729.

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

[14]石海鶴,薛錦云.基于PAR的算法形式化開發[J].計算機學報,2009,32(5):982-991.

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

[16]蘇昭.關系代數→關系演算轉換系統的研制[D].南昌:江西師范大學碩士學位論文,2010.

[17]冉小曉.Radl-Apla自動程序轉換系統研究與實現[D].南昌:江西師范大學碩士學位論文,2005.

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

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

[20]鄭宇軍,王連來,薛錦云.面向裝備聯勤保障的約束程序設計框架[J].南京大學學報（自然科學）,2005,41(z1):30-34.

（責任編輯：陳 輝）

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－)，男，安徽亳州人，江西科技學院信息工程學院，講師，碩士。研究方向：軟件形式化與自動化。

江西科技學院自然科學基金項目“基于項目反應理論的成人高考數學模塊化訓練系統的研制”(NO.XYKJ2011012)；江西科技學院協同創新基金項目“面向車聯網的智能交通最短路徑算法的優化及其應用研究”(NO.xtcx201318)。