命令式程序的语义.ppt

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 5.4 指称语义 命令的语法翻译 C?x := M? = ?s: state. ?update s x (V?M?s)? C?P1; 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在环境?下的含义 ?P?? = A??C?P??? ?P?? s = ( ?P??) s 5.4 指称语义 例 一个简单的程序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? 5.4 指称语义 指称语义可用来证明简单程序之间的等价 证明 while B do P od = if B then (P; while B do P od) else skip C?while B do P od?= fix (?f : state ? state?. ?s: state. if V?B?s then (f ? C?P?)s else ?s? ) = ?s: state. if V?B?s then (C?while B do P od? ? C?P?)s else ?s? = C?if B then (P; while B do P od) else skip? 5.4 指称语义 6.4.3 操作语义和指称语义的等价 引理5.1 令?是环境并且s?Astate不是底元。对任何类型为loc、val或bool的表达式M，以及Aloc、Aval或Abool中的a，有 ?M, s?? ?eval a 当且仅当 ?M?? s = a 对M的结构进行归纳来证明该引理 ?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是函数 F ? ?f : state ? state?. ?s: state. if Bs then f ? (Ps) else ?s? 这是把while循环翻译到?state, fix, ?所得的形式，其中 B: state?bool并且P : state?state? 令s:state是区别于?state的状态。对任何自然数n，若 (Fn ? s) = ?s??，则存在某个m ? n，使得?s?? = P?m s， Bs? = false，且对所有的k?m，有P?k s = ?sk?且Bsk =true 注：对P : state?state?，用P?k s表示把P的k次严格 合成作用到s，也就是P?k s ? P ? (P ? … (Ps) … ) 5.4 指称语义 定理5.3 令?是一个环境，并且s, s?? Astate是任意的“非底元”状态。对任何程序P有 ?P, s?? ?exec s?当且仅当 ?P?? s = ?s?? 5.5 Kernel程序的前后断言 5.5.1 一阶逻辑和部分正确性证明 证明Kernel程序的性质 用类型化?项上的一般证明系统 使用更适合于Kernel程序语法的逻辑 后一种方式的优点 不需要学习类型化?演算和最小不动点概念 程序正确与否的大部分直观理由都关联到程序的结构 如果证明系统以一种自然的方式反映程序设计语言的结构，它可能对程序设计风格产生直接的影响 5.5 Kernel程序的前后断