第5章 命令式程序的语义 函数式程序 命令式程序 本章围绕一个叫做Kernel的简单的命令式语言来讨论语义

Presentation on theme: "第5章 命令式程序的语义 函数式程序 命令式程序 本章围绕一个叫做Kernel的简单的命令式语言来讨论语义"— Presentation transcript:

1 第5章 命令式程序的语义 函数式程序 命令式程序 本章围绕一个叫做Kernel的简单的命令式语言来讨论语义
第5章 命令式程序的语义 函数式程序 不含赋值或其它形式的改变变量值的操作 命令式程序 赋值语句是典型的构造 本章围绕一个叫做Kernel的简单的命令式语言来讨论语义

2 5.1 引 言 Kernel语言的结构由下面的文法概括 例 求对数
5.1 引 言 Kernel语言的结构由下面的文法概括 P ::= x:= M | P ; P | if B then P else P | while B do P od x和M都有适当的类型val B的类型是bool 没有显式的输入、输出，也没有局部变量声明 例 求对数 x := 1; y := 0; while x < z do x := x + x; y := y + 1 od

3 5.1 引 言 本章主要内容 围绕Kernel来讨论命令式语言的语义 基于一组重写规则的结构化操作语义
5.1 引 言 本章主要内容 围绕Kernel来讨论命令式语言的语义 基于一组重写规则的结构化操作语义 使用类型化演算和论域（CPO）来表示的指称语义 把Kernel程序翻译成类型化演算的表达式 利用类型化演算的指称语义 基于Floyd-Hoare逻辑的公理语义

4 5.2 Kernel语言 5.2.1 存储单元 Kernel的变量可赋值 变量的左值和右值 为方便讨论，修改语言
与函数式语言let子句引入的变量有很大区别 可赋值变量指称存储单元 变量的左值和右值 左值是变量的存储单元的地址 右值是该存储单元存放的内容 为方便讨论，修改语言 显式区分左值和右值，例x和cont x

5 5.2 Kernel语言 例1 求对数 例2：计算m除以n的商q和余数r x := 1; y :=0;
例1 求对数 x := 1; y :=0; while cont x < z do x := cont x + cont x; y := cont y + 1 od 例2：计算m除以n的商q和余数r q := 0; r := m; while cont r  n do q := cont q +1; r := cont r – n;

6 5.2 Kernel语言 5.2.2 表达式的解释 在文法中，M和B分别代表val和bool表达式 不深入表达式的内部细节
P ::= x := M | P ; P | if B then P else P | while B do P od 不深入表达式的内部细节 为方便起见，把val看作nat 允许普通的数值和布尔运算

7 5.2 Kernel语言 用4类别代数A来建立Kernel的抽象机器模型 本小节先介绍相应代数规范的三个类别
作为介绍操作语义和指称语义的共同基础 便于比较操作语义和指称语义 本小节先介绍相应代数规范的三个类别 基调包含3类别val、bool和loc 仅关心loc类别有一个取存储单元内容的函数符号 cont : loc  val 环境把变量从 loc  val  bool映射到A的元素 loc：程序中的变量； val和bool ：程序中的常量 Abool的解释是布尔值集合{true, false}

8 5.2 Kernel语言 5.2.3 程序状态 操作语义和指称语义都涉及“状态”数据结构 名字 存储单元 状态 值 环境
从名字到值的两步映射

9 5.2 Kernel语言 基调的第4个类别state init : state
update : state  loc  val  state lookup : state  loc  val 代数公理 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

10 5.2 Kernel语言 四类别代数A Aloc是任意的可数集合，Astate是从Aloc到Aval的所有函数的集合
initA是任意的常函数 lookupA(s, l) = s(l) updateA(s, l, v)是函数s，除了s(l) = v以外，s等同于s 为了记号上的方便，下面用init，lookup和update代替initA，lookupA和updateA

11 5.2 Kernel语言 两个问题 为什么不在前三个类别的基础上引入作为状态的函数state = loc  val，而要引入第4个类别state 若那样，则lookup和update成了高阶的函数符号 为什么不用一个函数直接从变量映射到值，而要分离出环境和状态 直观上讲，环境和状态在概念上有区别，它们分 别对应到实际语言实现的不同机制 从技术角度说，Kernel没有提供声明常量的值的方式，只能将程序中常量的取值交给环境来确定

12 5.3 操作语义 5.3.1 表达式的求值 操作语义分成两部分 表达式的语义 表达式的计算 语句的执行
5.3 操作语义 5.3.1 表达式的求值 操作语义分成两部分 表达式的计算 语句的执行 表达式的语义 表达式、环境、状态和表达式的语义值之间的一个四元关系：M, s eval v 环境下标在下面将省略 eval由一个证明系统来给出

13 M1, s eval v1 … Mk, s eval vk
5.3 操作语义 eval公理 x, s eval  (x) c, s eval cA eval推理规则 fA(v1,…, vk)=v lookupA(s, l)=v M1, s eval v1 … Mk, s eval vk f M1… Mk, s eval v x, s eval l cont x, s eval v

14 5.3 操作语义 5.3.2 命令的执行 命令的执行可以用关系exec来刻画 M, s eval v
5.3 操作语义 5.3.2 命令的执行 命令的执行可以用关系exec来刻画 updateA(s, (x), v)=s M, s eval v x := M, s exec s P1, s exec s P2, s exec s  P1;P2, s exec s B, s eval true P1, s exec s if B then P1elseP2, s exec s

15 5.3 操作语义 B, s eval false P2, s exec s
5.3 操作语义 B, s eval false P2, s exec s if B then P1elseP2, s exec s B, s eval false while B do P od, s exec s B, s eval true P, s exec s while B do P od, s exec s while B do P od, s exec s

16 5.3 操作语义 如果想证明P, s exec s,需要观察P的语法形式,考察哪条规则是完成该证明的最后一条规则 例 p := 0;
5.3 操作语义 如果想证明P, s exec s,需要观察P的语法形式,考察哪条规则是完成该证明的最后一条规则 例 p := 0; m := 0; while (cont m)  n do p := cont m; m := (cont m) +1; od

17 5.3 操作语义 p := 0; s1 = updateA s lp 0 m := 0; while (cont m)  n do
5.3 操作语义 p := 0; s1 = updateA s lp 0 m := 0; while (cont m)  n do p := cont m; m := (cont m) +1; od

18 5.3 操作语义 p := 0; s1 = updateA s lp 0 m := 0; s2 = updateA s1 lm 0
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

19 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0
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

20 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0
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

21 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0
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

22 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0
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

23 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0
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

24 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0
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 (p := cont m; m := (cont m) +1), s3 exec s4 od

25 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0
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 & lookupA s4 lm = 2 (p := cont m; m := (cont m) +1), s3 exec s4 od

26 5.4 指称语义 5.4.1带状态的类型化演算 前两章已经给出了类型化演算的指称语义 只要给出从Kernel语言到类型化演算的翻译即可
5.4 指称语义 5.4.1带状态的类型化演算 前两章已经给出了类型化演算的指称语义 只要给出从Kernel语言到类型化演算的翻译即可 把Kernel程序翻译成类型化演算state, fix,  该演算有类型常量val, bool, loc, state和state state, fix, 演算还增加的运算 Eq? : loc  loc  bool 在state上的运算init, update和lookup

27 5.4 指称语义 每个类型都有条件运算if…then…else 还有提升运算（在下面描述），抽象，应用和不动点算子
5.4 指称语义 每个类型都有条件运算if…then…else 还有提升运算（在下面描述），抽象，应用和不动点算子 fixstate : ((state  state)  (state  state))  (state  state) state, fix, 的CPO模型A是四类别代数A的一个拓展 val, bool, loc和state的解释同A的解释一样 state被解释成提升集合Astate = (Astate) 这种解释延伸到函数类型,Astate  state 有最小元，该类型有最小不动点算子  

28   M: state  state   N: state
5.4 指称语义 提升运算 · :state  state 如果M:state,让M和M有同样的指称但不同的类型 中缀算符  (state Elim)   M   = : state   M  N = MN : state 函数合成的严格形式美化成 M  N  s : state. M  (N s)   M: state  state   N: state   M  N: state

29 5.4 指称语义 5.4.2 语义函数 指称语义由两部分组成 语法翻译部分 表达式和命令到state, fix, 项的语法翻译
5.4 指称语义 5.4.2 语义函数 指称语义由两部分组成 表达式和命令到state, fix, 项的语法翻译 这个演算在模型A中的标准解释 语法翻译部分 函数V·: 把布尔表达式和值表达式分别翻译成类型为state  bool和state  val的项 函数C·: 把命令翻译成类型为state  state的项

30 5.4 指称语义 语义函数 把这些语法翻译和从state, fix, 的项到模型A的标准含义函数组合起来
5.4 指称语义 语义函数 把这些语法翻译和从state, fix, 的项到模型A的标准含义函数组合起来 : expressions  environments  Astate  Avalues : commands  environments  Astate  Astate 

31 5.4 指称语义 表达式的语法翻译 表达式M在环境中的含义 Vx= s: state. x
5.4 指称语义 表达式的语法翻译 Vx= s: state. x Vcont x= s: state. lookup s x V f M1 … Mk = s: state. f VM1s …VMks 表达式M在环境中的含义 M = AVM M s = ( M)s

32 5.4 指称语义 命令的语法翻译 程序P在环境下的含义
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

33 5.4 指称语义 例 一个简单的程序skip  x := cont x
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

34 5.4 指称语义 指称语义可用来证明简单程序之间的等价 证明
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

35 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

36 5.4 指称语义 引理5.2 令F是函数 s: state. if Bs then f  (Ps) else 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) … )

37 5.4 指称语义 定理5.3 令是一个环境，并且s, s Astate是任意的“非底元”状态。对任何程序P有
5.4 指称语义 定理5.3 令是一个环境，并且s, s Astate是任意的“非底元”状态。对任何程序P有 P, s exec s当且仅当 P s = s

38 5.5 Kernel程序的前后断言 5.5.1 一阶逻辑和部分正确性证明 证明Kernel程序的性质 后一种方式的优点
用类型化项上的一般证明系统 使用更适合于Kernel程序语法的逻辑 后一种方式的优点 不需要学习类型化演算和最小不动点概念 程序正确与否的大部分直观理由都关联到程序的结构 如果证明系统以一种自然的方式反映程序设计语言的结构，它可能对程序设计风格产生直接的影响

39 5.5 Kernel程序的前后断言 Kernel程序的部分正确性断言的形式 {F} P {G}
F和G是一阶公式，用三类别（val, bool和loc）语言来写，但不可以含抽象或状态变量 P是一段程序 例 {(x  y  cont x = 3)} y := 1 {( cont y =1  cont x = 3)}

40 5.5 Kernel程序的前后断言 一阶公式的语言 上一阶项的定义（项的类别是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) 对于b {bool, val, loc}

41 5.5 Kernel程序的前后断言 对模型A来说，一阶公式的可满足性可以归纳定义如下：
, s  M = N当且仅当 M s = N s , s  F1  F2当且仅当, s  F1 并且, s  F2 , s   F当且仅当不是, s  F , s  bx.F当且仅当对所有的a  Ab， [xa], s  F

42 5.5 Kernel程序的前后断言 部分正确性 (1) 在环境和状态s state下，如果下面的蕴涵
若, s  F且 P  s = s，则, s  G 成立，就说部分正确性断言{F} P {G} 在环境和状态 sstate下可满足 (2) 如果 P  s = state，则认为{F} P {G}在s上也得到满足 (3) 如果在任何环境和状态s  state下，部分正确性断言{F} P {G}都可满足，则说{F} P {G}是可满足的 (4) {F} P {G}可满足不代表程序执行一定终止

43 5.5 Kernel程序的前后断言 5.5.2 证明规则 逻辑推论规则(conseq)  顺序推理规则(seq) 条件推理规则(cond)
{F}P{G} F  F G  G  {F }P{G } {F}P1{G} {G}P2{H} {F} P1; P2 {H} {F  B}P1{G} {F  B}P2{G} {F} if B then P1 else P2 {G}

44 5.5 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}

45 {F} while B do P od {F  B}
5.5 Kernel程序的前后断言 while规则(while) F叫做循环不变式 {F  B} P {F} {F} while B do P od {F  B}

46 5.5 Kernel程序的前后断言 例 考虑下面计算x - y的简单程序，假定y  x d := 0; —P0
while (cont d ) + y < x do —B d := (cont d ) + 1; —P1 od 证明 {y  x} P0; while B do P1 od {(cont d) + y = x}

47 5.5 Kernel程序的前后断言 d := 0; while (cont d ) + y < x do —B
d := (cont d ) + 1; od (a) {y  x} d := 0 {(cont d ) + y  x} (b) {((cont d)+y  x)  B}d:=(cont d) +1{(cont d)+y  x} (cont d) + y  x)  B  (cont d ) + y < x {(cont d) + y < x} d:=(cont d) + 1{(cont d) + y  x} (cont d)+y  x是循环不变式 (c) ((cont d) + y  x)  B  (cont d) + y = x

48 5.5 Kernel程序的前后断言 5.5.3 可靠性 使用程序的指称语义来证明可靠性 断言语言的证明系统对指称模型可靠
断言语言上的证明系统用的就是经典逻辑的公理和推理规则，它们的可靠性证明比较简单 Hoare逻辑的公理和推理规则对指称模型可靠

49 5.5 Kernel程序的前后断言 5.5.3 可靠性 使用程序的指称语义来证明可靠性 定理5.4 假定部分正确性规范FPG可证，
那么FP G在模型A中有效 只要证明该公理语义中的公理和推理规则对模型A中都可靠就可以了 49

50 习 题 第一次：5.2，5.6, (a), (b), (c)