kmoaaa第6章-結(jié)構(gòu)化程序的正確性證明-資料下載頁
2025-07-23 15:52本頁面
【正文】 }可知 即 f(x0)=f(x)＝ y=f?g(x)=f(g(x)) 循環(huán)不變式產(chǎn)生的方法 同理可知如下定理： 2 假設(shè) f(x)=[do g(x) until p(x) ]， 則該循環(huán)不變式q(x)為 f(x)=(f(x)=f?g(x0)) 3假設(shè) f(x)=[do1 g(x) while p(x) do2 h(x) ],則該循環(huán)不變式 q(x)為 f(x)=f?h?g(x) 循環(huán)不變式產(chǎn)生的方法 — 例 1 對于循環(huán)程序 P： while v?0 do u,v=u+1,v1 其程序函數(shù)為 (u,v):= u+v,0， 求其循環(huán)不變式 對循環(huán)中所有變量，分別計算 f(x)和 f(x0)， 列表如下： 則循環(huán)不變式為 f(x)=f(x0) ? 循環(huán)不變式為 u+v=u0+v0 x f(x) f(x0) U u+v u0+v0 v 0 0 循環(huán)不變式產(chǎn)生的方法 — 例 2 求程序 P： while ab do a,q:=ab,q+1 的循環(huán)不變式 該程序的程序函數(shù)為 {(a,b,q),(a[a/b]*b),b,[a/b]+q} a[a/b]*b=a0(a0/b0)*b0 （ 1） b=b0 （ 2） (a/b)+q=(a0/b0)+q0 （ 3） 由 (1)、 (2)得： a0a=b*(a0/b0a/b) （ 4） 由 (3)得： a0/b0a/b=qq0 （ 5） 綜合 (4)、 (5)得 a0a=b*(qq0) x f(x) f(x0) a a[a/b]?b a0[a0/b0]*b0 B b B0 q (a/b)+q (a0/b0)+
教學(xué)教案相關(guān)推薦
鄂ICP備17016276號-1