【正文】 ) 2 從 Q中刪除 x (r+1) 2，得一個可能得不變式 ?： ?： 0≤ r2 ∧ r2 ≤ x 由 P， ? 得初始化語句： r:=0, 使得 {P} r:=0 {?}成立。 循環(huán)條件： ∵ ?c = （ x (r+1) 2 ） ∴ c =（ x ≥ (r+1) 2 ) 得程序： r:=0 do (r+1) 2 ≤ x ? ? od 界函數(shù) ?： sqrt（ x） r 循環(huán)體語句： r:=r+1。 削弱 Q就 ? 用變量替換常量 ? 策略： ? 用變量替換 Q中的有關常量，且給出此變量的適當變化范圍，以此削弱 Q而構造 ?。 削弱 Q就 ? 用變量替換常量 ? 例 1：平臺問題：對給定的有序 ( ≤)）數(shù)組 b[0:n1]，數(shù)組的平臺是一串相等值的序列，要求寫一個程序，存 b的最長平臺的長度于變量 L中。即此程序執(zhí)行后 Q成立： Q: L 是 b[0:n1]的最長平臺的長度 ? 解： ∵ b是有序的， ∴ 區(qū)間 b[j,k]是平穩(wěn)的 ? (b[j]=b[k]) ∴ Q: (?k:0 ≤knL: b[k]=b[k+L1]) ∧ ( ?i: 0 ≤inL1: b[i] ? b[i+L]) P: n0 ∧ ordered(b[0:n1]) ?: 1 ≤i ≤ n ∧ L 是 b[0:i1]的最長平臺的長度 界函數(shù) ? ： ni 削弱 Q就 ? 用變量替換常量 衛(wèi)哨： i ?n 循環(huán)初值： i,L :=1,1。 可使 {P} i,L :=1,1。 {?}成立 i:=i+1 可使 ? 遞減， 條件： b[i] ? b[iL] 反之， 當 b[i] = b[iL]時， L:=L+1。i:=i+1 得程序： i,L :=1,1。 do i ?n ? if b[i] ? b[iL] ? i:=i+1 。 b[i] = b[iL] ? L:=L+1。i:=i+1。 fi od 削弱 Q就 ? 用變量替換常量 ? 例 2：已知 n≥0, 求整數(shù)數(shù)組 b[0:n1]的和存于 S中。有： ? P: n≥0 ? Q: S = ∑j: 0≤jn : b[j] ? 以變量替換常量： ?： 0≤i ≤ n ∧ S =(∑j: 0≤ji : b[j]) ?: ni 削弱 Q就 ? 用變量替換常量 ? 例 3：寫一個程序，對給定的整數(shù) n≥0，求 a，使 R為真： R： a2 ≤n ≤(a+1)2 ? 設計不變式： 用 b替換（ a+1），并令 ab, b ≤n+1, ∴ ? : ab ∧ b ≤n+1 ∧ a2 ≤n ≤b2 ?: ba1 程序： a, b := 0,n+1。 do a+1 ? b ? d :=(a+b)/2。 if d*d = n ? a :=d。 d*dn ? b:=d。 fi od 削弱 Q就 ?擴大變量的取值范圍 ? 策略：擴大 Q中某些 變量的取值范圍 ，削弱 Q構造 ?。 ? 例：令 f[0:n],g[0:n],h[0:n]是三個固定的單調上升的整數(shù)數(shù)組（ n0）。已知他們存在公共值。寫一程序，求最小公共值在 f,g,h中的位置。 解： P: n0 令 i0,j0,k0滿足： f[i0]=g[j0]=h[k0] ∧ ?i?j?k: ii0 ∧ jj0 ∧ kk0 = f[i] ? g[j] ? h[k] i0,j0,k0即是最小公共值所處的位置，因此執(zhí)行后滿足： Q: i=i0 ∧ j=j0 ∧ k=k0 ?: 0 ≤ i ≤ i0 ∧ 0 ≤ j ≤ j0 ∧ 0 ≤ k ≤ k0 ?: i0i+j0j+k0k 削弱 Q就 ?擴大變量的取值范圍 ? 程序： ? 初始語句： i,j,k:=0,0,0。 ? do f[i]g[j] ∨ f[i]h[k] ? i := i+1。 ? g[j]h[k]∨ g[j]f[i] ? j := j+1。 ? h[k]f[i]∨ h[k]g[j] ?k := k+1。 ? od 削弱 Q就 ?擴大變量的取值范圍 ? 討論： ∵ BB = f[i]g[j] ∨ f[i]h[k] ∨ g[j]h[k]∨ g[j]f[i] ∨ h[k]f[i]∨ h[k]g[j] ∴ ? BB = （ f[i]=g[j]=h[k]） 而 ?（ f[i]g[j] ∨ g[j]h[k] ∨ h[k]f[i]） = （ f[i]=g[j]=h[k]） ∴ 只要每個條件的第一個分量也是正確的。 聯(lián)合 P和 Q構造 ? ? 若輸入變量的值在程序執(zhí)行過程中必須變化，則需要聯(lián)合 P和 Q而構造 ?。 ? 例：對給定的 m,n0，把數(shù)組 b[0:n1]每個元素的值變?yōu)?m*i+b[i],即： P： ?i: 0 ≤in : b[i] = u[i] Q: ?i: 0 ≤in : b[i] = u[i]+m*i ?: 0 ≤j ≤ n ∧ ?i: 0 ≤ij : b[i] = u[i]+m*i ∧ ?i: j ≤in : b[i] = u[i] 界函數(shù)（ Bound Function) ? 前言 ? 界函數(shù)主要用于表明循環(huán)的終止性。 ? 同時也可以用于估計執(zhí)行時間的上限（時間復雜度）。 ? 同一程序可以有不同的界函數(shù)，只要滿足前面關于循環(huán)語義的定理的要求即可。 界函數(shù) ? 一般地，通過分析循環(huán)不變式 ?，能夠較容易地找到界函數(shù) ?。 ? 多數(shù)情況下，循環(huán)迭代是依照一個或幾個變量的值的變化而進行的，此時，界函數(shù)可依照這些變量的變化范圍和變化規(guī)律而設定。 ? 例如：假定 i, j 是出現(xiàn)在循環(huán)中的變量。（ i,j）的值隨著迭代次數(shù)的增加依字典序遞減。 i , j的變化范圍分別為： i0 ≤ i ≤ i1 ， j0 ≤ j ≤ j1 則： ? = (i i0)*(j1 j0+1) +(j j0) 若（ i,j）的值隨著迭代次數(shù)的增加依字典序遞增，則 ? = (i1i)*(j1 j0+1) +(j1 j) 界函數(shù) ? 策略：先用語言描述不變式和問題的一個簡單的性質，然后將其形式化為數(shù)學表達式。 ? 對于任意可數(shù)的良序集，都可以找一個從該集到自然數(shù)集的一一對應的滿射。 ? 所以在程序中找到一個良序集，如字典序，就可以通過這種映射得到界函數(shù)。 偏序集 ? 設 A是一個集合，如果 A上的一個關系 R，滿足自反性、反對稱性和傳遞性，則稱 R是 A上的一個偏序關系。 ? 在實數(shù)集上， ≤就是一個偏序關系 ? 自反性： a ≤ a ? 反對稱性：若 a ≤b且 b ≤a，則必有 a=b ? 傳遞性：若 a ≤b且 b ≤c，則必有 a ≤ c 良序集 ? 任一偏序集合，假如它的每一個非空子集存在最小元素，這種偏序集稱為良序的。 ? 正實數(shù)集 R+ 對于 ≤關系來說是不是良序的？ ? 自然數(shù)集 N 對于 ≤關系來說是不是良序的？ 練習 1. 寫一程序尋找有序數(shù)組 b[0:n1]的平臺數(shù)， n0. 2. 寫一程序判斷數(shù)組 b[0:n1]是否全為 0。應用一個布爾變量 s，結果條件為：Q: s = ?i: 0 ≤in : b[i] = 0 3. 寫一程序逆轉數(shù)組 b[0:n1]。即假定開始時 b=(B0,B1,...,Bn1),那么終止時 b=(Bn1,Bn2,..., B1,B0) 4. 寫一個程序把整數(shù)轉換成二進制表示（不帶打頭零），二進制表示用一個數(shù)組表示。寫出規(guī)范，不變式，界函數(shù)