基于par的算法形式化開(kāi)發(fā)

《基于par的算法形式化開(kāi)發(fā)》由會(huì)員上傳分享，免費(fèi)在線(xiàn)閱讀，更多相關(guān)內(nèi)容在行業(yè)資料-天天文庫(kù)。

1、《計(jì)算機(jī)學(xué)報(bào)》2009年5期基于PAR的算法形式化開(kāi)發(fā)*本課題得到國(guó)家自然科學(xué)基金（60573080,60773054）、江西省自然科學(xué)基金（2008GQS0056）資助.石海鶴,女,1979年生,博士研究生,主要研究方向?yàn)檐浖问交c自動(dòng)化.E-mail:haiheshi@163.com.薛錦云,男,1947年生,教授,博士生導(dǎo)師,主要研究領(lǐng)域?yàn)檐浖问交c自動(dòng)化,可信軟件.石海鶴1,2,3　薛錦云1,21（中國(guó)科學(xué)院軟件研究所計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室北京100080）2（江西師范大學(xué)高性能計(jì)算技術(shù)重點(diǎn)實(shí)驗(yàn)室南昌330022）3（中國(guó)科學(xué)院研究生院北京100049）摘要：

2、形式化方法是構(gòu)建可信軟件的重要途徑。基于對(duì)算法問(wèn)題的分析，針對(duì)形式化方法PAR開(kāi)發(fā)算法的特征，刻劃了問(wèn)題分劃、遞推關(guān)系構(gòu)造方面的規(guī)律。從一類(lèi)問(wèn)題的形式化功能規(guī)約出發(fā)，可機(jī)械的完成問(wèn)題的分劃及規(guī)約的變換，自然的揭露出求解問(wèn)題的算法思想，在相關(guān)工具的支持下自動(dòng)生成算法程序。研究結(jié)果將算法設(shè)計(jì)中盡可能多的創(chuàng)造性勞動(dòng)轉(zhuǎn)化為非創(chuàng)造性勞動(dòng)，降低了形式化求解算法問(wèn)題的難度，提高了算法程序的可靠性和形式化開(kāi)發(fā)效率。關(guān)鍵詞：算法；形式化方法；PAR；規(guī)約；可信軟件11《計(jì)算機(jī)學(xué)報(bào)》2009年5期1引言隨著社會(huì)對(duì)信息技術(shù)的依賴(lài)性日益增長(zhǎng)，處于信息技術(shù)核心的計(jì)算機(jī)軟件的可信性被提到一個(gè)新的高度，

3、國(guó)內(nèi)外都很重視并已開(kāi)展大量的研究工作。作為學(xué)術(shù)界的領(lǐng)袖人物之一，Hoare在歐、美同行的支持下，正組織關(guān)于軟件驗(yàn)證（VerifiedSoftware）的國(guó)際性項(xiàng)目，這被認(rèn)為是計(jì)算機(jī)科學(xué)界本世紀(jì)的一個(gè)重大挑戰(zhàn)性問(wèn)題[1]；美國(guó)政府制定的2006-2015國(guó)家軟件發(fā)展戰(zhàn)略——“下一代軟件工程”中，也將提高軟件可信性放在四大戰(zhàn)略任務(wù)的首位。對(duì)軟件可信性的需求已從安全性至關(guān)重要的領(lǐng)域，如國(guó)防、航空航天、醫(yī)療器械等擴(kuò)展到能源、通信、財(cái)經(jīng)、制造業(yè)等關(guān)鍵領(lǐng)域。而正確性被一致認(rèn)為是可信軟件的極其重要的性質(zhì)。算法作為軟件的核心，被譽(yù)為“計(jì)算的靈魂”[2]，保證算法的正確性對(duì)提高安全攸關(guān)系統(tǒng)的

4、可信度有很大幫助。統(tǒng)計(jì)表明，傳統(tǒng)的非形式化方法對(duì)軟件質(zhì)量的保證具有一個(gè)難以逾越的頂點(diǎn)，而形式化方法的實(shí)踐證明形式化方法是提高軟件質(zhì)量的重要途徑[3]。20世紀(jì)90年代以來(lái)，在國(guó)際上，形式化方法已成為軟件開(kāi)發(fā)中重要的可信軟件技術(shù)之一，它在保證算法的正確性、展示算法設(shè)計(jì)的過(guò)程、揭示算法設(shè)計(jì)的本質(zhì)特征和一般規(guī)律方面具有重要的意義，對(duì)自動(dòng)程序設(shè)計(jì)的探索將有很大的幫助[4,5]。由于算法求解涉及到創(chuàng)造性勞動(dòng)，形式化開(kāi)發(fā)算法仍然是計(jì)算機(jī)領(lǐng)域中最具挑戰(zhàn)性的問(wèn)題之一。本文針對(duì)形式化方法PAR（Partition-and-Recur）[6-11]開(kāi)發(fā)算法的特征，刻劃了問(wèn)題分劃、遞推關(guān)系構(gòu)造方

5、面的規(guī)律，使得從問(wèn)題的形式化功能規(guī)約出發(fā)，問(wèn)題的分劃及規(guī)約的變換可機(jī)械的完成，自然的揭露出求解問(wèn)題的算法思想，自動(dòng)的生成高效的求解問(wèn)題的算法程序。接下來(lái)我們首先介紹了PAR方法，重點(diǎn)介紹和分析了其中的形式化功能規(guī)約機(jī)制和開(kāi)發(fā)算法程序的方法；然后結(jié)合對(duì)問(wèn)題的分析，詳細(xì)闡述了我們提出的問(wèn)題分劃法則和規(guī)約變換策略；在第5節(jié)通過(guò)一個(gè)代表性的算法開(kāi)發(fā)實(shí)例展示了該模式的應(yīng)用效果；第6節(jié)和相關(guān)工作進(jìn)行了比較；于文章最后作了總結(jié)和討論。2PAR方法PAR方法是一種統(tǒng)一的算法設(shè)計(jì)方法，涵蓋了多種已知的算法設(shè)計(jì)技術(shù)，例如，動(dòng)態(tài)規(guī)劃法、貪心法、分治法、窮舉法等等，支持算法程序開(kāi)發(fā)的全過(guò)程。這里，

6、算法程序是指用已實(shí)現(xiàn)的或抽象的程序設(shè)計(jì)語(yǔ)言描述的算法。如圖1所示，該方法由自定義泛型算法設(shè)計(jì)語(yǔ)言Radl(Recurrence-basedAlgorithmDesignLanguage)、泛型抽象程序設(shè)計(jì)語(yǔ)言Apla(AbstractProgrammingLanguage)、系統(tǒng)的算法和程序設(shè)計(jì)方法學(xué)及轉(zhuǎn)換工具集組成。其中，PAR對(duì)從問(wèn)題出發(fā)設(shè)計(jì)出Radl算法的過(guò)程提供了形式化支持；對(duì)從Radl算法經(jīng)Apla程序到可執(zhí)行語(yǔ)言程序的生成提供了自動(dòng)化的支持。圖1.PAR2.1形式化功能規(guī)約形式化功能規(guī)約是算法程序開(kāi)發(fā)的起點(diǎn)。Radl語(yǔ)言的主要功能是描述問(wèn)題的規(guī)約、規(guī)約變換規(guī)則和

7、描述算法，由算法規(guī)約語(yǔ)言和算法描述語(yǔ)言?xún)刹糠纸M成。Radl提供了足夠抽象的機(jī)制，可集中刻劃問(wèn)題的功能，而不為設(shè)計(jì)和實(shí)現(xiàn)所涉及的問(wèn)題（如效率）所干擾。我們采用如下Radl算法規(guī)約的刻劃形式：

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

9、AQ:謂詞表達(dá)式；AR:謂詞表達(dá)式；其中標(biāo)識(shí)符說(shuō)明部分主要用于說(shuō)明前、后置斷言中出現(xiàn)的變量和函數(shù)的屬性及類(lèi)型。屬性有三種：一是輸入變量，用關(guān)鍵字in標(biāo)識(shí)；二是輸出變量，用關(guān)鍵字out標(biāo)識(shí)；三是輔助變量，用關(guān)鍵字aux標(biāo)識(shí)。類(lèi)型可以是Radl語(yǔ)言中的標(biāo)準(zhǔn)數(shù)據(jù)類(lèi)型（integer,real,boolean,char,