對(duì)程序進(jìn)行推理的邏輯計(jì)算機(jī)科學(xué)導(dǎo)論第二講教學(xué)課件

1、對(duì)程序進(jìn)行推理的邏輯計(jì)算機(jī)科學(xué)導(dǎo)論第二講計(jì)算機(jī)科學(xué)技術(shù)學(xué)院陳意yiyun/yiyun/課 程 內(nèi) 容課程內(nèi)容圍繞學(xué)科理論體系中的模型理論, 程序理論和計(jì)算理論1. 模型理論關(guān)心的問(wèn)題 給定模型M，哪些問(wèn)題可以由模型M解決；如何比較模型的表達(dá)能力2. 程序理論關(guān)心的問(wèn)題給定模型M，如何用模型M解決問(wèn)題包括程序設(shè)計(jì)范型、程序設(shè)計(jì)語(yǔ)言、程序設(shè)計(jì)、形式語(yǔ)義、類(lèi)型論、程序驗(yàn)證、程序分析等3. 計(jì)算理論關(guān)心的問(wèn)題給定模型M和一類(lèi)問(wèn)題, 解決該類(lèi)問(wèn)題需多少資源 本次講座討論怎樣用數(shù)學(xué)方法證明程序是正確的2講 座 提 綱基本知識(shí)程序驗(yàn)證、程序邏輯、命題邏輯、謂詞邏輯Hoare邏輯

2、Hoare三元式、賦值公理、結(jié)構(gòu)化語(yǔ)句的推理規(guī)則、推論規(guī)則生成驗(yàn)證條件的演算最弱前條件演算、生成驗(yàn)證條件的演算程序驗(yàn)證實(shí)例演示二分查找程序3序 曲近幾年軟件錯(cuò)誤帶來(lái)危害的事例2012年，美國(guó)KCP金融公司由于電子交易系統(tǒng)出現(xiàn)故障，交易算法出錯(cuò)，導(dǎo)致該公司對(duì)150支不同的股票高價(jià)購(gòu)進(jìn)、低價(jià)拋出，直接給公司帶來(lái)了4.4億美元的損失，當(dāng)天股票下跌62%2013年9月12日，美聯(lián)航售票網(wǎng)站一度出現(xiàn)問(wèn)題，售出票面價(jià)格為0-10美元的超低價(jià)機(jī)票，引發(fā)搶購(gòu)。大約15分鐘后，美聯(lián)航發(fā)現(xiàn)錯(cuò)誤，關(guān)閉售票網(wǎng)站并聲稱(chēng)正在進(jìn)行維護(hù)。大約兩個(gè)多小時(shí)后，該公司售票網(wǎng)站恢復(fù)正常，并且承認(rèn)已賣(mài)出的票有效4序 曲軟件錯(cuò)誤帶來(lái)危害

3、的事例據(jù)自然雜志網(wǎng)站報(bào)道，廣受世界天文學(xué)界期待的日本旗艦級(jí)天文衛(wèi)星“瞳”（Hitomi）于2016年2月17日發(fā)射升空，但在大約5周之后便出現(xiàn)翻滾失控跡象。經(jīng)調(diào)查后日本方面宣布，事故原因源自底層軟件錯(cuò)誤。衛(wèi)星的控制系統(tǒng)在發(fā)現(xiàn)飛行姿態(tài)失控時(shí)，采取了錯(cuò)誤的調(diào)整，推進(jìn)器點(diǎn)火時(shí)朝向了錯(cuò)誤的反方向，導(dǎo)致自身旋轉(zhuǎn)更加嚴(yán)重，最終徹底失控5序 曲軟件無(wú)處不在全世界有超過(guò)10億輛汽車(chē)在行駛，每輛新汽車(chē)上都有2080個(gè)微處理器，有多達(dá)3000萬(wàn)行的代碼在運(yùn)行全世界每年有多達(dá)23億次手術(shù)，在每個(gè)現(xiàn)代醫(yī)療設(shè)備上往往會(huì)有超過(guò)30萬(wàn)行的代碼在運(yùn)行全世界有超過(guò)3000輛高速列車(chē)在行駛，每輛列車(chē)上會(huì)有多達(dá)6000萬(wàn)行的代碼在

4、運(yùn)行全世界有超過(guò)300萬(wàn)架飛機(jī)，新型飛機(jī)上會(huì)有多達(dá)2000萬(wàn)行代碼在運(yùn)行如何保證這些代碼沒(méi)有錯(cuò)誤？6基 本 知 識(shí)程序：在數(shù)組a中快速查找某個(gè)值int amn:0.m2.an 0) 的各種情況都要測(cè)試嗎？對(duì)a中出現(xiàn)的各個(gè)元素都需要測(cè)試嗎？對(duì)a中不出現(xiàn)的元素要測(cè)多少種情況？1015212832374449535762677177837基 本 知 識(shí)程序測(cè)試與程序驗(yàn)證測(cè)試能發(fā)現(xiàn)程序有錯(cuò)；一般而言，測(cè)試不能保證程序無(wú)錯(cuò)程序驗(yàn)證：用數(shù)學(xué)的方法來(lái)證明程序的性質(zhì)，提高軟件可信程度演繹驗(yàn)證：指用邏輯推理的方法來(lái)證明程序具備所期望的性質(zhì)就所期望的性質(zhì)而言，演繹驗(yàn)證可保證程序無(wú)錯(cuò)程序邏輯：對(duì)程序進(jìn)行推理的邏輯8

5、基 本 知 識(shí)命題邏輯程序設(shè)計(jì)中用到命題邏輯的知識(shí)if (0 = m & m 100) 0 = m和m 100都是命題邏輯的原子命題 &是命題邏輯的二元運(yùn)算符(下面用而非&)if (0 m | 0 = 100) ; n = n + 1; !是命題邏輯的一元運(yùn)算符（下面用而不是 !）9基 本 知 識(shí)命題邏輯合式公式（well-formed formula）的歸納定義 := p | | | | | ( )(1) p代表原子命題，例如 x 3, a5 = 10.5 原子命題具體形式與討論的問(wèn)題領(lǐng)域有關(guān)(2) 代表一般命題，“:=”右部用“| ”分隔的各部分代表命題的構(gòu)成形式，如 0= x x 100

6、(3) , , 和代表合取、析取、非和蘊(yùn)涵運(yùn)算，在確定了它們的運(yùn)算優(yōu)先關(guān)系后，很多情況下括號(hào)可以省略，如p (q1 q2)可簡(jiǎn)化為p q1 q2備注：蘊(yùn)涵采用而不是 ， 用于描述函數(shù)類(lèi)型 10基 本 知 識(shí)命題邏輯推理規(guī)則例：有關(guān)合取“”運(yùn)算的推理規(guī)則( i)(e1) (e2)“ i”表示合取引入規(guī)則（i: introduction）“ e”表示合取消去規(guī)則（e: elimination）對(duì)和等也都有各自的推理規(guī)則 11謂詞邏輯程序設(shè)計(jì)中用到謂詞邏輯的知識(shí)謂詞：結(jié)果類(lèi)型為bool的函數(shù)bool even(int m) /用編程語(yǔ)言寫(xiě)的謂詞，與數(shù)理 if (m/2 * 2 = m) return

7、 true; /邏輯中的有區(qū)別 else return false; if(even(x) & even(y) 、=、=、!= 等關(guān)系算符都是謂詞基 本 知 識(shí)12謂詞邏輯合式公式(1) 謂詞集合、函數(shù)集合（包括常量）(2) 基于來(lái)定義項(xiàng)集 t := x | c | f(t, , t) ( f ) 例如 a + 5 b 3中的a + 5和b 3(3) 歸納地定義基于（ , ）的合式公式 := P(t1, t2, , tn) | | | | | x | x | ( ) ( P )增加的規(guī)則全稱(chēng)量詞斷言和存在量詞斷言的證明規(guī)則等基 本 知 識(shí)13Hoare 邏 輯程序邏輯對(duì)程序進(jìn)行推理的邏輯Hoa

8、re邏輯是一種程序邏輯介紹面向非常簡(jiǎn)單的編程語(yǔ)言（只有賦值語(yǔ)句、順序語(yǔ)句、條件語(yǔ)句和循環(huán)語(yǔ)句）的Hoare邏輯推理規(guī)則14Hoare 邏 輯合式公式（well-formed formula）語(yǔ)法形式：P S Q，稱(chēng)為Hoare三元式(1) S是代碼段，遵循相應(yīng)編程語(yǔ)言的語(yǔ)法(2) P和Q是關(guān)于程序狀態(tài)（變量到值的映射）的斷言，分別稱(chēng)為S的前斷言和后斷言，斷言是謂詞邏輯的合式公式(3) 例： x = 1 y 5 x = x +1 x = 2 y 5P S Q的含義：在滿(mǎn)足P的狀態(tài)下執(zhí)行S ，若執(zhí)行終止，則終止?fàn)顟B(tài)滿(mǎn)足Q例：x = 1 y 5 x = x +1 x = 2 y 1 y 0 y 6

9、x = x +1 x 6 是賦值公理的實(shí)例特點(diǎn)： x +1 6 （即x 5）是語(yǔ)句x = x+1和后斷言x 6 的最弱前斷言(1) x 5.1和x 7都可作為前斷言，因都強(qiáng)于x 5x 5.1 x 5 并且x 7 x 5(2) 若x 4.9作為前斷言，則三元式不成立，因?yàn)閤 4.9 x 5不成立16Hoare 邏 輯結(jié)構(gòu)化語(yǔ)句的推理規(guī)則順序語(yǔ)句條件語(yǔ)句（也可用其它形式表示）插曲：推論規(guī)則P P P S Q Q Q P S QP E S1 Q P E S2 QP if E then S1 else S2 QP S1 R R S2 QP S1; S2 Q17Hoare 邏 輯例（用Hoare邏輯手工

10、證明簡(jiǎn)單程序段）證: true if (x y) z = x; else z = y; z = x z = y(1)由賦值公理:x = x x =yz = xz = x z =y(2) 由(1)的所得、(true x y) (x = x x = y)和推論規(guī)則，可得： true x y z = x z = x z = y(3) 同理得: true (x y) z = y z = x z = y(4) 得: true if (x y) z = x; else z = y;z = x z = yP E S1 Q P E S2 QP if E then S1 else S2 Q 由條件語(yǔ)句的規(guī)則18

11、Hoare 邏 輯結(jié)構(gòu)化語(yǔ)句的推理規(guī)則（續(xù)）循環(huán)語(yǔ)句例：用自然數(shù)加法來(lái)完成自然數(shù)m和n相乘x = 0; y = 0;while (y n) x = x + m; y = y + 1; / x = m n 演算得到語(yǔ)句S和后斷言I的最弱前條件：x+m = m(y+1) y+1 nIE S II while E do S IEI 被稱(chēng)為 循環(huán)不變式/循環(huán)不變式I：(x = my) (y n)19Hoare 邏 輯結(jié)構(gòu)化語(yǔ)句的推理規(guī)則（續(xù)）循環(huán)語(yǔ)句例：用自然數(shù)加法來(lái)完成自然數(shù)m和n相乘x = 0; y = 0;while (y n) x = x + m; y = y + 1; / x = m n 演

12、算得到語(yǔ)句S和后斷言I的最弱前條件：x+m = m(y+1) y+1 nIE S II while E do S IEI 被稱(chēng)為 循環(huán)不變式/循環(huán)不變式I：(x = my) (y n)分兩步看，對(duì)于y = y + 120Hoare 邏 輯結(jié)構(gòu)化語(yǔ)句的推理規(guī)則（續(xù)）循環(huán)語(yǔ)句例：用自然數(shù)加法來(lái)完成自然數(shù)m和n相乘x = 0; y = 0;while (y n) x = x + m; y = y + 1; / x = m n 演算得到語(yǔ)句S和后斷言I的最弱前條件：x+m = m(y+1) y+1 nIE S II while E do S IEI 被稱(chēng)為 循環(huán)不變式/循環(huán)不變式I：(x = my)

13、(y n)分兩步看，對(duì)于x = x + m21Hoare 邏 輯結(jié)構(gòu)化語(yǔ)句的推理規(guī)則（續(xù)）循環(huán)語(yǔ)句例：用自然數(shù)加法來(lái)完成自然數(shù)m和n相乘x = 0; y = 0;while (y n) x = x + m; y = y + 1; / x = m n 證明I E 語(yǔ)句S和后斷言I的最弱前條件：IE S II while E do S IEI 被稱(chēng)為 循環(huán)不變式/循環(huán)不變式I：(x = my) (y n)(x = my y n y n) (x+m = m(y+1) y+1 n)最后一行稱(chēng)為驗(yàn)證條件22Hoare 邏 輯小結(jié)用Hoare邏輯，可對(duì)簡(jiǎn)單程序進(jìn)行手工推理證明手工體現(xiàn)在兩方面(1) 手工用

14、推理規(guī)則進(jìn)行演算或推理(2) 手工進(jìn)行驗(yàn)證條件的證明（前例遇到蘊(yùn)涵式的證明，第一講對(duì)自動(dòng)定理證明已略有介紹）雖是證明程序的一種方法，但低效、不能接受如何走向自動(dòng)驗(yàn)證（以函數(shù)的正確性驗(yàn)證為例）(1) 函數(shù)的前條件和后條件必須由驗(yàn)證者給出(2) 把Hoare邏輯規(guī)則改成能自動(dòng)推演的演算規(guī)則(3) 借助自動(dòng)定理證明器證明驗(yàn)證條件23生成驗(yàn)證條件的演算最弱前條件（Weakest Precondition）演算WP函數(shù)WP : 程序集 斷言集 斷言集 WP(S, Q)：計(jì)算P S Q的最弱前條件PHoare邏輯的賦值公理直接是最弱前條件演算的一條規(guī)則(1) 賦值公理：QE/x x = E Q(2) 賦值

15、語(yǔ)句的WP演算規(guī)則： WP (x =E, Q) = QE/x24生成驗(yàn)證條件的演算最弱前條件演算WP若一個(gè)函數(shù)的前后條件是P和Q，函數(shù)的代碼是賦值語(yǔ)句序列S1, , Sn，那么(1) 逆向從Sn到S1連續(xù)使用賦值語(yǔ)句的WP規(guī)則，WP(S1, , WP(Sn, Q)它是保證執(zhí)行上述代碼段后得到Q的最弱前條件(2) 若P WP(S1, , WP(Sn, Q)得證，則代碼段S1, , Sn對(duì)前后條件P和Q正確(3) P WP(S1, , WP(Sn, Q)稱(chēng)為驗(yàn)證條件強(qiáng)調(diào)：P蘊(yùn)涵最弱前條件即可, 不必要求等于后者25生成驗(yàn)證條件的演算最弱前條件演算WPWP(x =E, Q) = QE/xQE/x x

16、 = E QWP(S1;S2, Q) = WP (S1, WP(S2, Q)WP(if E then S1 else S2, Q) =(WP(S1, Q) E) (WP(S2, Q) E)P S1 R R S2 QP S1; S2 QP E S1 Q P E S2 QP if E then S1 else S2 Q26生成驗(yàn)證條件的演算最弱前條件演算WP對(duì)于WP (while E do S, Q)，演算有可能不終止 假定WPk為循環(huán)體S執(zhí)行k次的演算 WP0(while E do S, Q) = E Q WPi (while E do S, Q) = E WP(S, WPi1(while E

17、do S, Q) WP(while E do S, Q) = WP0 () WP1 () WP2 () IE S II while E do S IE WP演算在循環(huán)語(yǔ)句這里遇到了困難27生成驗(yàn)證條件的演算最弱前條件演算WP一些其他規(guī)則(1) WP(S, Q1 Q2) = WP(S, Q1) WP(S, Q2) (2) WP(S, Q1 Q2) = WP(S, Q1) WP(S, Q2)(3)(4) WP(S, false) = false(4)和(5)較難理解, 不介紹(5) WP(S, true) = 保證S終止的最弱前條件 . 下面考慮解決由循環(huán)語(yǔ)句引出的問(wèn)題Q QWP(S, Q) WP

18、(S, Q) 28生成驗(yàn)證條件的演算生成驗(yàn)證條件的演算VC(verification condition) (1) 觀察P和WP之間的關(guān)系(2) 尋找兩者之間的一種稱(chēng)為VC(S, Q)的演算(3) 即P VC(S, Q)WP(S, Q)(4) VC演算的特點(diǎn)：要求驗(yàn)證者提供循環(huán)不變式falsetruestrongweak Precondition(S, Q)最弱前條件 WP(S, Q)驗(yàn)證者提供的前條件P驗(yàn)證條件演算結(jié)果VC(S, Q)29生成驗(yàn)證條件的演算生成驗(yàn)證條件的演算VC(verification condition)除了循環(huán)語(yǔ)句外，VC演算與WP的一致循環(huán)語(yǔ)句的VC演算如下，其中I是

19、循環(huán)不變式VC(while E do S, Q) = I x1xn( I E VC(S, I) (I E Q)其中x1, , xn是在S中被修改的所有變量實(shí)際做法(1) 黃色部分和綠色部分 分別作為循環(huán)出口和入口的驗(yàn)證條件(2) I作為繼續(xù)逆向VC演算的后斷言IE S II while E do S IE30程 序 驗(yàn) 證 實(shí) 例void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do x = x + m ;y = y + 1 ; 例子：用加運(yùn)算來(lái)實(shí)現(xiàn)乘運(yùn)算的函數(shù)31程 序 驗(yàn) 證 實(shí) 例n 0/ 前條件void mult(int m, int

20、 n) x = 0 ; y = 0 ;while (y n) do x = x + m ;y = y + 1 ; x = m n / 后條件由程序員提供由程序員提供32程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = my) (y n) / 循環(huán)不變式x = x + m ;y = y + 1 ; x = m n也由程序員提供33程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = my) (y n) / 循環(huán)

21、不變式x = x + m ;y = y + 1 ; x = m n函數(shù)前后條件、循環(huán)不變式都稱(chēng)為斷言它們看上去像編程語(yǔ)言的布爾表達(dá)式34程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = my) (y n) x = x + m ;y = y + 1 ; (x = my) (y n) (y n) / 循環(huán)結(jié)束程序點(diǎn)的斷言 x = m n I E 35程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = my) (

22、y n) x = x + m ;y = y + 1 ; (x = my) (y n) (y n) (x = mn) x = m nI E Q（Q是函數(shù)后條件）第1個(gè)驗(yàn)證條件36程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = my) (y n) x = x + m ;(x = m(y+1) (y+1) n)y = y + 1 ; (x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n 通過(guò)最弱前條件演算得到37程 序 驗(yàn) 證 實(shí) 例n 0void m

23、ult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x = x + m ;(x = m(y+1) (y+1) n) y = y + 1 ;(x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n38程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) x = 0 ; y = 0 ; I E VC(S, I)（S是循環(huán)體） (x =my) (y n) (y n) (x+m =m(y+1) (y+1) n)wh

24、ile (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x = x + m ;(x = m(y+1) (y+1) n) y = y + 1 ;(x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n第2個(gè)驗(yàn)證條件39程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) x = 0 ;(x = m0) (0 n) y = 0 ;(x =my) (y n) (y n) (x+m =m(y+1) (y+1) n)while (y n) do (x = my) (y n) (x+m =

25、m(y+1) (y+1) n) x = x + m ;(x = m(y+1) (y+1) n) y = y + 1 ;(x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n40程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) (0 = m0) (0 n) x = 0 ;(x = m0) (0 n) y = 0 ;(x =my) (y n) (y n) (x+m =m(y+1) (y+1) n)while (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x = x + m ;

26、(x = m(y+1) (y+1) n) y = y + 1 ;(x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n41程 序 驗(yàn) 證 實(shí) 例n 0 P VC(S, I) void mult(int m, int n) ( n 0 ) (0 = m0) (0 n)(0 = m0) (0 n) x = 0 ;(x = m0) (0 n) y = 0 ;(x =my) (y n) (y n) (x+m =m(y+1) (y+1) n)while (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x =

27、x + m ;(x = m(y+1) (y+1) n) y = y + 1 ;(x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n第3個(gè)驗(yàn)證條件P是函數(shù)前條件，S是循環(huán)之前的語(yǔ)句序列42程 序 驗(yàn) 證 實(shí) 例n 0void mult(int m, int n) ( n 0 ) (0 = m0) (0 n)x = 0 ;y = 0 ;(x =my) (y n) (y n) (x+m =m(y+1) (y+1) n)while (y n) do (x = my) (y n) x = x + m ;y = y + 1 ; (x = my) (y n

28、) (y n) (x = mn) x = m n 由自動(dòng)定理證明器完成驗(yàn)證條件的證明43程 序 驗(yàn) 證 實(shí) 例程序：二分查找#define m 15int amn:0.m2.an an+1用二分法在數(shù)組a15中快速查找3810152128323744495357626771778344程 序 驗(yàn) 證 實(shí) 例程序：二分查找val = 38, i = 0, j = 14, k = 7i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到 else 沒(méi)有找到1015212832374449535

29、76267717783ijk觀察點(diǎn)45程 序 驗(yàn) 證 實(shí) 例程序：二分查找val = 38, i = 0, j = 6, k = 3i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到 else 沒(méi)有找到101521283237444953576267717783ijk觀察點(diǎn)46程 序 驗(yàn) 證 實(shí) 例程序：二分查找val = 38, i = 4, j = 6, k = 5i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i

30、= k + 1;if (i 1 j) 找到 else 沒(méi)有找到101521283237444953576267717783ijk觀察點(diǎn)循環(huán)不變性： a0到ai-1都小于38 aj+1到a14都大于3847程 序 驗(yàn) 證 實(shí) 例程序：二分查找val = 38, i = 6, j = 6, k = 6i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到 else 沒(méi)有找到101521283237444953576267717783ijk觀察點(diǎn)循環(huán)不變性： a0到ai-1都小于38 aj+1到

31、a14都大于3848程 序 驗(yàn) 證 實(shí) 例程序：二分查找val = 38, i = 6, j = 5, k = 6i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到 else 沒(méi)有找到101521283237444953576267717783ijk條件不成立49程 序 驗(yàn) 證 實(shí) 例程序：二分查找val = 37, i = 4, j = 6, k = 5 （若val改成37）i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak

32、) i = k + 1;if (i 1 j) 找到 else 沒(méi)有找到101521283237444953576267717783ijk觀察點(diǎn)循環(huán)不變性： a0到ai-1都小于38 aj+1到a14都大于3850程 序 驗(yàn) 證 實(shí) 例程序：二分查找val = 37, i = 6, j = 4, k = 5 （若val改成37）i = 0; j = 14;while(i = j) k = i + (j i)/2; if(val = ak) i = k + 1;if (i 1 j) 找到 else 沒(méi)有找到101521283237444953576267717783jik條件不成立51程 序 驗(yàn) 證 實(shí) 例程序：二分查找的主要程序段和斷言int i, j, k, val, am; /此前有#define m 15m = 15 (n:0.m2.an an+1) i = 0 j = m1while(i = j) m=15 (n:0.m2.an an+1) 0 i m 1 j m1 (ji 1(n:j+1.m1. val an) ji = 2 k = i1 val = ak ) /循環(huán)不變式, 含黃色部分 k = i + (j i)/2; if(val = ak) i = k + 1;m = 15 (n:0.m2.an an+1) (ij