程序正确性证明课件

程式正確性證明

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

一段程式是正確的，是指這段程式能正確無誤地完成程式設計時所期望的功能。或者說：對任何一組允許的輸入資訊，程式執行後能得到一組和這組輸入資訊相對應的正確的輸出資訊。程式的正確性是衡量一個程式是否優秀的最基本條件。一段程式是錯誤的，是指（1）程式完成的事情並不是程式員想要完成的事情；（2）程式員想要程式完成的事情，程式並沒有完成。一般來說，程式中含有錯誤是很難避免的。錯誤可能有（1）設計時的錯誤；（2）程式編寫時的錯誤；（2）運行時的錯誤等。發現錯誤或儘量減少錯誤，是程式設計人員的努力方向，更是其職責。基本概念－程式測試如何發現錯誤或儘量減少錯誤？（1）設計程式時盡可能使用結構化程式設計方法，使程式設計過程規範化和標準化；（2）程式調試或運行時採用測試的方法去跟蹤程式的運行，從而發現與改正錯誤；（3）利用程式正確性證明的方法檢驗程式是否正確。程式測試：給程式一組或幾組初始值進行試運行，將運行的結果與實現已知的結果比較，若兩則相同，則認為程式是正確的，若兩則不同，則說明程式有錯誤。程式測試一個軟體的開發過程要經過程式設計，設計，編寫，測試與證明等一系列過程後，才能投入使用。已編寫好的軟體是否有錯誤是用戶極其關心的問題。程式測試程式測試的目的是為了發現程式的錯誤程式測試的方法是按習慣挑選各種數據，設計測試用例程式程式測試我們測試的程式一般有兩種情況：知道程式的輸入和輸出功能，而不知道程式的具體結構（常稱為黑盒子方法）已知程式內部結構和流向，測試的用例是根據程式內部邏輯來設計的（白盒子方法）黑盒子測試方法在VAX電腦上（字長32位），輸入X,Y整數，運行程式後輸出Z,則輸入數據可能值有2的64次方種可能。如果執行程式一次要1毫秒，那麼對所有數據進行測試需要5億年白盒子測試方法（圖例）白盒子測試方法（續）一程式流程如前圖所示。其中從a到b有5種路徑，再外套迴圈20次，這樣一個小程式的路徑測試就有5的20次方種。如果程式執行一次從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測試用例舉例在執行這個程式時，有各種不同的路徑，如：abdabedacbdacbed測試用例舉例我們可用白盒子方法設計測試用例，其任務是盡可能多地執行各種語句，以及調試到各種路徑。如選擇A=2,B=0,X=3則可執行路徑acbed此時能覆蓋到全部2個計算框，可發現一般的語句的錯誤我們通常把這種注重語句的複蓋叫“語句複蓋”測試用例舉例如選擇A=3,B=0,X=1A=2,B=1,X=3則可執行的路徑為acbdabed從所走路徑來看，上面這組數據要全面一些，它不僅通過全部兩個計算框，而且第一個判別框的兩邊都執行過一次。我們通常把這種注重選擇測試的複蓋叫做“判定複蓋”程式測試從以上兩個例子可以看出，測試通常是不充分的，它只能發現某些錯誤的存在，而不能證明錯誤的不存在。所有，在真正設計測試用例的過程種常常要考慮經濟性，可行性。測試的關鍵就是如何設計好高效，可行的用例程式。程式測試如選擇A=2,B=0,X=4A=1,B=1,X=1則可執行的路徑為

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

美國SEGUE公司的SILK系列自動測試技術。SILK系列自動化黑盒測試平臺能夠全面適應電子商務技術的最新發展，具有測試自動化，易用易維護，場景模擬精確，支持分佈式測試，支持多標準協議，擴展性強等優點。

基本概念－程式正確性證明測試通常是不充分的，它只能發現某些錯誤的存在，而不能證明錯誤的不存在。為解決程式測試的不足，開展了“程式正確性證明”的方法研究。“程式正確性證明”的研究歷史：（1）“程式正確性證明”開始於20世紀60年代末期，主要成就完成於70年代後期。（2）80年代OO技術的出現，對“程式正確性證明”提出了更高的要求，導致“程式正確性證明”研究日漸消退。（3）“程式正確性證明”的有關理論和技術，目前絕大多數只是使用在實驗室和小規模程式功能驗證中。（4）近幾年來，隨著UML、MDA等研究領域的出現，程式設計方法的研究焦點又逐漸回到程式的代碼的自動生成上來，程式正確性證明的理論又將成為一個研究熱點。基本概念－程式正確性證明程式正確性證明方法認為：一段程式的正確性是指給定一個輸入斷言以及程式的程式函數，能夠導出程式的輸出斷言。輸入斷言：滿足程式的輸入條件輸出斷言：滿足程式的輸出條件嚴格意義上的程式正確性定義分為部分正確性、終止性和完全正確性。定義：謂詞Φ(x)為輸入斷言，Ψ(x,z)為輸出斷言。（1）若對每一個使Φ(ζ)為真，並且程式計算終止的輸入資訊ζ、Ψ(ζ,P(ζ))為真，則稱程式P關於Φ和Ψ是部分正確的。（2）若對每一個使Φ(ζ)為真，程式的計算都能終止，則稱程式P對Φ是終止的。（3）若對每一個使Φ(ζ)為真的輸入資訊ζ

，程式的計算都能終止，並且Ψ(ζ,P(ζ))為真，則稱程式P關於Φ和Ψ是完全正確的。很顯然，（3）等價於（1）和（2）的同時成立。基本概念－程式正確性證明程式正確性證明的基本方法（1）部分正確性證明的方法：Floyd的不變式斷言法Manna的子目標斷言法Hoare的公理化方法（2）終止性證明的方法Floyd的良序集方法Knuth的計數器方法Manna的不動點方法（3）完全正確性證明的方法部分正確性證明－不變式斷言法

不變式斷言法是Floyd在1967年提出來的，是一個用於程式正確性證明的經典方法。Manna的子目標斷言法和Hoare的公理化方法都是在其基礎上形成的。使用不變式斷言法的基本過程：（1）建立斷言，建立輸入斷言和輸出斷言，如果程式中有迴圈，還要建立針對該迴圈的不變式斷言，是迴圈執行到中斷點時，斷言都為真。（2）建立檢驗條件，即程式運行通過各個通路時應該分別滿足的條件。對於通路i，設其輸入、輸出斷言分別為:Φi(x,y)、Ψ(x,y)，通過通路i的條件為:Ri(x,y),通過通路i後y的值變為ri(x,y),則檢驗條件為：Φi(x,y)∧Ri(x,y)－>Ψi(x,ri(x,y))（3）證明檢驗條件，即證明（2）中所列出的所有檢驗條件，如果每一條通路上的檢驗條件都為真，則該程式是部分正確的。部分正確性證明－不變式斷言法實例例1：設x1、x2是正整數，求它們的最大公約數，z=gcd(x1,x2)基本演算法：對於任意正整數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即反復執行（1）或（2），直到出現（3）中的情況部分正確性證明－不變式斷言法實例(x1,x2)->(y1,y2)y1=y2開始y1>y2y1->z結束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)考慮到存在迴圈，將迴圈在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設為中斷點後，程式執行中所有可能的通路分解為：通路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)考慮到存在迴圈，將迴圈在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],更求最大公約數的輾轉演算法，gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)，此時，檢驗條件的後項為真（成立），因此，整個蘊涵運算為真，即檢驗條件為真。同理可證條件3成立。整個流程圖的部分正確性得到了證明。部分正確性證明－不變式斷言法實例不變式斷言法也可以直接用於高級語言寫出的程式。具體使用時，以注釋的形式在程式的中斷點處加上斷言。例2：設x、y是非負整數，求它們的最大公約數，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)建立斷言。設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)建立檢驗條件。設x,y的初始值為x0,y0,假定輸入斷言成立，即要證明程式第一次執行到中斷點L處時，不變式斷言成立。此時的檢驗條件為：檢驗條件1：［x0>=0∧y0>=0∧(x0≠0∨y0≠0)]->[x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)]進一步證明，當檢驗條件1成立，程式控制迴圈後再次回到中斷點L處時，不變式斷言仍然成立。程式控制迴圈再次回到中斷點L處有兩個途徑，一個是y>=x成立時，另一個是y<x時。當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)]當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)]部分正確性證明－不變式斷言法實例最後要證明如果不變時斷言成立，但程式控制轉出迴圈時，輸出斷言成立。此時的檢驗條件為：檢驗條件4：［x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x=0]->y=gcd(x0,y0)(3)證明檢驗條件條件1：程式第一次執行到L處時，x=x0,y=y0,gcd(x,y)=gcd(x0,y0)成立，整個檢驗條件1成立。條件2：如果蘊涵式前項成立，由x>=0,y>=x成立可以推導出：x>=0∧y-x>=0成立。由x≠0成立可以推導出：x≠0∨y-x≠0成立,再根據數論中輾轉法可知：y>=x時，gcd(x,y)=gcd(x,y-x)成立，而gcd(x,y)=gcd(x0,y0)成立，因此gcd(x,y-x)=gcd(x0,y0)成立，由此，條件2為真。條件3：如果蘊涵式前項成立，由x,y互換，由合適公式的互換定律，可以推導出條件2為真。部分正確性證明－不變式斷言法實例條件4：如果蘊涵式前項成立，由x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x=0可以推出x=0,再由(x≠0∨y≠0)成立可以推導出y>0

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

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)建立斷言。設x,y的初始值為x0,y0,

輸入斷言：Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)輸出斷言Ψ(x,z):z=gcd(x0,y0)在迴圈中斷點L處建立子目標斷言q(x,y,yf)：x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)(2)建立檢驗條件。首先證明當程式控制最後一次通過L時，及控制轉出迴圈時，子目標斷言應該成立。此時的檢驗條件為：檢驗條件1：X=0->[x>=0∧y>=0∧(x≠0∨y≠0)->yf=gcd(x,y)]

接下來要進一步證明，在迴圈終止前，子目標斷言也應該成立。程式控制迴圈再次回到中斷點L處有兩個途徑，一個是y>=x成立時，另一個是y<x時。當y>=x成立時：檢驗條件2：［q(x,y-x,yf)∧x≠0∧y>=x]->q(x,y,yf)即通過迴圈的then通路之後的子目標斷言蘊涵通過此通路之前的子目標斷言。部分正確性證明－子目標斷言法實例當y<x成立時：檢驗條件3：［q(y,x,yf)∧x≠0∧y<x]->q(x,y,yf)即通過迴圈的else通路之後的子目標斷言蘊涵通過此通路之前的子目標斷言。接下來要進一步證明，如果輸入斷言為真，且當控制第一次通過L時子目標斷言為真，則輸出斷言為真，整個反向推理結束。檢驗條件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)]關鍵點在於x=0時，yf是否等於gcd(x,y)？退出迴圈後，yf=y，gcd(x,y)=gcd(0,yf),根據數論知識，gcd(0,yf)=yf是成立的，即yf=gcd(x,y)成立。部分正確性證明－子目標斷言法實例條件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)]如果蘊涵式前項成立，存在x≠0，y>=x為真，則x>=0∧y>=0∧(x≠0∨y≠0)為真。由再根據數論中輾轉法可知：y>=x時，gcd(x,y)=gcd(x,y-x)成立，因此yf=gcd(x,y)成立，由此，條件2為真。部分正確性證明－子目標斷言法實例條件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)]如果蘊涵式前項成立，由於x,y互換，由合適公式的互換定律，可以推導出x>=0∧y>=0∧(x≠0∨y≠0)為真，根據數論中輾轉法可知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為真。部分正確性證明－子目標斷言法實例根據子目標斷言法的定義，證明了：（1）每當控制到達L時，子目標斷言都是成立的；（2）當輸入斷言為真，且當程式第一次運行到L時子目標斷言成立，則輸出斷言為真。

事實上，不論是子目標斷言法還是不變式斷言法，其關鍵都在於建立正確的斷言描述。但建立正確的斷言環主要依賴程式設計人員的實踐經驗，還沒有一個有效的、系統的方法。程式的終止性證明－計數器法計數器法是由D.E.knuth在1968年提出來的一種與不變式斷言相配套的程式終止性證明的基本方法。基本思想：對程式中的每一個迴圈附加一個計數器變數，進入迴圈之前，計數器置為0，迴圈通路每執行一次，計數器加1。同時，對每一個迴圈提供一個新的中間斷言，用來表示相應的計數器不會超過某個固定的界限。然後，證明此中間斷言是不變式斷言，就可以斷定迴圈只能執行有限次，因而程式是終止的。程式的終止性證明－計數器法實例例1：用計數器法證明程式的終止性設x、y是非負整數，求它們的最大公約數，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程式的終止性證明－計數器法實例

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

將斷言直接寫入程式中（這段代碼中，計數器i的設置有問題,請大家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｝//計數器斷言ify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;i:=i+1;endz:=y;write(z);End程式的終止性證明－計數器法實例（2）建立檢驗條件。設x,y的初始值為x0,y0,假定輸入斷言成立，即要證明程式第一次執行到中斷點L處時，中間斷言成立。此時，x=x0,y=y0,i=0,檢驗條件為：檢驗條件1：［x0>=0∧y0>=0∧(x0≠0∨y0≠0)]->[x0>=0∧y0>=0∧(2x0+y0<=2x0+y0)]

進一步證明，當檢驗條件1成立，程式控制迴圈再次回到計數器中斷點L處時，中間斷言仍然成立。程式控制迴圈再次回到中斷點L處有兩個途徑，一個是y>=x成立時，另一個是y<x時。當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)]當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)]程式的終止性證明－計數器法實例(3)證明檢驗條件條件1：程式第一次執行到L處時，(2x0+y0<=2x0+y