第5章命令式程序的語義(參考版)
2025-07-23 11:28本頁面
【正文】 while (cont d ) + y x do —B d := (cont d ) + 1。 —P1 od 證明 {y ? x} P0。 P2 {H} {F ? B}P1{G} {F ? ?B}P2{G} {F} if B then P1 else P2 {G} Kernel程序的前后斷言 ? 賦值公理 (asg) {[M?cont x]F} x := M {F} 在賦值 x := M后對 cont x為真的東西 ， 在賦值前必定 已對 M為真 ? 例 – {y ? z} x := y {cont x ? z} – {cont w ? z} x := cont w {cont x ? z} – {y?cont v} x := y {cont x?cont v} // 假定沒有別名 ? 賦值公理為什么不是正向的 {F} x := y {[(cont x)/y]F} Kernel程序的前后斷言 ? while規(guī)則 (while) F叫做循環(huán)不變式 {F ? B} P {F} {F} while B do P od {F ? ?B} Kernel程序的前后斷言 ? 例 考慮下面計(jì)算 x y的簡單程序 ， 假定 y ? x d := 0。 對任何自然數(shù) n， 若 (Fn ? s) = ?s??， 則存在某個(gè) m ? n， 使得 ?s?? = P?m s， Bs? = false， 且對所有的 k?m， 有 P?k s = ?sk?且 Bsk =true 注：對 P : state?state?， 用 P?k s表示把 P的 k次嚴(yán)格 合成作用到 s， 也就是 P?k s ? P ? (P ? … (Ps) … ) 指稱語義 ? 定理 令 ?是一個(gè)環(huán)境 ， 并且 s, s?? Astate是任意的 “ 非底元 ” 狀態(tài) 。 while B do P od) else skip? 指稱語義 操作語義和指稱語義的等價(jià) ? 引理 令 ?是環(huán)境并且 s?Astate不是底元 。 P2? = C?P2? ? C?P1? – C?if B then P1 else P2? = ?s: state. if V?B?s then C?P1?s else C?P2?s – C?while B do P od? = fix(?f : state ? state?. ?s: state. if V?B?s then (f ? C?P?)s else ?s?) ? 程序 P在環(huán)境 ?下的含義 – ?P?? = A??C?P??? – ?P?? s = ( ?P??) s CC C 指稱語義 ? 例 一個(gè)簡單的程序 skip ? x := cont x C?skip?? = ?s: state.?update s x (V?cont x?s)? = ?s: state.?update s x (lookup s x)? = ?s: state. ?s? ?skip?? s = (A??C?skip???)(s) = (A???s: state. ?s???)(s) = ?s? C 指稱語義 ? 指稱語義可用來證明簡單程序之間的等價(jià) 證明 while B do P od = if B then (P。?: 把 布爾表達(dá)式和值表達(dá)式分別翻譯成類型為 state ? bool和 state ? val的 ?項(xiàng) – 函數(shù) C? m := (cont m) +1), s3? ?exec s4 od 指稱語義 ?演算 ? 前兩章已經(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 指稱語義 – 每個(gè)類型都有條件運(yùn)算 if… then… else – 還有提升運(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)? –
環(huán)評公示相關(guān)推薦
鄂ICP備17016276號-1