命令式程序的语义

《命令式程序的语义》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第5章命令式程序的语义函数式程序不含赋值或其它形式的改变变量值的操作命令式程序赋值语句是典型的构造本章围绕一个叫做Kernel的简单的命令式语言来讨论语义5.1引言Kernel语言的结构由下面的文法概括P::=x:=M

2、P;P

3、ifBthenPelseP

4、whileBdoPodx和M都有适当的类型valB的类型是bool没有显式的输入、输出，也没有局部变量声明例求对数x:=1;y:=0;whilex

5、称语义把Kernel程序翻译成类型化演算的表达式利用类型化演算的指称语义基于Floyd-Hoare逻辑的公理语义5.2Kernel语言5.2.1存储单元Kernel的变量可赋值与函数式语言let子句引入的变量有很大区别可赋值变量指称存储单元变量的左值和右值左值是变量的存储单元的地址右值是该存储单元存放的内容为方便讨论，修改语言显式区分左值和右值，例x和contx5.2Kernel语言例1求对数x:=1;y:=0;whilecontx

6、ndoq:=contq+1;r:=contr–n;od5.2Kernel语言5.2.2表达式的解释在文法中，M和B分别代表val和bool表达式P::=x:=M

7、P;P

8、ifBthenPelseP

9、whileBdoPod不深入表达式的内部细节为方便起见，把val看作nat允许普通的数值和布尔运算5.2Kernel语言用4类别代数A来建立Kernel的抽象机器模型作为介绍操作语义和指称语义的共同基础便于比较操作语义和指称语义本小节先介绍相应代数规范的三个类别基调包含3类别val、bool和loc仅关心loc类别有一个取存储单元内容的函数符号cont:locval环

10、境把变量从locvalbool映射到A的元素loc：程序中的变量；val和bool：程序中的常量Abool的解释是布尔值集合{true,false}5.2Kernel语言5.2.3程序状态操作语义和指称语义都涉及“状态”数据结构名字存储单元状态值环境从名字到值的两步映射5.2Kernel语言基调的第4个类别stateinit:stateupdate:statelocvalstatelookup:statelocval代数公理lookup(updateslv)l=(lookup)ifEq?llthenvelse(lookupsl)upd

11、atesl(lookupsl)=s(update)1update(updateslu)lv=ifEq?ll(update)2thenupdateslvelseupdate(updateslv)lu5.2Kernel语言四类别代数AAloc是任意的可数集合，Astate是从Aloc到Aval的所有函数的集合initA是任意的常函数lookupA(s,l)=s(l)updateA(s,l,v)是函数s，除了s(l)=v以外，s等同于s为了记号上的方便，下面用init，lookup和update代替initA，lookupA和updateA5.2Kernel语言

12、两个问题为什么不在前三个类别的基础上引入作为状态的函数state=locval，而要引入第4个类别state若那样，则lookup和update成了高阶的函数符号为什么不用一个函数直接从变量映射到值，而要分离出环境和状态直观上讲，环境和状态在概念上有区别，它们分别对应到实际语言实现的不同机制从技术角度说，Kernel没有提供声明常量的值的方式，只能将程序中常量的取值交给环境来确定5.3操作语义5.3.1表达式的求值操作语义分成两部分表达式的计算语句的执行表达式的语义表达式、环境、状态和表达式的语义值之间的一个四元关系：M,sevalv环境下标在下面将省略e

13、val由一个证明系统来给出5.3操作语义eval公理x,seval(x)c,sevalcAeval推理规则fA(v1,…,vk)=vlookupA(s,l)=vM1,sevalv1…Mk,sevalvkfM1…Mk,sevalvx,sevallcontx,sevalv5.3操作语义5.3.2命令的执行命令的执行可以用关系exec来刻画updateA(s,(x),v)=sM,sevalvx:=M,sexecsP1,sexecsP2,sexecsP1;P2,se