程序的形式推導技術

程序的形式推導技術第1頁，共38頁，2023年，2月20日，星期二謂詞轉換器wp(S,R)：表示一個狀態(tài)的集合，從其中的任何一個狀態(tài)出發(fā)，執(zhí)行S后必定會終止，終止時滿足R，是最弱的前置斷言。要證{Q}S{R}，即證：Q=>wp(S,R)s終止wp(S,R)R一些狀態(tài)集合后置條件第2頁，共38頁，2023年，2月20日，星期二最弱前置謂詞的幾個性質公理性質1：排奇律wp(S,F)=F要從某個狀態(tài)集的任何一個狀態(tài)出發(fā)執(zhí)行S后必定會終止，終止時滿足F，即使F為真，這樣的狀態(tài)是找不到的，因此對應的狀態(tài)集為空。第3頁，共38頁，2023年，2月20日，星期二最弱前置謂詞的幾個性質公理性質2：合取分配律wp(S,Q)wp(S,R)=wp(S,QR)證明：設任何一個狀態(tài)Pwp(S,Q)wp(S,R) 表示從P出發(fā)經(jīng)S執(zhí)行后必終止，終止時滿足Q；同時從P出發(fā)經(jīng)S執(zhí)行后必終止，終止時滿足R，也即滿足QR。所以，Pwp(S,QR)那么，wp(S,Q)wp(S,R)wp(S,QR)反之也可證明，wp(S,QR)wp(S,Q)wp(S,R)

第4頁，共38頁，2023年，2月20日，星期二最弱前置謂詞的幾個性質公理性質3:析取分配律wp(S,Q)wp(S,R)=wp(S,QR)證明：設任何一個狀態(tài)Pwp(S,Q)wp(S,R) 表示從P出發(fā)經(jīng)S執(zhí)行后必終止，終止時滿足Q；或者從P出發(fā)經(jīng)S執(zhí)行后必終止，終止時滿足R，也即滿足QR。所以，Pwp(S,QR)那么，wp(S,Q)wp(S,R)wp(S,QR)反之也可證明，wp(S,QR)wp(S,Q)wp(S,R)第5頁，共38頁，2023年，2月20日，星期二最弱前置謂詞的幾個性質公理性質4:單調律如果QR，則wp(S,Q)wp(S,R)假設任何一個狀態(tài)P表示從P

wp(S,R)出發(fā)，經(jīng)S執(zhí)行后必終止，終止時滿足R。又因為，QR，所以終止時也滿足Q。所以，Pwp(S,Q)，所以wp(S,Q)wp(S,R)第6頁，共38頁，2023年，2月20日，星期二求解最弱前置謂詞的規(guī)則1、skip、abort、復合語句wp(skip,R)=R(相當于空語句)wp(abort,R)=F(執(zhí)行過程中夭折的語句)wp(S1;S2,R)=wp(S1,wp(S2,R))（相當于順序復合語句）例如wp(skip;skip,R)=wp(skip,wp(skip,R))=R第7頁，共38頁，2023年，2月20日，星期二求解最弱前置謂詞的規(guī)則2、賦值語句(1)單個簡單變量的賦值語句(2)多個簡單變量的賦值語句(3)單個數(shù)組元素的賦值(4)多重賦值語句第8頁，共38頁，2023年，2月20日，星期二(1)單個簡單變量的賦值語句對單個簡單變量的賦值語句

S::=I:=E其語義為：

wp(“I:=E”,R)=domain(E)candRIEdomain(E)表示能獲得正常表達式E結果的條件。

當條件顯然時，可略去此項。RIE表示表達式E去替換R中所有自由出現(xiàn)的變量I。B1candB2表示從左到右的次序計算，B1為F時，則不必計算B2，其結果全為F。B1為T時，則其結果為B2的結果。B1無定義時，其結果也無定義。第9頁，共38頁，2023年，2月20日，星期二同步練習1.wp(“x:=x+1”,x<0)=(x+1<0)=(x<-1)2.wp(“x:=5”,x=5)=(5=5)=T3.wp(“x:=5”,x≠5)=(5≠5)=F4.wp(“x:=A÷B”,P(x))=(B≠0)candP(A÷B)5.wp(“x:=x*x”,x4=10)=((x*x)4=10)=(x8=10)6.設數(shù)組B的下標域為0:100，則:wp(“x:=B[I]”,x=B[I])=(0≤I≤100)candB[I]=B[I]=(0≤I≤100)7.wp(“t:=x;x:=y;y:=t”,x=X∧y=Y)=wp(“t:=x;x:=y”,wp(“y:=t”,x=X∧y=Y)=wp(“t:=x;x:=y”,x=X∧t=Y)=wp(“t:=x”,wp(“x:=y”,x=X∧t=Y)=wp(“t:=x”,y=X∧t=Y)=(y=X∧x=Y)第10頁，共38頁，2023年，2月20日，星期二(2)多個簡單變量的賦值語句多個簡單變量賦值語句為

S::=X:=E其中X為n(n>1)個互不相同的變量x1,x2,…,xnE為n個表達式e1,e2,…,en

其語義是：wp(“X:=E”,R)=domain(E)candRX

E

domainE=(i1≤i≤n:domain(ei))第11頁，共38頁，2023年，2月20日，星期二同步練習8.wp(“x,y:=x-y,y-x”,x+y=c)=(x-y+y-x=c)=(0=c)9.{T}a:=a+1;b:=x{a=b}wp(“a:=a+1;b:=x”,a=b)=wp(“a:=a+1”,a=x)=(a+1=x)10.wp(“a:=a+1;b:=x(a,b)”,a=b)=wp(“a:=a+1”,a=x(a,b))=(a+1=x(a+1,b))11.wp(“s,i:=s+b[i],i+1”,i>0∧s=(∑j:0≤j<i:b[j]))=(i+1>0∧s+b[i]=(∑j:0≤j<i+1:b[j]))=(i≥0∧s=(∑j:0≤j<i:b[j]))第12頁，共38頁，2023年，2月20日，星期二(3)單個數(shù)組元素的賦值語句對一個數(shù)組元素的賦值語句

S::=b[i]:=E其中b是數(shù)組名，i是b的下標表達式我們用（b;i:E）表示一個數(shù)組函數(shù)，定義為：(b;i:E)[j]=E當i=jb[j]當i≠j這樣，語句b[i]:=E等價于b:=(b;i:E)若略去domain(E)與domain(i)等因素，數(shù)組的賦值語句語義是wp(“b[i]:=E”,R)=Rb(b;i:E)其中Rb(b;i:E)表示用數(shù)組(b;i:E)去替換R中自由出現(xiàn)的數(shù)組名b。第13頁，共38頁，2023年，2月20日，星期二同步練習12.wp(“b[i]:=5”,b[i]=5)=(b[i]=5)b(b;i:5)=((b;i:5)[i]=5)=(5=5)=T13.wp(“b[i]:=5”,b[i]=b[j])=(b[i]=b[j])b(b;i:5)=((b;i:5)[i]=(b;i:5)[j])=((i≠j∧5=b[j])∨(i=j∧5=5))=((i≠j∧5=b[j])∨(i=j))=((i≠j∨i=j)∧(5=b[j]∨i=j))=(T∧(i=j∨b[j]=5))=(i=j∨b[j]=5)14.wp(“b[b[i]]:=i”,b[i]=i)=(b[i]:=i)b(b;b[i]:i)(定義)=(b;b[i]:i)[i]=i(替換)=(b[i]≠i∧b[i]=i)∨(b[i]=i∧i=i)=F∨(b[i]=i∧T)=(b[i]=i)第14頁，共38頁，2023年，2月20日，星期二求解最弱前置謂詞的規(guī)則3、條件語句條件語句是任何一種高級語言中不可缺少的語句之一，常用if表示。大家已熟知，它一般有二種格式，即：

ifx≥0thenZ:=xelseZ:=―xifx<0thenZ:=―x第15頁，共38頁，2023年，2月20日，星期二為說明方便，我們可改寫成

ifx≥0→Z:=x

□x<0→Z:=―xfi

與

ifx≥0→skip□x<0→Z:=―xfi其中“□”記號把兩個B→S的子句分開，而B是布爾表達式，S是語句。當B為真時，→S表示執(zhí)行S語句，所以稱B→S為條件子句。第16頁，共38頁，2023年，2月20日，星期二故我們有條件語句的一般表示形式：

S::=ifB1→S1□B2→S2...□Bn→Snfi其中，n≥1，Bi→Si是條件子語句，設BB=B1∨B2∨…∨Bn

，則在執(zhí)行if之前，如果BB為假，則if等價于abort語句；如果只有某個Bi為真，則執(zhí)行對應的Si語句；如果有m個條件同時為真，則選擇某一個Bi為真的條件子語句Bi→Si執(zhí)行Si

。if的執(zhí)行是不確定的，當有m個條件同時為真時，并沒有規(guī)定一定要選取哪一個條件子句執(zhí)行。第17頁，共38頁，2023年，2月20日，星期二例如，語句{x=6}ifx≥1→x:=x-1;□x≥2→x:=x-2;□x≥5→x:=x-5; ...

fi

就是不確定的

if語句的語義是

wp(“if”,R)=(i:1≤i≤n:Bi)∧(i:1≤i≤n:Biwp(“Si”,R))還可將語義記為

wp(“if”,R)=domain(BB)∧BB∧B1wp(“S1”,R)∧B2wp(“S2”,R)∧…∧Bnwp(“Sn”,R)第18頁，共38頁，2023年，2月20日，星期二同步練習15.

ifx≥0→Z:=x;□x＜0→Z:=―x;fiwp(“if”,Z=abs(x))=(x≥0∨x＜0)∧(x≥0wp(“Z:=x”,Z=abs(x)))∧(x＜0wp(“Z:=―x”,Z=abs(x)))=T∧(x≥0x=abs(x))∧(x＜0―x=abs(x))=T∧T∧T=T第19頁，共38頁，2023年，2月20日，星期二同步練習16.本例條件語句是一個循環(huán)體，是對數(shù)組b[0..m-1]中的正值進行計數(shù)。

ifb[i]＞0→P,i:=P+1,i+1□b[i]＜0→i:=i+1fiR:=i≤m∧P=(Nj:0≤j＜i:b[j]＞0) 其中，N是計數(shù)量詞，P:=(Nj:0≤j＜i:b[j]＞0)，指P等于在0≤j＜i域內b[0:i-1]中的正值的個數(shù)計數(shù)器。

wp(“if”,R)=(b[i]＞0∨b[i]＜0)∧(b[i]＞0wp(“P,i:=P+1,i+1”,R))∧(b[i]＜0wp(“i:=i+1”,R))=(b[i]≠0)∧(b[i]＞0i+1≤m∧P+1=(Nj:0≤j＜i+1;b[j]＞0))∧(b[i]＜0i+1≤m∧P=(Nj:0≤j＜i+1;b[j]＞0))=(b[i]≠0)∧((i＜m∧(P=(Nj:0≤j＜i:b[j]＞0)))∧((i＜m∧(P=(Nj:0≤j＜i:b[j]＞0)))=(b[i]≠0)∧(i＜m)∧(P=(Nj:0≤j＜i:b[j]＞0))第20頁，共38頁，2023年，2月20日，星期二定理1定理一對if語句，如果謂詞Q滿足

QBB(1)Q∧Bi

wp(“Si”,R)(2)

則Qwp(“if”,R)證明先看(2)式(iQ∧Bi

wp(“Si”,R))=(

i:﹁(Q∧Bi)∨wp(“Si”,R))=(

i:﹁Q∨﹁Bi∨wp(“Si”,R))=﹁Q∨(i:﹁Bi)∨wp(“Si”,R))=Q(i:Bi

wp(“Si”,R))因此(QBB)∧(

iQ∧Bi

wp(“Si”,R))=(QBB)∧(Q

(

i:Bi

wp(“Si”,R)))=(Q(BB∧(i:Biwp(“Si”,R)))=Qwp(“if”,R)第21頁，共38頁，2023年，2月20日，星期二例17

假設我們正在用二分搜索法從已排序的數(shù)組ordered(b[0..n-1])中搜索值x,已知目前階段謂詞Q為真(假定已查找區(qū)間縮小到i..j),即Q:ordered(b[0..n-1])∧0≤i＜k＜j＜n∧xb[i..j])要證明

Qwp(“if”,xb[i..j])

其中條件語句是{Q}ifb[k]≤x→i:=k□b[k]＞

x→j:=kfi{xb[i..j]}

要求證明的是

Qwp(“if”,R)證明因為b[k]≤x∨b[k]＞x恒為T,故QBB對(1)式成立。又因Q∧b[k]≤xxb[k..j]=wp(“i:=k”,xb[i..j])Q∧b[k]＞xxb[i..k]=wp(“j:=k”,xb[i..j])由此可知(2)式也成立。根據(jù)定理一,即可證明。證畢。第22頁，共38頁，2023年，2月20日，星期二求解最弱前置謂詞的規(guī)則4、循環(huán)語句循環(huán)語句是重要的控制語句(常用do表示)，也是高級語言中不可缺少的語句之一。顯然，它是重復的條件語句

loop:ifBthenbeginS;gotoloopend第23頁，共38頁，2023年，2月20日，星期二循環(huán)語句循環(huán)語句的一般表示形式為

S::=doB1→S1□B2→S2...□Bn→Snod其中n≥1，每個Bi→Si都是條件子語句。當BB為假時停止執(zhí)行；當BB為真時執(zhí)行對應的條件子語句。循環(huán)語句也可簡單地表示為

doB→Sod

循環(huán)語句又可記為

doBB→ifB1→S1□B2→S2...□Bn→Snfi od

或簡記為doBB→ifod循環(huán)語句也允許不確定性，即每次迭代，過程如有二個或二個以上條件為真，則任何一個相應的條件語句都可執(zhí)行。第24頁，共38頁，2023年，2月20日，星期二循環(huán)語句設H0(R)表示執(zhí)行do時只迭代0次便終止，且能使R成立的相應狀態(tài)集，顯然有

H0(R)=┐BB∧R又設Hk(R)表示執(zhí)行do時至多迭代k次(k≥0)便終止，且能使R成立的相應狀態(tài)集。至多迭代k次意味著有二種情況：一種是do迭代0次便終止，這時，顯然有：Hk(R)=H0(R);另一種是至少迭代一次，這次迭代過程等同于執(zhí)行一次if語句，而且執(zhí)行完if語句之后至多再迭代k-1次便終止。此時，相應狀態(tài)集是Hk-1(R)，而剛才執(zhí)行if語句之前相應狀態(tài)集顯然是wp(“if”,Hk-1(R))綜合兩種情況，我們得到Hk(R)=H0(R)∨wp(“if”,Hk-1(R))k>0第25頁，共38頁，2023年，2月20日，星期二循環(huán)語句從而可得到do語句的定義wp(“do”,R)=(k:k≥0:Hk(R))這樣定義是清楚的，但使用是不便的，因為計算Hk(R)很不容易。所以，我們常采用比wp(“do”,R)強的一些謂詞，即循環(huán)不變式，來設計與驗證我們的循環(huán)程序。循環(huán)不變式(簡稱不變式)P，就是在循環(huán)的每次迭代前后反映程序變量之間互相關系的謂詞P保持不變，即如果設謂詞P在進入循環(huán)前為真，而且每次迭代后P依然為真，到循環(huán)結束時P仍然為真，則P是循環(huán)不變式。第26頁，共38頁，2023年，2月20日，星期二同步練習…例18.下面程序段是在變量S中存放數(shù)組b[0..10]的諸元素之和。

i,S:=1,b[0]doi＜11→i,S:=i+1,S+b[i]od{R:S=(∑k:0≤k＜11:b[k])}現(xiàn)欲證明P（下面）是循環(huán)不變式。證明：設變量i,S,b之間互相關系的謂詞為

P:1≤i≤11∧S=(∑k:0≤k＜i:b[k])

開始執(zhí)行該程序段的狀態(tài)無論是什么,執(zhí)行i,S:=1,b[0]語句之后,P為真(初次進入循環(huán)之前),這是因為

wp(“i,S:=1,b[0]”,P)=1≤1≤11∧b[0]=(∑k:0≤k＜1:b[k])=T第27頁，共38頁，2023年，2月20日，星期二第二步再證明迭代一次后P仍然成立，即只要P和i＜11都成立，則執(zhí)行語句i,S:=i+1,S+b[i]后P仍然成立。

wp(“i,S:=i+1,S+b[i]”,P)=1≤i+1≤11∧S+b[i]=(∑k:0≤k＜i+1:b[k])=0≤i＜11∧S=(∑k:0≤k＜i:b[k])顯然，(P∧i＜11)蘊含了上述最后一行。這樣，我們就證明了P確實是循環(huán)不變式。程序段插入斷言可表示成：{T}i,S:=1,b[0]{P}doi＜11→{i＜11∧P}i,S:=i+1,S+b[i]{P}od{i≥11∧P}{R}第28頁，共38頁，2023年，2月20日，星期二定理2定理二設P∧BBwp(“if”,P)則P∧wp(“do”,T)wp(“do”,P∧﹁BB)假設P是循環(huán)不變式，則每次迭代開始和結束時P都成立。當然，在循環(huán)終止時P也成立，而終止條件是﹁BB，所以P∧﹁BB在循環(huán)終止時成立。定理二又稱為循環(huán)不變式定理。證明：根據(jù)do語句定義,我們有

H0(T)=﹁BB(1)Hk(T)=wp(“if”,Hk-1(T))∨﹁BB(k＞0)(2)

以及H0(P∧﹁BB)=P∧﹁BB(3)Hk(P∧﹁BB)=wp(“if”,Hk-1(P∧﹁BB))∨(P∧﹁BB)(k＞0)(4)第29頁，共38頁，2023年，2月20日，星期二我們首先用歸納法證明

P∧Hk(T)Hk(P∧﹁BB)(5)當k=0時，由(1)式和(3)式可知，(5)式顯然成立。當k＞0時，假設k=k-1時，命題成立，即P∧Hk-1(T)Hk-1(P∧﹁BB)則P∧Hk(T)=P∧(wp(“if”,Hk-1(T))∨﹁BB)(根據(jù)(2)式)

(P∧BB∧wp(“if”,Hk-1(T)))∨(P∧﹁BB)(因wp(“if”,R)BB)

(wp(“if”,P)∧wp(“if”,Hk-1(T)))∨(P∧﹁BB)(假設)=wp(“if”,P∧Hk-1(T))∨(P∧﹁BB)(wp的合取分配律)

wp(“if”,Hk-1(P∧﹁BB))∨(P∧﹁BB)(歸納假設)=Hk(P∧﹁BB)(根據(jù)(4)式)所以，對一切的k，(5)式成立。因此，有：

P∧wp(“do”,T)=(:k≥0:P∧Hk(T))(:k≥0:Hk(P∧﹁BB))=wp(“do”,P∧﹁BB)定理證畢。第30頁，共38頁，2023年，2月20日，星期二定理3對任一個循環(huán)，計算wp(“do”,T)是很困難的。為了證明該循環(huán)能夠終止，我們還需引入一個程序變量的整型函數(shù)t，表示尚需進行迭代次數(shù)的下界零，則循環(huán)一定能終止。這里的t就是界函數(shù)。下面，給出一個判定循環(huán)終止的定理。此定理的直觀意義也是很清楚的。一方面P∧t≥0必須保持為真；另一方面，循環(huán)體S的每次執(zhí)行至少使t減少1。無限的循環(huán)下去必將使t的值減小為負。但這是不允許的，所以循環(huán)必有終止。定理三

設P是do的不變式,t是一個整函數(shù),t0是任意常數(shù),如果

P∧BBt＞0;(1)P∧BB∧t≤t0+1wp(“if”,t≤t0)(2)則Pwp(“do”,T)第31頁，共38頁，2023年，2月20日，星期二定理3證明由(2)式,根據(jù)定理二,可得到

P∧BB∧t≤t0+1wp(“if”,P∧t≤t0)首先我們用歸納法證明

P∧t≤kHk(T)當k=0時,H0(T)=﹁BB,由條件(1)式可得Ｐ∧ＢＢ

t＞０=﹁P∨﹁BB∨t＞0=﹁P∨t＞0∨﹁BB=P∧t≤0﹁BB=P∧t≤0H0(T)當k＞0時，設k=k-1時命題成立，即

P∧t≤k-1Hk-1(T)則P∧BB∧t≤kwp(“if”,P∧t≤k-1)(根據(jù)(2))

wp(“if”,Hk-1(T))(歸納假設)而P∧﹁BB∧t≤k﹁BB=H0(T)所以P∧t≤k

wp(“if”,Hk-1(T))∨H0(T)因t≤t0+1,則必有（k:k≥0:t≤k）所以P=P∧(k:k≥0:t≤k)

=

k:k≥0:P∧t≤k(因k在Ｐ中不是自由變量)

k:k≥0Hk(T)=wp(“do”,T)即一切k≥０，命題都成立。定理證畢。

第32頁，共38頁，2023年，2月20日，星期二定理4合并定理二與定理三，有如下十分有用的定理：從定理四中，我們得到如下結果：假設（1）式意味著循環(huán)執(zhí)行結束時Ｐ仍成立，假設（2）式指出循環(huán)執(zhí)行結束前整函數(shù)t以０為下界，假設（3）式指出每次迭代至少使t減小１，因而循環(huán)一定能終止。如果循環(huán)不終止，t必小于任何界限，這與假設矛盾，因而﹁ＢＢ為真。應用這些概念和定理，我們就可方便地驗證程序的正確性。定理四設謂詞Ｐ滿足

P∧Bi

wp(“Si”,P),1≤i≤n

(1)

又設整函數(shù)t滿足

P∧BB(t＞0)(2)P∧Bi

wp(“t1:=t;Si”,t＜t1)，１≤i≤n(3)其中t１是一個新的標識符，則Ｐ

wp(“do”,P∧﹁BB)第33頁，共38頁，2023年，2月20日，星期二循環(huán)語句在討論循環(huán)語句時我們除了引入前置條件與后置謂詞外，循環(huán)不變式Ｐ與界函數(shù)t是必不可少的，我們將下面的形式稱為注解了的循環(huán)語句。{Q}{P}{t}doB1→S1□B2→S2