程序正確性證明課件

程序正確性證明

基本概念－程序正確性的定義

一段程序是正確的，是指這段程序能正確無誤地完成程序設(shè)計時所期望的功能?；蛘哒f：對任何一組允許的輸入信息，程序執(zhí)行后能得到一組和這組輸入信息相對應(yīng)的正確的輸出信息。程序的正確性是衡量一個程序是否優(yōu)秀的最基本條件。一段程序是錯誤的，是指（1）程序完成的事情并不是程序員想要完成的事情；（2）程序員想要程序完成的事情，程序并沒有完成。一般來說，程序中含有錯誤是很難避免的。錯誤可能有（1）設(shè)計時的錯誤；（2）程序編寫時的錯誤；（2）運行時的錯誤等。發(fā)現(xiàn)錯誤或盡量減少錯誤，是程序設(shè)計人員的努力方向，更是其職責(zé)?；靖拍睿绦驕y試如何發(fā)現(xiàn)錯誤或盡量減少錯誤？（1）設(shè)計程序時盡可能使用結(jié)構(gòu)化程序設(shè)計方法，使程序設(shè)計過程規(guī)范化和標(biāo)準(zhǔn)化；（2）程序調(diào)試或運行時采用測試的方法去跟蹤程序的運行，從而發(fā)現(xiàn)與改正錯誤；（3）利用程序正確性證明的方法檢驗程序是否正確。程序測試：給程序一組或幾組初始值進(jìn)行試運行，將運行的結(jié)果與實現(xiàn)已知的結(jié)果比較，若兩則相同，則認(rèn)為程序是正確的，若兩則不同，則說明程序有錯誤。程序測試一個軟件的開發(fā)過程要經(jīng)過程序設(shè)計，設(shè)計，編寫，測試與證明等一系列過程后，才能投入使用。已編寫好的軟件是否有錯誤是用戶極其關(guān)心的問題。程序測試程序測試的目的是為了發(fā)現(xiàn)程序的錯誤程序測試的方法是按習(xí)慣挑選各種數(shù)據(jù)，設(shè)計測試用例程序程序測試我們測試的程序一般有兩種情況：知道程序的輸入和輸出功能，而不知道程序的具體結(jié)構(gòu)（常稱為黑盒子方法）已知程序內(nèi)部結(jié)構(gòu)和流向，測試的用例是根據(jù)程序內(nèi)部邏輯來設(shè)計的（白盒子方法）黑盒子測試方法在VAX計算機(jī)上（字長32位），輸入X,Y整數(shù)，運行程序后輸出Z,則輸入數(shù)據(jù)可能值有2的64次方種可能。如果執(zhí)行程序一次要1毫秒，那么對所有數(shù)據(jù)進(jìn)行測試需要5億年白盒子測試方法（圖例）白盒子測試方法（續(xù)）一程序流程如前圖所示。其中從a到b有5種路徑，再外套循環(huán)20次，這樣一個小程序的路徑測試就有5的20次方種。如果程序執(zhí)行一次從a到b平均花1分鐘，整個路徑需要運行2億年才能走遍。測試用例舉例例1試測試下面這一程序ProcedureP(varA,B:REAL)BeginIf(A>1)and(B=0)thenX:=X/A;If(A=2)or(X>1)thenX:=X+1;end測試用例舉例在執(zhí)行這個程序時，有各種不同的路徑，如：abdabedacbdacbed測試用例舉例我們可用白盒子方法設(shè)計測試用例，其任務(wù)是盡可能多地執(zhí)行各種語句，以及調(diào)試到各種路徑。如選擇A=2,B=0,X=3則可執(zhí)行路徑acbed此時能覆蓋到全部2個計算框，可發(fā)現(xiàn)一般的語句的錯誤我們通常把這種注重語句的復(fù)蓋叫“語句復(fù)蓋”測試用例舉例如選擇A=3,B=0,X=1A=2,B=1,X=3則可執(zhí)行的路徑為acbdabed從所走路徑來看，上面這組數(shù)據(jù)要全面一些，它不僅通過全部兩個計算框，而且第一個判別框的兩邊都執(zhí)行過一次。我們通常把這種注重選擇測試的復(fù)蓋叫做“判定復(fù)蓋”程序測試從以上兩個例子可以看出，測試通常是不充分的，它只能發(fā)現(xiàn)某些錯誤的存在，而不能證明錯誤的不存在。所有，在真正設(shè)計測試用例的過程種常常要考慮經(jīng)濟(jì)性，可行性。測試的關(guān)鍵就是如何設(shè)計好高效，可行的用例程序。程序測試如選擇A=2,B=0,X=4A=1,B=1,X=1則可執(zhí)行的路徑為

acbedabd從這組數(shù)據(jù)來看，它注意了4個條件A>1,B=0,A=2和X>1的復(fù)蓋。我們稱這種注重判斷的復(fù)蓋為“條件復(fù)蓋”程序測試以上這些數(shù)據(jù)雖然均達(dá)到一些測試目的，且各有側(cè)重，但是都是不充分的。如從條件出發(fā)，用組合的辦法使各個條件都能執(zhí)行到，則我們可以寫出以下8種條件組合：1)A>1,B=02)A>1,B<>0;(<>是不等號)3)A<=1,B=04)A<=1,B<>05)A=2,X>16)A=2,X<=17)A<>2,X>18)A<>2,X<=1程序測試根據(jù)這8種條件組合，又可以優(yōu)化組成如下4組數(shù)據(jù)：A=2,B=0,X=4A=2,B=1,X=1A=1,B=0,X=2A=1,B=1,X=1它們都能使各種條件均能出現(xiàn)一次。雖然這個組合方法比較方便，邏輯也很清楚，且對執(zhí)行條件來說還是比較全面的，但是仍然又未走遍的路徑，如acbd程序測試在測試時，還要注意到計算機(jī)執(zhí)行多個條件的特點，即它必須把多個條件分解為簡單判別才能執(zhí)行，如上述例子可分解為右圖。例子2某個TRIANGLE程序，用3個整數(shù)表示一個三角形的3條邊長。當(dāng)輸入3個整數(shù)后，該程序輸出一個結(jié)果，指出這三角形是等腰，等邊，還是不等邊三角形。程序測試這個例子只知程序的功能，而不知內(nèi)部的邏輯與結(jié)構(gòu)。在選擇數(shù)據(jù)組來測試程序時，我們可以憑經(jīng)驗，考慮如下情況：1）合理構(gòu)成等腰三角形2）合理構(gòu)成等邊三角形3）合理構(gòu)成不等邊三角形4）等腰三角形的三種排列5）三個正數(shù)，其中兩個數(shù)之和等于第三個數(shù)6）兩邊之和等于第三邊的三種排列7）三個正數(shù)，其中兩個數(shù)之和小于第三個數(shù)8）兩邊之和小于第三邊的三種排列程序測試9）輸入三個數(shù)，其中含有010）輸入三個數(shù)，其中含有負(fù)數(shù)11）輸入三個數(shù)，其中含有非整數(shù)值12）輸入三個均為0的數(shù)13）輸入三個均為非法字符列出各種產(chǎn)生的情況來測試的方法顯然是黑盒子方法。它不關(guān)心盒子內(nèi)程序的具體邏輯，只是根據(jù)程序功能來設(shè)計測試用例常用的測試數(shù)據(jù)選擇方法有等價分類法，邊緣值分析法，因果圖方法和錯誤推測法等。程序測試等價分類法：根據(jù)程序功能將輸入的數(shù)據(jù)劃分為若干個等價類，然后考慮數(shù)據(jù)選擇，設(shè)計出測試用例。如上例中，我們可將輸入條件劃分為三種三角形或劃分為合理三角形，不合理三角形等二項。在選擇時要同時考慮合法的和不合法的數(shù)據(jù)。有時，還要憑經(jīng)驗和其他知識進(jìn)行更全面的測試劃分。程序測試程序出錯通常發(fā)生在邊界狀態(tài)，所以在測試中我們常常首先根據(jù)程序的功能確定邊緣情況的數(shù)據(jù)變化，以便設(shè)計測試用例。對邊界狀態(tài)進(jìn)行分析，以設(shè)計測試用例來測試程序的方法稱為邊緣值分析法。邊緣值的選擇要根據(jù)題目實際情況有針對性地，有一定創(chuàng)造性地進(jìn)行。邊緣值分析法可以考慮如下幾種情況：1）恰好在邊界附近，且欲越界的數(shù)據(jù)2）取最大或最小值，最多或最少值加減1的數(shù)據(jù)3）循環(huán)或迭代的初始值和終值數(shù)據(jù)4）有序集合的第一個或最后一個數(shù)據(jù)元素5）零點附近的數(shù)據(jù)6）最大誤差值的數(shù)據(jù)7）文件處理時的“空文件”，“nil”，”first”等數(shù)據(jù)程序測試總之，程序測試的黑盒子方法常憑經(jīng)驗進(jìn)行，在設(shè)計測試用例時可以綜合使用上述各種方法。在設(shè)計測試數(shù)據(jù)時，我們應(yīng)該考慮認(rèn)為最易出錯和最易忽略的地方，進(jìn)行重點測試。程序測試設(shè)計測試用例的幾點原則：1）測試用例的設(shè)計者最好和程序設(shè)計者不是同一個人2）對輸入的數(shù)據(jù)欲輸出的數(shù)據(jù)要有詳細(xì)的了解與描述3）測試用例數(shù)據(jù)復(fù)蓋面盡可能大4）測試時既應(yīng)注意程序是否做了它預(yù)定的事，又應(yīng)該注意檢查它不應(yīng)該做的事5）設(shè)計測試用例時要考慮經(jīng)濟(jì)性和可行性。程序測試美國MI公司開發(fā)的TestDirector產(chǎn)品作為測試管理流程平臺，運用WinRunner和QuickTestProfessional作為自動化測試工具，推薦LoadRunner作為性能測試工具。MI公司作為一個跨國型業(yè)內(nèi)專業(yè)公司，在自動化測試方面積累了豐富的經(jīng)驗。其測試工具作為目前測試市場的主流工具，市場占有率超過50％，從測試平臺的先進(jìn)性上來說，達(dá)到了國際上主流標(biāo)準(zhǔn)。

美國SEGUE公司的SILK系列自動測試技術(shù)。SILK系列自動化黑盒測試平臺能夠全面適應(yīng)電子商務(wù)技術(shù)的最新發(fā)展，具有測試自動化，易用易維護(hù)，場景模擬精確，支持分布式測試，支持多標(biāo)準(zhǔn)協(xié)議，擴(kuò)展性強(qiáng)等優(yōu)點。

基本概念－程序正確性證明測試通常是不充分的，它只能發(fā)現(xiàn)某些錯誤的存在，而不能證明錯誤的不存在。為解決程序測試的不足，開展了“程序正確性證明”的方法研究?！俺绦蛘_性證明”的研究歷史：（1）“程序正確性證明”開始于20世紀(jì)60年代末期，主要成就完成于70年代后期。（2）80年代OO技術(shù)的出現(xiàn)，對“程序正確性證明”提出了更高的要求，導(dǎo)致“程序正確性證明”研究日漸消退。（3）“程序正確性證明”的有關(guān)理論和技術(shù)，目前絕大多數(shù)只是使用在實驗室和小規(guī)模程序功能驗證中。（4）近幾年來，隨著UML、MDA等研究領(lǐng)域的出現(xiàn)，程序設(shè)計方法的研究焦點又逐漸回到程序的代碼的自動生成上來，程序正確性證明的理論又將成為一個研究熱點。基本概念－程序正確性證明程序正確性證明方法認(rèn)為：一段程序的正確性是指給定一個輸入斷言以及程序的程序函數(shù)，能夠?qū)С龀绦虻妮敵鰯嘌?。輸入斷言：滿足程序的輸入條件輸出斷言：滿足程序的輸出條件嚴(yán)格意義上的程序正確性定義分為部分正確性、終止性和完全正確性。定義：謂詞Φ(x)為輸入斷言，Ψ(x,z)為輸出斷言。（1）若對每一個使Φ(ζ)為真，并且程序計算終止的輸入信息ζ、Ψ(ζ,P(ζ))為真，則稱程序P關(guān)于Φ和Ψ是部分正確的。（2）若對每一個使Φ(ζ)為真，程序的計算都能終止，則稱程序P對Φ是終止的。（3）若對每一個使Φ(ζ)為真的輸入信息ζ

，程序的計算都能終止，并且Ψ(ζ,P(ζ))為真，則稱程序P關(guān)于Φ和Ψ是完全正確的。很顯然，（3）等價于（1）和（2）的同時成立?；靖拍睿绦蛘_性證明程序正確性證明的基本方法（1）部分正確性證明的方法：Floyd的不變式斷言法Manna的子目標(biāo)斷言法Hoare的公理化方法（2）終止性證明的方法Floyd的良序集方法Knuth的計數(shù)器方法Manna的不動點方法（3）完全正確性證明的方法部分正確性證明－不變式斷言法

不變式斷言法是Floyd在1967年提出來的，是一個用于程序正確性證明的經(jīng)典方法。Manna的子目標(biāo)斷言法和Hoare的公理化方法都是在其基礎(chǔ)上形成的。使用不變式斷言法的基本過程：（1）建立斷言，建立輸入斷言和輸出斷言，如果程序中有循環(huán)，還要建立針對該循環(huán)的不變式斷言，是循環(huán)執(zhí)行到斷點時，斷言都為真。（2）建立檢驗條件，即程序運行通過各個通路時應(yīng)該分別滿足的條件。對于通路i，設(shè)其輸入、輸出斷言分別為:Φi(x,y)、Ψ(x,y)，通過通路i的條件為:Ri(x,y),通過通路i后y的值變?yōu)閞i(x,y),則檢驗條件為：Φi(x,y)∧Ri(x,y)－>Ψi(x,ri(x,y))（3）證明檢驗條件，即證明（2）中所列出的所有檢驗條件，如果每一條通路上的檢驗條件都為真，則該程序是部分正確的。部分正確性證明－不變式斷言法實例例1：設(shè)x1、x2是正整數(shù)，求它們的最大公約數(shù)，z=gcd(x1,x2)基本算法：對于任意正整數(shù)x1,x2，有：（1）若x1>x2,gcd(x1,x2)=gcd(x1-x2,x2)（2）若x2>x1,gcd(x1,x2)=gcd(x1,x2-x1)（3）若x1=x2,gcd(x1,x2)=x1=x2即反復(fù)執(zhí)行（1）或（2），直到出現(xiàn)（3）中的情況部分正確性證明－不變式斷言法實例(x1,x2)->(y1,y2)y1=y2開始y1>y2y1->z結(jié)束y2-y1->y2y1-y2->y1B······

P(x,y)A······

Φ(x)TGC······

Ψ(x,z)FEDFT部分正確性證明－不變式斷言法實例利用不變式斷言法實例證明該流程框圖的部分正確性:(1)建立斷言輸入斷言Φ(x):x1>0∧x2>0輸出斷言Ψ(x,z):z=gcd(x1,x2)考慮到存在循環(huán)，將循環(huán)在B點斷開，建立B點的不變式斷言：P(x,y):x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)其中，x,y分別表示(x1,x2)、(y1,y2)。(2)建立檢驗條件將B設(shè)為斷點后，程序執(zhí)行中所有可能的通路分解為：通路1：A->B通路2：B->D->B通路3：B->E->B通路4：B->G->C部分正確性證明－不變式斷言法實例利用不變式斷言法實例證明該流程框圖的部分正確性:(1)建立斷言輸入斷言Φ(x):x1>0∧x2>0輸出斷言Ψ(x,z):z=gcd(x1,x2)考慮到存在循環(huán)，將循環(huán)在B點斷開，建立B點的不變式斷言：P(x,y):x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)其中，x,y分別表示(x1,x2)、(y1,y2)。(2)建立檢驗條件通路1的檢驗條件：通路1（A->B）是無條件的,即R1(x,y)=1（恒為真），同時Φ1(x)－>P(x,y),具體可寫為：［x1>0∧x2>0]->[x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)]部分正確性證明－不變式斷言法實例通路2的檢驗條件：R2(x,y)=[y1≠y2∧y1>y2>],通路2的輸入、輸出斷言均為：P(x,y),因而檢驗條件為：［P(x,y)∧y1≠y2∧y1>y2>]->P(x,y1-y2,y2),也即：[x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1≠y2∧y1>y2]->[x1>0∧x2>0∧(y1-y2)>0∧y2>0∧gcd(y1-y2,y2)=gcd(x1,x2)]通路3的檢驗條件：R3(x,y)=[y1≠y2∧y1<y2>],通路3的輸入、輸出斷言均為：P(x,y),因而檢驗條件為：［P(x,y)∧y1≠y2∧y1<y2>]->P(x,y1,y2-y1),也即：[x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1≠y2∧y1<y2]->[x1>0∧x2>0∧y1>0∧(y2-y1)>0∧gcd(y1,y2-y1)=gcd(x1,x2)]通路4的檢驗條件：R4(x,y)=[y1=y2],通路4的輸入斷言為P(x,y),輸出斷言為Ψ(x1,y2)，檢驗條件為：［P(x,y)∧y1=y2]->Ψ(x1,y2)考試時間下周四晚7：00------9：30地點西12S401到S404，S406到S412周五上課時間、地點不變部分正確性證明－不變式斷言法實例（3）證明檢驗條件是否成立通路1、通路4的檢驗條件為真對于通路2，檢驗條件為：[x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1≠y2∧y1>y2]->[x1>0∧x2>0∧(y1-y2)>0∧y2>0∧gcd(y1-y2,y2)=gcd(x1,x2)]檢驗條件的前項為真（成立）時，[y1>y2]->[y1-y2>0],更求最大公約數(shù)的輾轉(zhuǎn)算法，gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)，此時，檢驗條件的后項為真（成立），因此，整個蘊(yùn)涵運算為真，即檢驗條件為真。同理可證條件3成立。整個流程圖的部分正確性得到了證明。部分正確性證明－不變式斷言法實例不變式斷言法也可以直接用于高級語言寫出的程序。具體使用時，以注釋的形式在程序的斷點處加上斷言。例2：設(shè)x、y是非負(fù)整數(shù)，求它們的最大公約數(shù)，z=gcd(x,y)ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;endz:=y;write(z);end部分正確性證明－不變式斷言法實例(1)建立斷言。設(shè)x,y的初始值為x0,y0,輸入斷言：Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)輸出斷言Ψ(x,z):z=gcd(x0,y0)不變式斷言：P(x,y):x>=0∧y>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)將斷言直接寫入程序中：ProgramAvarx,y,z,s:integer;beginread(x,y);｛x0>=0∧y0>=0∧(x0≠0∨y0≠0)｝//輸入斷言whilex≠0doL：｛x>=0∧y>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)｝//不變式斷言ify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;endz:=y;{z=gcd(x0,y0)}//輸出斷言write(z);end部分正確性證明－不變式斷言法實例(2)建立檢驗條件。設(shè)x,y的初始值為x0,y0,假定輸入斷言成立，即要證明程序第一次執(zhí)行到斷點L處時，不變式斷言成立。此時的檢驗條件為：檢驗條件1：［x0>=0∧y0>=0∧(x0≠0∨y0≠0)]->[x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)]進(jìn)一步證明，當(dāng)檢驗條件1成立，程序控制循環(huán)后再次回到斷點L處時，不變式斷言仍然成立。程序控制循環(huán)再次回到斷點L處有兩個途徑，一個是y>=x成立時，另一個是y<x時。當(dāng)y>=x成立時：檢驗條件2：［x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x≠0∧y>=x]->[x>=0∧y-x>=0∧(x≠0∨y-x≠0)∧gcd(x,y-x)=gcd(x0,y0)]當(dāng)y<x成立時：檢驗條件3：［x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x≠0∧y<x]->[y>=0∧x>=0∧(y≠0∨x≠0)∧gcd(y,x)=gcd(x0,y0)]部分正確性證明－不變式斷言法實例最后要證明如果不變時斷言成立，但程序控制轉(zhuǎn)出循環(huán)時，輸出斷言成立。此時的檢驗條件為：檢驗條件4：［x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x=0]->y=gcd(x0,y0)(3)證明檢驗條件條件1：程序第一次執(zhí)行到L處時，x=x0,y=y0,gcd(x,y)=gcd(x0,y0)成立，整個檢驗條件1成立。條件2：如果蘊(yùn)涵式前項成立，由x>=0,y>=x成立可以推導(dǎo)出：x>=0∧y-x>=0成立。由x≠0成立可以推導(dǎo)出：x≠0∨y-x≠0成立,再根據(jù)數(shù)論中輾轉(zhuǎn)法可知：y>=x時，gcd(x,y)=gcd(x,y-x)成立，而gcd(x,y)=gcd(x0,y0)成立，因此gcd(x,y-x)=gcd(x0,y0)成立，由此，條件2為真。條件3：如果蘊(yùn)涵式前項成立，由x,y互換，由合適公式的互換定律，可以推導(dǎo)出條件2為真。部分正確性證明－不變式斷言法實例條件4：如果蘊(yùn)涵式前項成立，由x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x=0可以推出x=0,再由(x≠0∨y≠0)成立可以推導(dǎo)出y>0

。再根據(jù)數(shù)論中輾轉(zhuǎn)法可知：x=0,y>0時，gcd(0,y)=y成立，由此，條件4為真。整個程序的部分正確性得以證明。整個程序的部分正確性不能保證整個程序的完全正確性。在例1中，若將問題前提改為與例2一致：設(shè)x1、x2是非負(fù)整數(shù)，求它們的最大公約數(shù)，z=gcd(x1,x2)輸入斷言：x>=0∧y>=0∧(x≠0∨y≠0)可能不能保證整個程序的運行的正常終止。如x>0,y=0時,程序會出現(xiàn)什么情況？部分正確性證明－子目標(biāo)斷言法子目標(biāo)斷言法是在不變式斷言法基礎(chǔ)發(fā)展起來的一種證明程序部分正確性的。與不變式斷言法主要區(qū)別在于：（1）對循環(huán)所建立的斷言不同。不變式斷言描述了程序變量y的中間值與初值之間的關(guān)系，而子目標(biāo)斷言描述的是y的中間值與循環(huán)終止時的最終值yf之間的關(guān)系；（2）進(jìn)行歸納的方向不同。不變式斷言法沿著程序正常執(zhí)行的方向進(jìn)行歸納，而子目標(biāo)斷言則沿著相反的方向進(jìn)行歸納。例1設(shè)x、y是非負(fù)整數(shù)，求它們的最大公約數(shù)，

z=gcd(x,y)

ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;endz:=y;write(z);end部分正確性證明－子目標(biāo)斷言法實例

(1)建立斷言。設(shè)x,y的初始值為x0,y0,

輸入斷言：Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)輸出斷言Ψ(x,z):z=gcd(x0,y0)在循環(huán)斷點L處建立子目標(biāo)斷言q(x,y,yf)：x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)(2)建立檢驗條件。首先證明當(dāng)程序控制最后一次通過L時，及控制轉(zhuǎn)出循環(huán)時，子目標(biāo)斷言應(yīng)該成立。此時的檢驗條件為：檢驗條件1：X=0->[x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)]

接下來要進(jìn)一步證明，在循環(huán)終止前，子目標(biāo)斷言也應(yīng)該成立。程序控制循環(huán)再次回到斷點L處有兩個途徑，一個是y>=x成立時，另一個是y<x時。當(dāng)y>=x成立時：檢驗條件2：［q(x,y-x,yf)∧x≠0∧y>=x]->q(x,y,yf)即通過循環(huán)的then通路之后的子目標(biāo)斷言蘊(yùn)涵通過此通路之前的子目標(biāo)斷言。部分正確性證明－子目標(biāo)斷言法實例當(dāng)y<x成立時：檢驗條件3：［q(y,x,yf)∧x≠0∧y<x]->q(x,y,yf)即通過循環(huán)的else通路之后的子目標(biāo)斷言蘊(yùn)涵通過此通路之前的子目標(biāo)斷言。接下來要進(jìn)一步證明，如果輸入斷言為真，且當(dāng)控制第一次通過L時子目標(biāo)斷言為真，則輸出斷言為真，整個反向推理結(jié)束。檢驗條件4：x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧q(x0,y0,yf)->yf=gcd(x0,y0)(3)證明檢驗條件條件1：x=0->[x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)]關(guān)鍵點在于x=0時，yf是否等于gcd(x,y)？退出循環(huán)后，yf=y，gcd(x,y)=gcd(0,yf),根據(jù)數(shù)論知識，gcd(0,yf)=yf是成立的，即yf=gcd(x,y)成立。部分正確性證明－子目標(biāo)斷言法實例條件2：［q(x,y-x,yf)∧x≠0∧y>=x]->q(x,y,yf)，考慮到q(x,y,yf)為：x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)，代入條件2：[[x>=0∧y-x>=0∧(x≠0∨y-x≠0)->yf=gcd(x,y-x)]∧x≠0∧y>=x]->[x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)]如果蘊(yùn)涵式前項成立，存在x≠0，y>=x為真，則x>=0∧y>=0∧(x≠0∨y≠0)為真。由再根據(jù)數(shù)論中輾轉(zhuǎn)法可知：y>=x時，gcd(x,y)=gcd(x,y-x)成立，因此yf=gcd(x,y)成立，由此，條件2為真。部分正確性證明－子目標(biāo)斷言法實例條件3：［q(y,x,yf)∧x≠0∧y<x]->q(x,y,yf)，考慮到q(x,y,yf)為：x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)，代入條件3：[[y>=0∧x>=0∧(y≠0∨x≠0)->yf=gcd(y,x)]∧x≠0∧y<x]->[x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)]如果蘊(yùn)涵式前項成立，由于x,y互換，由合適公式的互換定律，可以推導(dǎo)出x>=0∧y>=0∧(x≠0∨y≠0)為真，根據(jù)數(shù)論中輾轉(zhuǎn)法可知gcd(x,y)=gcd(y,x)，由此，條件3為真。檢驗條件4：x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧q(x0,y0,yf)->yf=gcd(x0,y0)，考慮到q(x0,y0,yf)為：x0>=0∧y0>=0∧(x0≠0∨y0≠0)->yf=gcd(x0,y0)，代入條件4：[x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧[x0>=0∧y0>=0∧(x0≠0∨y0≠0)->yf=gcd(x0,y0)]]->yf=gcd(x0,y0),很顯然，條件4為真。部分正確性證明－子目標(biāo)斷言法實例根據(jù)子目標(biāo)斷言法的定義，證明了：（1）每當(dāng)控制到達(dá)L時，子目標(biāo)斷言都是成立的；（2）當(dāng)輸入斷言為真，且當(dāng)程序第一次運行到L時子目標(biāo)斷言成立，則輸出斷言為真。

事實上，不論是子目標(biāo)斷言法還是不變式斷言法，其關(guān)鍵都在于建立正確的斷言描述。但建立正確的斷言環(huán)主要依賴程序設(shè)計人員的實踐經(jīng)驗，還沒有一個有效的、系統(tǒng)的方法。程序的終止性證明－計數(shù)器法計數(shù)器法是由D.E.knuth在1968年提出來的一種與不變式斷言相配套的程序終止性證明的基本方法?；舅枷耄簩Τ绦蛑械拿恳粋€循環(huán)附加一個計數(shù)器變量，進(jìn)入循環(huán)之前，計數(shù)器置為0，循環(huán)通路每執(zhí)行一次，計數(shù)器加1。同時，對每一個循環(huán)提供一個新的中間斷言，用來表示相應(yīng)的計數(shù)器不會超過某個固定的界限。然后，證明此中間斷言是不變式斷言，就可以斷定循環(huán)只能執(zhí)行有限次，因而程序是終止的。程序的終止性證明－計數(shù)器法實例例1：用計數(shù)器法證明程序的終止性設(shè)x、y是非負(fù)整數(shù)，求它們的最大公約數(shù)，z=gcd(x,y)ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;endz:=y;write(z);End程序的終止性證明－計數(shù)器法實例

建立輸入斷言：Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)（1）建立計數(shù)器I及其中間斷言:x>=0∧y>=0∧2x+y+i<=2x0+y0考慮到輸入斷言：x0>=0∧y0>=0∧(x0≠0∨y0≠0)，可以推斷i的上限不能超過2x0+y0

將斷言直接寫入程序中（這段代碼中，計數(shù)器i的設(shè)置有問題,請大家ProgramA

思考該如何修改？）varx,y,z,s:integer;beginread(x,y);｛x0>=0∧y0>=0∧(x0≠0∨y0≠0)｝//輸入斷言whilex≠0doL：｛x>=0∧y>=0∧2x+y+i<=2x0+y0｝//計數(shù)器斷言ify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;i:=i+1;endz:=y;write(z);End程序的終止性證明－計數(shù)器法實例（2）建立檢驗條件。設(shè)x,y的初始值為x0,y0,假定輸入斷言成立，即要證明程序第一次執(zhí)行到斷點L處時，中間斷言成立。此時，x=x0,y=y0,i=0,檢驗條件為：檢驗條件1：［x0>=0∧y0>=0∧(x0≠0∨y0≠0)]->[x0>=0∧y0>=0∧(2x0+y0<=2x0+y0)]

進(jìn)一步證明，當(dāng)檢驗條件1成立，程序控制循環(huán)再次回到計數(shù)器斷點L處時，中間斷言仍然成立。程序控制循環(huán)再次回到斷點L處有兩個途徑，一個是y>=x成立時，另一個是y<x時。當(dāng)y>=x成立時：檢驗條件2：［x>=0∧y>=0∧(2x+y+i<=2x0+y0)∧(x≠0∧y>=x)]->[x>=0∧y-x>=0∧(2x+y-x+i+1<=2x0+y0)]當(dāng)y<x成立時：檢驗條件3：［x>=0∧y>=0∧(2x+y+i<=2x0+y0)∧(x≠0∧y<x)]->[y>=0∧x>=0∧(2y+x+i+1<=2x0+y0)]程序的終止性證明－計數(shù)器法實例(3)證明檢驗條件條件1：程序第一次執(zhí)行到L處時，(2x0+y0<=2x0+