命令式程序的語義.pptVIP

第5章 命令式程序的語義,函數(shù)式程序 不含賦值或其它形式的改變變量值的操作 命令式程序 賦值語句是典型的構(gòu)造 本章圍繞一個(gè)叫做Kernel的簡(jiǎn)單的命令式語言來討論語義,5.1 引 言,Kernel語言的結(jié)構(gòu)由下面的文法概括 P := x:= M | P ; P | if B then P else P | while B do P od x和M都有適當(dāng)?shù)念愋蛌al B的類型是bool 沒有顯式的輸入、輸出，也沒有局部變量聲明 例 求對(duì)數(shù) x := 1; y := 0; while x z do x := x + x; y := y + 1 od,5.1 引 言,本章主要內(nèi)容 圍繞Kernel來討論命令式語言的語義 基于一組重寫規(guī)則的結(jié)構(gòu)化操作語義 使用類型化演算和論域（CPO）來表示的指稱語義 把Kernel程序翻譯成類型化演算的表達(dá)式 利用類型化演算的指稱語義 基于Floyd-Hoare邏輯的公理語義,5.2 Kernel語言,5.2.1 存儲(chǔ)單元 Kernel的變量可賦值 與函數(shù)式語言let子句引入的變量有很大區(qū)別 可賦值變量指稱存儲(chǔ)單元 變量的左值和右值 左值是變量的存儲(chǔ)單元的地址 右值是該存儲(chǔ)單元存放的內(nèi)容 為方便討論，修改語言 顯式區(qū)分左值和右值，例x和cont x,5.2 Kernel語言,例1 求對(duì)數(shù) x := 1; y :=0; while cont x z do x := cont x + cont x; y := cont y + 1 od 例2：計(jì)算m除以n的商q和余數(shù)r q := 0; r := m; while cont r n do q := cont q +1; r := cont r n; od,5.2 Kernel語言,5.2.2 表達(dá)式的解釋 在文法中，M和B分別代表val和bool表達(dá)式 P := x := M | P ; P | if B then P else P | while B do P od 不深入表達(dá)式的內(nèi)部細(xì)節(jié) 為方便起見，把val看作nat 允許普通的數(shù)值和布爾運(yùn)算,5.2 Kernel語言,用4類別代數(shù)A來建立Kernel的抽象機(jī)器模型 作為介紹操作語義和指稱語義的共同基礎(chǔ) 便于比較操作語義和指稱語義 本小節(jié)先介紹相應(yīng)代數(shù)規(guī)范的三個(gè)類別 基調(diào)包含3類別val、bool和loc 僅關(guān)心loc類別有一個(gè)取存儲(chǔ)單元內(nèi)容的函數(shù)符號(hào) cont : loc val 環(huán)境把變量從 loc val bool映射到A的元素 loc：程序中的變量； val和bool ：程序中的常量 Abool的解釋是布爾值集合true, false,5.2 Kernel語言,5.2.3 程序狀態(tài) 操作語義和指稱語義都涉及“狀態(tài)”數(shù)據(jù)結(jié)構(gòu),5.2 Kernel語言,基調(diào)的第4個(gè)類別state init : state update : state loc val state lookup : state loc val 代數(shù)公理 lookup (update s l v) l = (lookup) if Eq? l l then v else (lookup s l) update s l (lookup s l) = s (update)1 update (update s l u) l v = if Eq? l l (update)2 then update s l v else update (update s l v) l u,5.2 Kernel語言,四類別代數(shù)A Aloc是任意的可數(shù)集合，Astate是從Aloc到Aval的所有函數(shù)的集合 initA是任意的常函數(shù) lookupA(s, l) = s(l) updateA(s, l, v)是函數(shù)s，除了s(l) = v以外，s等同于s 為了記號(hào)上的方便，下面用init，lookup和update代替initA，lookupA和updateA,5.2 Kernel語言,兩個(gè)問題 為什么不在前三個(gè)類別的基礎(chǔ)上引入作為狀態(tài)的函數(shù)state = loc val，而要引入第4個(gè)類別state 若那樣，則lookup和update成了高階的函數(shù)符號(hào) 為什么不用一個(gè)函數(shù)直接從變量映射到值，而要分離出環(huán)境和狀態(tài) 直觀上講，環(huán)境和狀態(tài)在概念上有區(qū)別，它們分別對(duì)應(yīng)到實(shí)際語言實(shí)現(xiàn)的不同機(jī)制 從技術(shù)角度說，Kernel沒有提供聲明常量的值的方式，只能將程序中常量的取值交給環(huán)境來確定,5.3 操作語義,5.3.1 表達(dá)式的求值 操作語義分成兩部分 表達(dá)式的計(jì)算 語句的執(zhí)行 表達(dá)式的語義 表達(dá)式、環(huán)境、狀態(tài)和表達(dá)式的語義值之間的一個(gè)四元關(guān)系：M, s eval v 環(huán)境下標(biāo)在下面將省略 eval由一個(gè)證明系統(tǒng)來給出,5.3 操作語義,eval公理 x, s eval (x) c, s eval cA eval推理規(guī)則 fA(v1, vk)=v lookupA(s, l)=v,5.3 操作語義,5.3.2 命令的執(zhí)行 命令的執(zhí)行可以用關(guān)系exec來刻畫 updateA(s, (x), v)=s,5.3 操作語義,5.3 操作語義,如果想證明P, s exec s,需要觀察P的語法形式,考察哪條規(guī)則是完成該證明的最后一條規(guī)則 例 p := 0; m := 0; while (cont m) n do p := cont m; m := (cont m) +1; od,5.3 操作語義,p := 0; s1 = updateA s lp 0 m := 0; while (cont m) n do p := cont m; m := (cont m) +1; od,5.3 操作語義,p := 0; s1 = updateA s lp 0 m := 0; s2 = updateA s1 lm 0 while (cont m) n do p := cont m; m := (cont m) +1; od,5.3 操作語義,p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) n do p := cont m; m := (cont m) +1; od,5.3 操作語義,p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) n do (cont m) n, s2 eval true p := cont m; m := (cont m) +1; od,5.3 操作語義,p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) n do p := cont m; m := (cont m) +1; (p := cont m; m := (cont m) +1), s2 exec s3 od,5.3 操作語義,p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) n do p := cont m; m := (cont m) +1; lookupA s3 lp = 0 & lookupA s3 lm = 1 od,5.3 操作語義,p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) n do (cont m) n, s3 eval true p := cont m; m := (cont m) +1; lookupA s3 lp = 0 & lookupA s3 lm = 1 od,5.3 操作語義,p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) n do p := cont m; m := (cont m) +1; lookupA s3 lp = 0 m := (cont m) +1), s3 exec s4 od,5.3 操作語義,p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) n do p := cont m; m := (cont m) +1; lookupA s4 lp = 1 m := (cont m) +1), s3 exec s4 od,5.4 指稱語義,5.4.1帶狀態(tài)的類型化演算 前兩章已經(jīng)給出了類型化演算的指稱語義 只要給出從Kernel語言到類型化演算的翻譯即可 把Kernel程序翻譯成類型化演算state, fix, 該演算有類型常量val, bool, loc, state和state state, fix, 演算還增加的運(yùn)算 Eq? : loc loc bool 在state上的運(yùn)算init, update和lookup,5.4 指稱語義,每個(gè)類型都有條件運(yùn)算ifthenelse 還有提升運(yùn)算（在下面描述），抽象，應(yīng)用和不動(dòng)點(diǎn)算子 fixstate : (state state) (state state) (state state) state, fix, 的CPO模型A是四類別代數(shù)A的一個(gè)拓展 val, bool, loc和state的解釋同A的解釋一樣 state被解釋成提升集合Astate = (Astate) 這種解釋延伸到函數(shù)類型,Astate state 有最小元，該類型有最小不動(dòng)點(diǎn)算子,5.4 指稱語義,提升運(yùn)算 :state state 如果M:state,讓M和M有同樣的指稱但不同的類型 中綴算符 (state Elim) M = : state M N = MN : state 函數(shù)合成的嚴(yán)格形式美化成 M N s : state. M (N s),5.4 指稱語義,5.4.2 語義函數(shù) 指稱語義由兩部分組成 表達(dá)式和命令到state, fix, 項(xiàng)的語法翻譯 這個(gè)演算在模型A中的標(biāo)準(zhǔn)解釋 語法翻譯部分 函數(shù)V: 把布爾表達(dá)式和值表達(dá)式分別翻譯成類型為state bool和state val的項(xiàng) 函數(shù)C: 把命令翻譯成類型為state state的項(xiàng),5.4 指稱語義,語義函數(shù) 把這些語法翻譯和從state, fix, 的項(xiàng)到模型A的標(biāo)準(zhǔn)含義函數(shù)組合起來 : expressions environments Astate Avalues : commands environments Astate Astate,5.4 指稱語義,表達(dá)式的語法翻譯 Vx= s: state. x Vcont x= s: state. lookup s x V f M1 Mk = s: state. f VM1s VMks 表達(dá)式M在環(huán)境中的含義 M = AVM M s = ( M)s,5.4 指稱語義,命令的語法翻譯 Cx := M = s: state. update s x (VMs) CP1; P2 = CP2 CP1 Cif B then P1 else P2 = s: state. if VBs then CP1s else CP2s Cwhile B do P od = fix(f : state state. s: state. if VBs then (f CP)s else s) 程序P在環(huán)境下的含義 P = ACP P s = ( P) s,5.4 指稱語義,例 一個(gè)簡(jiǎn)單的程序skip x := cont x Cskip = s: state.update s x (Vcont xs) = s: state.update s x (lookup s x) = s: state. s skip s = (ACskip)(s) = (As: state. s)(s) = s,5.4 指稱語義,指稱語義可用來證明簡(jiǎn)單程序之間的等價(jià) 證明 while B do P od = if B then (P; while B do P od) else skip Cwhile B do P od= fix (f : state state. s: state. if VBs then (f CP)s else s ) = s: state. if VBs then (Cwhile B do P od CP)s else s = Cif B then (P; while B do P od) else skip,5.4 指稱語義,6.4.3 操作語義和指稱語義的等價(jià) 引理5.1 令是環(huán)境并且sAstate不是底元。對(duì)任何類型為loc、val或bool的表達(dá)式M，以及Aloc、Aval或Abool中的a，有 M, s eval a 當(dāng)且僅當(dāng) M s = a 對(duì)M的結(jié)構(gòu)進(jìn)行歸納來證明該引理 x, s eval (x) = x s cont x, s eval lookupA s (x) = cont x s f M1 Mk , s eval fA(a1, , ak) = f M1 Mk s,5.4 指稱語義,引理5.2 令F是函數(shù) F f : state state. s: state. if Bs then f (Ps) else s 這是把while循環(huán)翻譯到state, fix, 所得的形式，其中 B: statebool并且P : statestate 令s:state是區(qū)別于state的狀態(tài)。對(duì)任何自然數(shù)n，若 (Fn s) = s，則存在某個(gè)m n，使得s = Pm s， Bs = false，且對(duì)所有的km，有Pk s = sk且Bsk =true 注：對(duì)P : statestate，用Pk s表示把P的k次嚴(yán)格 合成作用到s，也就是Pk s P (P (Ps) ),5.4 指稱語義,定理5.3 令是一個(gè)環(huán)境，并且s, s Astate是任意的“非底元”狀態(tài)。對(duì)任何程序P有 P, s exec s當(dāng)且僅當(dāng) P s = s,5.5 Kernel程序的前后斷言,5.5.1 一階邏輯和部分正確性證明 證明Kernel程序的性質(zhì) 用類型化項(xiàng)上的一般證明系統(tǒng) 使用更適合于Kernel程序語法的邏輯 后一種方式的優(yōu)點(diǎn) 不需要學(xué)習(xí)類型化演算和最小不動(dòng)點(diǎn)概念 程序正確與否的大部分直觀理由都關(guān)聯(lián)到程序的結(jié)構(gòu) 如果證明系統(tǒng)以一種自然的方式反映程序設(shè)計(jì)語言的結(jié)構(gòu)，它可能對(duì)程序設(shè)計(jì)風(fēng)格產(chǎn)生直接的影響,5.5 Kernel程序的前后斷言,Kernel程序的部分正確性斷言的形式 F P G F和G是一階公式，用三類別（val, bool和loc）語言來寫，但不可以含抽象或狀態(tài)變量 P是一段程序 例 (x y cont x = 3) y := 1 ( cont y =1 cont x = 3),5.5 Kernel程序的前后斷言,一階公式的語言 上一階項(xiàng)的定義（項(xiàng)的類別是loc, val或bool） M := x | f M M | cont y| Eq? y z | if B then M else M 一階邏輯公式的定義 F :=M = N| F F | F | locx. F | valx.F| boolx.F 一些縮寫 M N (M = N) F1 F2 (F1 F2) F1 F2 F1 F2 bx.F (bx.F) 對(duì)于b bool, val, loc,5.5 Kernel程序的前后斷言,對(duì)模型A來說，一階公式的可滿足性可以歸納定義如下： , s M = N當(dāng)且僅當(dāng) M s = N s , s F1 F2當(dāng)且僅當(dāng), s F1 并且, s F2 , s F當(dāng)且僅當(dāng)不是, s F , s bx.F當(dāng)且僅當(dāng)對(duì)所有的a Ab， xa, s F,5.5 Kernel程序的前后斷言,部分正確性 (1) 在環(huán)境和狀態(tài)s state下，如果下面的蘊(yùn)涵 若, s F且 P s = s，則, s G 成立，就說部分正確性斷言F P G 在環(huán)境和狀態(tài) sstate下可滿足 (2) 如果 P s = state，則認(rèn)為F P G在s上也得到滿足 (3) 如果在任何環(huán)境和狀態(tài)s state下，部分正確性斷言F P G都可滿足，則說F P G是可滿足的 (4) F P G可滿足不代表程序執(zhí)行一定終止,5.5 Kernel程序的前后斷言,5.5.2 證明規(guī)則 邏輯推論規(guī)則(conseq) 順序推理規(guī)則(seq) 條件推理規(guī)則(cond),5.5 Kernel程序的前后斷言,賦值公理(asg) Mcont xF x := M F 在賦值x := M后對(duì)cont x為真的東西，在賦值前必定 已對(duì)M為真 例 y z x := y cont x z cont w z x := cont w cont x z ycont v x := y cont xcont v / 假定沒有別名 賦值公理為什么不是