程序的形式推導(dǎo)技術(shù)

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

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

wp(S,R)出發(fā)，經(jīng)S執(zhí)行后必終止，終止時(shí)滿足R。又因?yàn)?，QR，所以終止時(shí)也滿足Q。所以，Pwp(S,Q)，所以wp(S,Q)wp(S,R)第六頁(yè)，共三十八頁(yè)，2022年，8月28日求解最弱前置謂詞的規(guī)則1、skip、abort、復(fù)合語(yǔ)句wp(skip,R)=R(相當(dāng)于空語(yǔ)句)wp(abort,R)=F(執(zhí)行過(guò)程中夭折的語(yǔ)句)wp(S1;S2,R)=wp(S1,wp(S2,R))（相當(dāng)于順序復(fù)合語(yǔ)句）例如wp(skip;skip,R)=wp(skip,wp(skip,R))=R第七頁(yè)，共三十八頁(yè)，2022年，8月28日求解最弱前置謂詞的規(guī)則2、賦值語(yǔ)句(1)單個(gè)簡(jiǎn)單變量的賦值語(yǔ)句(2)多個(gè)簡(jiǎn)單變量的賦值語(yǔ)句(3)單個(gè)數(shù)組元素的賦值(4)多重賦值語(yǔ)句第八頁(yè)，共三十八頁(yè)，2022年，8月28日(1)單個(gè)簡(jiǎn)單變量的賦值語(yǔ)句對(duì)單個(gè)簡(jiǎn)單變量的賦值語(yǔ)句

S::=I:=E其語(yǔ)義為：

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

當(dāng)條件顯然時(shí)，可略去此項(xiàng)。RIE表示表達(dá)式E去替換R中所有自由出現(xiàn)的變量I。B1candB2表示從左到右的次序計(jì)算，B1為F時(shí)，則不必計(jì)算B2，其結(jié)果全為F。B1為T(mén)時(shí)，則其結(jié)果為B2的結(jié)果。B1無(wú)定義時(shí)，其結(jié)果也無(wú)定義。第九頁(yè)，共三十八頁(yè)，2022年，8月28日同步練習(xí)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è)數(shù)組B的下標(biāo)域?yàn)?: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)第十頁(yè)，共三十八頁(yè)，2022年，8月28日(2)多個(gè)簡(jiǎn)單變量的賦值語(yǔ)句多個(gè)簡(jiǎn)單變量賦值語(yǔ)句為

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

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

E

domainE=(i1≤i≤n:domain(ei))第十一頁(yè)，共三十八頁(yè)，2022年，8月28日同步練習(xí)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]))第十二頁(yè)，共三十八頁(yè)，2022年，8月28日(3)單個(gè)數(shù)組元素的賦值語(yǔ)句對(duì)一個(gè)數(shù)組元素的賦值語(yǔ)句

S::=b[i]:=E其中b是數(shù)組名，i是b的下標(biāo)表達(dá)式我們用（b;i:E）表示一個(gè)數(shù)組函數(shù)，定義為：(b;i:E)[j]=E當(dāng)i=jb[j]當(dāng)i≠j這樣，語(yǔ)句b[i]:=E等價(jià)于b:=(b;i:E)若略去domain(E)與domain(i)等因素，數(shù)組的賦值語(yǔ)句語(yǔ)義是wp(“b[i]:=E”,R)=Rb(b;i:E)其中Rb(b;i:E)表示用數(shù)組(b;i:E)去替換R中自由出現(xiàn)的數(shù)組名b。第十三頁(yè)，共三十八頁(yè)，2022年，8月28日同步練習(xí)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)第十四頁(yè)，共三十八頁(yè)，2022年，8月28日求解最弱前置謂詞的規(guī)則3、條件語(yǔ)句條件語(yǔ)句是任何一種高級(jí)語(yǔ)言中不可缺少的語(yǔ)句之一，常用if表示。大家已熟知，它一般有二種格式，即：

ifx≥0thenZ:=xelseZ:=―xifx<0thenZ:=―x第十五頁(yè)，共三十八頁(yè)，2022年，8月28日為說(shuō)明方便，我們可改寫(xiě)成

ifx≥0→Z:=x

□x<0→Z:=―xfi

與

ifx≥0→skip□x<0→Z:=―xfi其中“□”記號(hào)把兩個(gè)B→S的子句分開(kāi)，而B(niǎo)是布爾表達(dá)式，S是語(yǔ)句。當(dāng)B為真時(shí)，→S表示執(zhí)行S語(yǔ)句，所以稱(chēng)B→S為條件子句。第十六頁(yè)，共三十八頁(yè)，2022年，8月28日故我們有條件語(yǔ)句的一般表示形式：

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

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

。if的執(zhí)行是不確定的，當(dāng)有m個(gè)條件同時(shí)為真時(shí)，并沒(méi)有規(guī)定一定要選取哪一個(gè)條件子句執(zhí)行。第十七頁(yè)，共三十八頁(yè)，2022年，8月28日例如，語(yǔ)句{x=6}ifx≥1→x:=x-1;□x≥2→x:=x-2;□x≥5→x:=x-5; ...

fi

就是不確定的

if語(yǔ)句的語(yǔ)義是

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

wp(“if”,R)=domain(BB)∧BB∧B1wp(“S1”,R)∧B2wp(“S2”,R)∧…∧Bnwp(“Sn”,R)第十八頁(yè)，共三十八頁(yè)，2022年，8月28日同步練習(xí)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第十九頁(yè)，共三十八頁(yè)，2022年，8月28日同步練習(xí)16.本例條件語(yǔ)句是一個(gè)循環(huán)體，是對(duì)數(shù)組b[0..m-1]中的正值進(jìn)行計(jì)數(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是計(jì)數(shù)量詞，P:=(Nj:0≤j＜i:b[j]＞0)，指P等于在0≤j＜i域內(nèi)b[0:i-1]中的正值的個(gè)數(shù)計(jì)數(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))第二十頁(yè)，共三十八頁(yè)，2022年，8月28日定理1定理一對(duì)if語(yǔ)句，如果謂詞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)第二十一頁(yè)，共三十八頁(yè)，2022年，8月28日例17

假設(shè)我們正在用二分搜索法從已排序的數(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])

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

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

要求證明的是

Qwp(“if”,R)證明因?yàn)閎[k]≤x∨b[k]＞x恒為T(mén),故QBB對(duì)(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ù)定理一,即可證明。證畢。第二十二頁(yè)，共三十八頁(yè)，2022年，8月28日求解最弱前置謂詞的規(guī)則4、循環(huán)語(yǔ)句循環(huán)語(yǔ)句是重要的控制語(yǔ)句(常用do表示)，也是高級(jí)語(yǔ)言中不可缺少的語(yǔ)句之一。顯然，它是重復(fù)的條件語(yǔ)句

loop:ifBthenbeginS;gotoloopend第二十三頁(yè)，共三十八頁(yè)，2022年，8月28日循環(huán)語(yǔ)句循環(huán)語(yǔ)句的一般表示形式為

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

doB→Sod

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

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

或簡(jiǎn)記為doBB→ifod循環(huán)語(yǔ)句也允許不確定性，即每次迭代，過(guò)程如有二個(gè)或二個(gè)以上條件為真，則任何一個(gè)相應(yīng)的條件語(yǔ)句都可執(zhí)行。第二十四頁(yè)，共三十八頁(yè)，2022年，8月28日循環(huán)語(yǔ)句設(shè)H0(R)表示執(zhí)行do時(shí)只迭代0次便終止，且能使R成立的相應(yīng)狀態(tài)集，顯然有

H0(R)=┐BB∧R又設(shè)Hk(R)表示執(zhí)行do時(shí)至多迭代k次(k≥0)便終止，且能使R成立的相應(yīng)狀態(tài)集。至多迭代k次意味著有二種情況：一種是do迭代0次便終止，這時(shí)，顯然有：Hk(R)=H0(R);另一種是至少迭代一次，這次迭代過(guò)程等同于執(zhí)行一次if語(yǔ)句，而且執(zhí)行完if語(yǔ)句之后至多再迭代k-1次便終止。此時(shí)，相應(yīng)狀態(tài)集是Hk-1(R)，而剛才執(zhí)行if語(yǔ)句之前相應(yīng)狀態(tài)集顯然是wp(“if”,Hk-1(R))綜合兩種情況，我們得到Hk(R)=H0(R)∨wp(“if”,Hk-1(R))k>0第二十五頁(yè)，共三十八頁(yè)，2022年，8月28日循環(huán)語(yǔ)句從而可得到do語(yǔ)句的定義wp(“do”,R)=(k:k≥0:Hk(R))這樣定義是清楚的，但使用是不便的，因?yàn)橛?jì)算Hk(R)很不容易。所以，我們常采用比wp(“do”,R)強(qiáng)的一些謂詞，即循環(huán)不變式，來(lái)設(shè)計(jì)與驗(yàn)證我們的循環(huán)程序。循環(huán)不變式(簡(jiǎn)稱(chēng)不變式)P，就是在循環(huán)的每次迭代前后反映程序變量之間互相關(guān)系的謂詞P保持不變，即如果設(shè)謂詞P在進(jìn)入循環(huán)前為真，而且每次迭代后P依然為真，到循環(huán)結(jié)束時(shí)P仍然為真，則P是循環(huán)不變式。第二十六頁(yè)，共三十八頁(yè)，2022年，8月28日同步練習(xí)…例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)不變式。證明：設(shè)變量i,S,b之間互相關(guān)系的謂詞為

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

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

wp(“i,S:=1,b[0]”,P)=1≤1≤11∧b[0]=(∑k:0≤k＜1:b[k])=T第二十七頁(yè)，共三十八頁(yè)，2022年，8月28日第二步再證明迭代一次后P仍然成立，即只要P和i＜11都成立，則執(zhí)行語(yǔ)句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)蘊(yùn)含了上述最后一行。這樣，我們就證明了P確實(shí)是循環(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}第二十八頁(yè)，共三十八頁(yè)，2022年，8月28日定理2定理二設(shè)P∧BBwp(“if”,P)則P∧wp(“do”,T)wp(“do”,P∧﹁BB)假設(shè)P是循環(huán)不變式，則每次迭代開(kāi)始和結(jié)束時(shí)P都成立。當(dāng)然，在循環(huán)終止時(shí)P也成立，而終止條件是﹁BB，所以P∧﹁BB在循環(huán)終止時(shí)成立。定理二又稱(chēng)為循環(huán)不變式定理。證明：根據(jù)do語(yǔ)句定義,我們有

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)第二十九頁(yè)，共三十八頁(yè)，2022年，8月28日我們首先用歸納法證明

P∧Hk(T)Hk(P∧﹁BB)(5)當(dāng)k=0時(shí)，由(1)式和(3)式可知，(5)式顯然成立。當(dāng)k＞0時(shí)，假設(shè)k=k-1時(shí)，命題成立，即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)(假設(shè))=wp(“if”,P∧Hk-1(T))∨(P∧﹁BB)(wp的合取分配律)

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

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

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

P∧BBt＞0;(1)P∧BB∧t≤t0+1wp(“if”,t≤t0)(2)則Pwp(“do”,T)第三十一頁(yè)，共三十八頁(yè)，2022年，8月28日定理3證明由(2)式,根據(jù)定理二,可得到

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

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

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

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

wp(“if”,Hk-1(T))(歸納假設(shè))而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≥０，命題都成立。定理證畢。

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

P∧Bi

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

(1)

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

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

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

wp(“do”,P∧﹁BB)第三十三頁(yè)，共三十八頁(yè)，2022年，8月28日循環(huán)語(yǔ)句在討論循環(huán)語(yǔ)句時(shí)我們除了引入前置條件與后置謂詞外，循環(huán)不變式Ｐ與界函數(shù)t是必不可少的，我們將下面的形式稱(chēng)為注解了的循環(huán)語(yǔ)句。{Q}{P}{t}doB1→S1□B2→S2