公理語義-Mann子目標Hoare

1、程序設計形式語義學程序設計形式語義學南京理工大學南京理工大學 計算機系計算機系張琨張琨二二四年八月二日四年八月二日2 公理語義公理語義2.5 程序正確性證明程序正確性證明Manna的子目標斷言法的子目標斷言法2.5 程序正確性證明程序正確性證明Manna的子目標斷言法的子目標斷言法n3. 證明驗證條件證明驗證條件n驗證條件驗證條件1： C1(x,y): x=0 = q(x,y,yf) q(0,yf,yf)即：即： x=0 = 0 0 yf 0 (0 0 yf 0 ) = yf = gcd(0, yf) 。 n驗證條件驗證條件2： C2(x,y): x 0 y q(x,y,yf) 即：即： x

2、0 y yf = gcd(y, x) = x 0 y 0 (x 0 y 0 ) = yf = gcd(x,y)n驗證條件驗證條件3， C3(x,y): x 0 y x q(x,y-x,yf) = q(x,y,yf) 即：即： x 0y xx0y-x 0(x 0 y-x 0 )=yf=gcd(x,y-x) = x 0 y 0 (x 0 y 0 ) = yf = gcd(x,y)n驗證條件驗證條件4， C4(x,y): x0 0 y0 0 (x0 0 y0 0 ) q(x0,y0,yf) = yf = gcd(x0,y0) BAAAn,212.5 程序正確性證明程序正確性證明Hoare的公理化方法

3、nHoare提出的公理和相應控制語句的證明規(guī)則。提出的公理和相應控制語句的證明規(guī)則。n4. 并置規(guī)則并置規(guī)則P S1R,R S2 QP S1;S2 QGoal Goal1 Goal2 Goal Goal1 Goal2 Log1 Goal Goal1 Goal2 Log1 Goal3 Goal Goal1 Goal2 Log1 Goal3 Log2 Goal Goal1 Goal2 Log1 Goal3 Log2 Goal4 Goal5 Goal Goal1 Goal2 Log1 Goal3 Log2 Goal4 Goal5 Log3 Log4 nR.W.Floyd在在1967年提出來的。設程序

4、年提出來的。設程序P的輸入斷言為的輸入斷言為(x)，利用良序集方法證明，利用良序集方法證明P關于關于(x)是終止的可按以下步驟進行：是終止的可按以下步驟進行：n1. 選取一個點集去截斷程序的各個循環(huán)部分，并且在每一截斷點選取一個點集去截斷程序的各個循環(huán)部分，并且在每一截斷點i處建立一個中間斷言處建立一個中間斷言qi(x,y)。程序就被分解為若干條通路，同時規(guī)定每一條通路都不包含有中間截斷點；。程序就被分解為若干條通路，同時規(guī)定每一條通路都不包含有中間截斷點；n2. 選取一個良序集選取一個良序集(W, )，并且在每一截斷點，并且在每一截斷點i處定義一個終止表達式處定義一個終止表達式Ei(x,y)

5、；n3. 證明所選取的斷言是證明所選取的斷言是“良斷言良斷言”。即滿足：。即滿足：n1）若對于每一個從程序入口到斷點）若對于每一個從程序入口到斷點i的通路的通路有：有： (x) R(x,y)= qi(x,r(x,y)n2）若對于每一個由斷點）若對于每一個由斷點i到斷點到斷點j的通路的通路有：有： qi(x,y)R(x,y)= qj(x,r(x,y)n這里，這里， R和和r分別表示通過通路分別表示通過通路的條件及通過通路的條件及通過通路后變量后變量y的值。的值。n4. 證明終止表達式是證明終止表達式是“良函數(shù)良函數(shù)”。即對于每個斷點。即對于每個斷點i有有 qi(x,y)= Ei(x,y) Wn5

6、. 證明終止條件成立。即對每一條從斷點證明終止條件成立。即對每一條從斷點i到斷點到斷點j，并且為某個循環(huán)的一部分的通路，并且為某個循環(huán)的一部分的通路有：有： qi(x,y) R(x,y)= Ei(x,y) Ej(x, r(x,y) ?(W, )是一個偏序集（滿足傳遞、反對稱和反自反性），如果不是一個偏序集（滿足傳遞、反對稱和反自反性），如果不存在由存在由W中的元素構成的無限遞減序列中的元素構成的無限遞減序列 a0 a1 a2 則稱則稱(W, )為良序集。為良序集。?nqB(x,y): y1 0 y2 0nqC(x,y): y1 0 y2 0nEB(x,y): y1nEC(x,y): y1 + 2y2n1. 通路1(AB)(x) = qB(x,y) qB(x, x1,x2,1)即： y1 + 2y2 y1 + 2y2 2.5 程序正確性證明程序正確性證明Kunth的計數(shù)器方法2.5 程序正確性證明程序正確性證明Kunth的計數(shù)器方法PROGRAM gcd1; VAR x, y, z, s: INTEGER; BEGIN READ(x,y); i := 0;I(x): x0 0 y0 0 (x0 0 y0 0 ) WHILE x 0 DOL(x,y): x 0 y 0 2x + y + i 2x0 + y0 BEGIN IF y x T