程序規(guī)范及其正確性證明概述課件

第3章程序標準及其正確性證明概述內(nèi)容－Whereweare？程序標準、標準的描述斷言與標準及{P}S{Q}程序正確性的概念程序正確性證明的過程3.1程序標準與程序1.程序標準：程序設計之前，第一步必須明確“做什么〞。所謂“做什么〞是指對欲求解的問題的描述。程序標準〔PS-ProgramSpecification〕:關于“做什么〞的描述。這里的PS僅指功能的描述，不包括諸如處理速度、執(zhí)行時間、響應周期等與時間有關性能指標。PS是軟件工程的需求分析的結果。PS的含義是映射，是輸入到輸出的映射，它反映了程序對數(shù)據(jù)的作用。3.1程序標準與程序(續(xù))2.程序程序也是映射，是輸入到計算的映射，即每一輸入都對應一串計算步。3.程序標準與程序的關系給出標準后，程序開發(fā)就是建立一個程序，使得計算剛好能實現(xiàn)標準的映射；程序驗證是證明程序正確地實現(xiàn)了標準，即證明標準和已有程序之間的一致性規(guī)范程序輸入輸出映射輸入計算映射3.1程序標準與程序(續(xù))4.程序標準的描述-----標準語言標準必須用語言描述，該語言稱為標準語言。描述一個復雜問題的輸入和輸出之間的關系是困難的，目前對標準語言的模式尚無定論。有三種模式：自然語言：不夠準確，存在二義性，必須輔以數(shù)學語言。一階謂詞：可以精確地描述問題的輸入和輸出的關系，但是標準文本比較長。如Hoare系統(tǒng)。數(shù)學語言：用數(shù)學語言可以把輸入和輸出的映射描述為函數(shù)。這些函數(shù)的精確的泛函定義就構成了問題的標準。但存在過于標準的問題。3.1程序標準與程序(續(xù))5.一個適宜的程序標準語言應滿足的根本條件:應當為描述者和使用者所直接理解；應當有嚴格的數(shù)學語義應當與形式方法的構造理論和程序設計語言協(xié)調(diào)應當有較強的表達能力和通用性3.1程序標準與程序(續(xù))Z語言VDMB方法三者的比較6.形式化程序標準描述語言簡介3.1程序標準與程序(續(xù))Z語言是一種基于集合論和一階謂詞邏輯的形式化語言；Z語言支持軟件的形式化標準描述，標準的推理和求精；是迄今為止應用最廣泛的形式語言之一；Z是在JeanRaymondAbrial等的開創(chuàng)性工作下，由英國牛津大學的程序設計研究小組〔PRG，ProgrammingResearchGroup〕，于20世紀80年代初開發(fā)；PRG與IBM的Hursley實驗室合作，將Z語言用于IBM的客戶信息控制系統(tǒng)的開發(fā)，使得最終的產(chǎn)品質(zhì)量得到了全面的的提高，所測出的錯誤數(shù)量大大減少，并且整體開發(fā)費用降低了9％；在ISO指導下的國際標準化Z工作于2002年完成6.形式化程序標準描述語言簡介－Z語言簡介13.1程序標準與程序(續(xù))提供了一種稱為模式〔Schema〕的結構，它是Z的根本描述單位，以此來描述一個標準說明的狀態(tài)空間〔靜態(tài)性質(zhì)〕和操作〔動態(tài)行為〕。Ｚ語言的模式和模式演算：狀態(tài)模式對目標軟件系統(tǒng)的結構特征進行抽象描述；操作模式對目標軟件系統(tǒng)的行為特征進行抽象描述；通過模式演算，無論多么大型系統(tǒng)的規(guī)格說明都可以通過一個個小的局部來構成；6.形式化程序標準描述語言簡介－Z語言簡介23.1程序標準與程序(續(xù))Ｚ模式說明可以組合成新的Ｚ模式，新的Ｚ模式繼承其成分模式的一切屬性和約束。軟件系統(tǒng)的Ｚ模式規(guī)格說明可以按一定的層次結構給出。Ｚ規(guī)格說明由一系列模式組成，每個模式定義一個抽象對象或操作，并用謂詞判定描述給出新的對象或操作的語義約束。模式例:6.形式化程序標準描述語言簡介－Z語言簡介33.1程序標準與程序(續(xù))模式例1:[Student]//引入根本類型studentStudentSys//模式名Enrolled,tested:PStudent//聲明局部,學生的密集類型#enrolled≤size//斷言局部，合取關系testedenrolled等價于：//水平方式StudentSys=[enrolled,tested:PStudent|

#enrolled≤sizetestedenrolled]6.形式化程序標準描述語言簡介－Z語言簡介43.1程序標準與程序(續(xù))模式例2:EnrollStudentStudentSys//=StudentsysStudentSys’的簡寫

name?:Student//在輸入變量后加？name?enrolled//在輸出變量后加！enrolled<size//帶有后綴‘的變量表示操作后的變量enrolled’=enrolled∪{name?}tested’=tested

6.形式化程序標準描述語言簡介－Z語言簡介53.1程序標準與程序(續(xù))缺點:⑴Ｚ語言對大型系統(tǒng)的模塊化能力缺乏。⑵難以識別影響某一狀態(tài)模式的所有操作模式。⑶不能支持規(guī)格說明的重用。⑷Ｚ語言難以由計算機直接處理。缺少商品化的工具支持等到諸多原因6.形式化程序標準描述語言簡介－Z語言簡介63.1程序標準與程序(續(xù))VDM〔ViennaDevelopmentMethod〕是在1969年為開發(fā)PL/1語言時，由IBM公司維也納實驗室的研究小組提出的。初衷是為了描述PL/1語言的語義。VDM是一種功能構造性規(guī)格說明技術，它通過一階謂詞邏輯和已建立的抽象數(shù)據(jù)類型來描述每個運算或函數(shù)的功能。這種方法在90年代初在歐美許多研究機構或大學得到了廣泛的應用。如曼徹斯特大學將其作為CS的必修課。1996年ISO制訂了VDM的國際標準化版本VDM-SL6.形式化程序標準描述語言簡介－VDM簡介13.1程序標準與程序(續(xù))VDM技術的根本思想：運用抽象數(shù)據(jù)類型、數(shù)學概念和符號來規(guī)定運算或函數(shù)的功能；可使軟件系統(tǒng)的功能描述在抽象級上進行，完全擺脫了實現(xiàn)細節(jié)，這樣為軟件實現(xiàn)者提供了很大的靈活性；這種形式化規(guī)格說明還為程序正確性證明提供了依據(jù)。6.形式化程序標準描述語言簡介－VDM簡介23.1程序標準與程序(續(xù))VDM支持兩種抽象：數(shù)據(jù)抽象和操作抽象。一個VDM標準有以下不同的塊組成：types<typedefinitions>values<valuedefinitions>functions<functiondefinitions>operations<operationdefinitions>state<statename>of<statedefinition>end6.形式化程序標準描述語言簡介－VDM簡介33.1程序標準與程序(續(xù))缺點：⑴由于VDM對抽象數(shù)據(jù)類型預先定義了運算，而某些用戶定義的類型在規(guī)格說明描述中無需這么多運算，因而產(chǎn)生了運算冗余。⑵VDM目前還未能建立一整套描述機制，將一個大型系統(tǒng)分解為許多運算而描述出這些運算之間的關系⑶VDM形式規(guī)格說明過于形式化不容易理解6.形式化程序標準描述語言簡介－VDM簡介43.1程序標準與程序(續(xù))B方法是20世紀80年代初中期由以及BP研究中心的MATRA和GEAlsthom研究小組開發(fā)的。Ｂ語言是計算機輔助軟件工程中Ｂ技術、方法和工具集的簡稱;Ｂ語言是一種健全的面向實際軟件過程的基于數(shù)學理論的技術;Ｂ方法所用的符號和方法支持大局部的軟件過程：需求分析、規(guī)格說明、軟件設計、實現(xiàn)和維護;Ｂ方法的指導性原那么：分層軟件的逐步構造伴隨著逐步的驗證和校驗；6.形式化程序標準描述語言簡介－B語言簡介13.1程序標準與程序(續(xù))Ｂ工具盒包括有大量的工具，所有的工具集成在一個基于窗口的軟件開發(fā)環(huán)境中，因而支持運用Ｂ方法開發(fā)軟件的整個軟件過程；Ｂ工具支持軟件的逐步構造，其中的驗證過程可用靜態(tài)分析，動態(tài)分析采用模擬技術，正確性證明那么使用集成的定理證明器。Ｂ方法用一種簡單的偽程序語言來描述需求模型、說明接口，并進行中間設計和實現(xiàn)；B語言就是AMN〔抽象機器符號〕，AMN支持規(guī)格說明的類型檢測、動態(tài)驗證、數(shù)學證明等來確保設計過程的正確。6.形式化程序標準描述語言簡介－B語言簡介23.1程序標準與程序(續(xù))B方法的特點簡單熟悉的符號表示法：這種符號表示法用來表達狀態(tài)轉換，從規(guī)格說明到編碼，這種統(tǒng)一的形式減少了學習的難度和轉換中的語法錯誤。模塊化構造：從規(guī)格說明到實現(xiàn)的模塊化構造允許將規(guī)格說明和驗證過程分解為多個子任務來進行。大量實用的工具支持：現(xiàn)有大量的實用工具支持了B方法軟件開發(fā)周期的所有階段，包括動畫和文檔生成。成功的工業(yè)應用：B語言和方法已在很多的工業(yè)領域得到成功應用，包括實時、仿真、信息處理和工程等。6.形式化程序標準描述語言簡介－B語言簡介33.1程序標準與程序(續(xù))6.Z語言、VDM、B形式化方法的比較屬性ZVDMB基礎謂詞演算,集合論,模式偏函數(shù),集合論最弱前置條件,集合論開發(fā)階段規(guī)范說明規(guī)范說明,設計規(guī)范說明,設計,實現(xiàn)形式模式的符號表示,關系前/后置條件,函數(shù)嚴格的編程語言工具支持在規(guī)格說明級在規(guī)格說明級B-Toolkit,AtchierB,所有開發(fā)階段培訓支持圖書、課程圖書,課程實例研究、課程內(nèi)容－Whereweare？程序標準、標準的描述斷言與標準及{P}S{Q}程序正確性的概念程序正確性證明的過程3.2斷言與標準1.斷言斷言就是關于事物性質(zhì)的陳述。這個陳述可真可假。如“三是個質(zhì)數(shù)〞用斷言作為程序的注解或作為正確性命題的一局部時，常用大括號括起來。例1：寫一個計算商和余數(shù)的程序程序標準：“設被除數(shù)x1是個非負整數(shù)，除數(shù)x2是個正整數(shù)，計算x1除以x2的商y1和余數(shù)y2〞又描述為：“初始條件：{x1>=0ANDx2>0},計算滿足{x1=x2*y1+y2and0<=y2<x2}的整數(shù)y1和y2〞3.2斷言與標準(續(xù))一般地，一個程序標準可表示為由兩個謂詞構成的二元組〔P，Q〕。其中，P描述了所欲求解的問題必須滿足的初始條件，它限定了輸入?yún)?shù)的性質(zhì)，稱為初始斷言或前置斷言；Q描述了問題的最終解必須滿足的性質(zhì)，稱為結果斷言或后置斷言。3.2斷言與標準(續(xù))程序斷言是對程序的性質(zhì)的陳述。最重要的一個程序斷言為：{P}S{Q}。其中，〔P，Q〕是程序S的程序標準，S是一個程序〔或語句〕斷言{P}S{Q}稱為S關于〔P，Q〕的正確性斷言。它的意義：“假設S開始執(zhí)行時P為真，那么S的執(zhí)行必終止且終止時Q為真〞3.2斷言與標準(續(xù))例：求商余程序{x1>=0andx2>0}Y2:=x1;y1:=0;{0<=y2and0<x2andx1=x2*y1+y2}Whiley2>=x2dobegin{0<=y2and0<x2<＝y(tǒng)2andx1=x2*y1+y2}

y2:=y2-x2;y1:=y1+1;

{0<=y2and0<x2andx1=x2*y1+y2}end;{x1=x2*y1+y2and0<=y2<x2}3.2斷言與標準(續(xù))問題：如何構造斷言使他們能準確地反映不同位置上程序的性質(zhì)？有了斷言，如何證明他們的正確性？能否有準那么，可以從標準〔P，Q〕構造出程序S，使{P}S{Q}為真。3.2斷言與標準(續(xù))2.程序斷言的進一步說明說明：在給出標準描述〔P，Q〕時，必須指明哪些量是可變的，哪些是不可變的。如果是可變的，必要時對前者還需指明其變化方式。輸入?yún)?shù)：在程序執(zhí)行前從外部獲得值，但在程序執(zhí)行中，其值始終保持不變的變量。一般用以x開頭的標識符表示。輸出變量：其值隨程序的執(zhí)行而不斷變化的變量。一般以y開頭的變量，或不以x和u開頭的變量標識。輔助變量：為了描述程序變量取值變化方式而因入的變量。這些變量不得在程序中出現(xiàn)，用以u開頭的變量表示。3.2斷言與標準(續(xù))例1.編寫一個程序Swap〔y1，y2〕，功能是把y1，y2兩變量的值互換。其標準:({y1=u1∧y2=u2}，{y1=u2∧y2=u1})3.2斷言與標準(續(xù))例2：對數(shù)組b[m：n]進行排序的程序。功能是把數(shù)組b[m：n]各元素的值從小到大排列起來，使得最后的數(shù)組滿足b[i]≤b[i+1]，i=m，…,n-1。標準：P：{m≤n∧b[m:n]=u[m:n]}Q：{m≤n∧perm(b[m:n],u[m:n])∧(i:m≤i<n:b[i]≤b[i+1])}其中，u[m:n]代表b的任意可能初值；perm(b[m:n],u[m:n])是一個常謂詞，表示b是u的一個置換。3.2斷言與標準(續(xù))程序標準總結：在做程序標準時，必須區(qū)分三種變量：輸入變量、輸出變量、輔助變量。作為某一個標準〔P，Q〕的實現(xiàn)程序S，S不得包含輔助變量，S也不得對輸入?yún)?shù)進行任何形式的賦值，這些就是對標準〔P，Q〕和斷言{P}S{Q}的語法規(guī)定。程序正確性斷言{P}S{Q}的意義：“假設S的執(zhí)行開始于一個滿足P的狀態(tài)，那么這個執(zhí)行必將在有限的時間內(nèi)終止于一個滿足Q的狀態(tài)〞。所謂一個狀態(tài)是滿足P〔或Q〕的，假設在此狀態(tài)下P〔或Q〕為真。內(nèi)容－Whereweare？程序標準、標準的表示方法斷言與標準及{P}S{Q}程序正確性的概念程序正確性證明的過程3.3程序正確性概念定義1.如果對于每一個使得P(ā)為真的輸入ā，程序S計算都終止，稱程序S對P是終止的。定義2：對于滿足P(ā)為真，且能夠使程序S計算終止的每個ā，如果Q(ā,P(ā))為真，那么稱程序S對于P和Q是局部正確的。記為[P]S[Q]。?[P]S[Q]iff(ā)((?p(ā)and(?Sterminates))?Q(ā,P(ā))3.3程序正確性概念(續(xù))定義3：對于滿足P(ā)為真的每個ā，如果程序S能夠計算終止，且Q(ā,P(ā))為真，那么稱程序S對于P和Q是完全正確的。記為{P}S{Q}?{P}S{Q}iff(ā)(?p(ā)((?Sterminates)

and?Q(ā,P(ā)))?[P]S[Q]iff(ā)((?p(ā)and(?Sterminates))?

Q(ā,P(ā))〔1〕關于局部正確性證明的方法Floyd的不變式斷言法Manna的子目標斷言法Hoare的公理化方法〔2〕關于終止性證明的方法Floyd的良序集方法Knuth的計數(shù)器方法Manna等人的不動點方法〔3〕關于完全正確性的證明方法Hoare的公理化方法〔Manna、Pnueli〕Bustall的間發(fā)斷言法Dijkstra的弱謂詞轉換方法以及強驗證方法。3.3程序正確性概念(續(xù))主要的程序正確性證明方法內(nèi)容－Whereweare？程序標準、標準的表示方法斷言與標準及{P}S{Q}程序正確性的概念程序正確性證明的過程3.4程序的非形式化正確性證明簡介設〔P，Q〕是一個標準，S是依照這個標準要求設計的程序，且是由語句s1，s2，…，sn組成的一個枚舉型程序〔即其執(zhí)行等于組成它的各個語句的逐一順序的執(zhí)行，其中的每個語句都只有一個入口和一個出口，且沒有GOTO語句〕。令P1,Q1,P2,Q2,…,Pn,Qn是2n個謂詞，且P=P1，Q=Qn。如果所有斷言{Pi}Si{Qi}，i=1，2，…,n,為真，并且每個蘊涵：QiPi+1，i=1，2，…,n成立，就稱〔P1，Q1〕，〔P2，Q2〕，…,〔Pn，Qn〕是{P}S{Q}的一個證明。例1：3.4程序的非形式化正確性證明簡介(續(xù))例1：令〔P，Q〕為：P：{i≥0∧s=b[0]+…+b[i]}Q：{i>0∧s