5.2 Kerneli语言 ·两个问题 为什么不在前三个类别的基础上引入作为状态的 函数state=loc→val,而要引入第4个类别state 若那样，则lookupi和update)成了高阶的函数符号 为什么不用一个函数直接从变量映射到值，而要 分离出环境和状态 直观上讲，环境和状态在概念上有区别，它们分 别对应到实语言实现的不同机制 从技术角度说，Kernel没有提供声明常量的值的 方式，只能将程序中常量的取值交给环境来确定
5.2 Kernel语言 • 两个问题 – 为什么不在前三个类别的基础上引入作为状态的 函数state = loc → val，而要引入第4个类别state 若那样，则lookup和update成了高阶的函数符号 – 为什么不用一个函数直接从变量映射到值，而要 分离出环境和状态 直观上讲，环境和状态在概念上有区别，它们分 别对应到实际语言实现的不同机制 从技术角度说，Kernel没有提供声明常量的值的 方式，只能将程序中常量的取值交给环境来确定
5.3操作语义 5.3.1表达式的求值 操作语义分成两部分 -表达式的计算 -语句的执行 表达式的语义 表达式、环境、状态和表达式的语义值之间的一 个四元关系：M,s)n→aN 一环境下标在下面将省略 -→eval由一个证明系统来给出
5.3 操作语义 5.3.1 表达式的求值 • 操作语义分成两部分 – 表达式的计算 – 语句的执行 • 表达式的语义 –表达式、环境、状态和表达式的语义值之间的一 个四元关系：M, s →eval v – 环境下标在下面将省略 – →eval由一个证明系统来给出
5.3操作语义 ·-→eam公理 (x,S〉-→eal7(c) -〈c,S）-→eval CA →ea推理规则 (M,s〉-→emly1…〈Mn〉-之erat V&(Vp,w小y fM1.M3S〉-→eval V 〈k,S〉-→ealI lookupA(s,D)=v (contx,S〉→eval V
5.3 操作语义 • →eval公理 – x, s →eval (x) – c, s →eval c A • →eval推理规则 f A(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
5.3 操作语义 5.3.2命令的执行 命令的执行可以用关系→>c来刻画 (M,S〉-→evat V updateA(s,n(x),v)=s' K:=M,S〉-→exec S KP1,S〉-→exec S'(P2,s'〉→exec S" 〈P1;P2z,S〉-→exec S” KB,S〉-→eval true〈Pi,S〉-→exec S' (if B then P1 elseP2,S〉→exes
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 P1 elseP2 , s →exec s
5.3 操作语义 KB,s〉→eval false(Pz,S〉→exec S' if B then Pielsep2,s)->exec s' 〈B,s)-→eval false 〈while B do Pod,S〉→eees KB,s)-→eval true(P,s)→exec S'(while B do P od,.s'）→>exes' while B do Pod,.S〉-→exec S
5.3 操作语义 B, s →eval false P2 , s →exec s if B then P1 elseP2 , 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