形式语义-操作语义PPT课件.ppt

程序设计语言的形式语义 TheFormalSemanticsofProgrammingLanguages 操作语义 操作语义 operationalsemantics 通过描述程序语法构造在机器上的运行效果而定义程序的语义 以抽象机器为语义解释对象操作语义关注程序的运行效果是怎样得到的HOW 2 操作语义 操作语义概述 1 1960s 对编译程序所产生的目标程序标准化 形式化的愿望 自动机理论研究的兴旺时期抽象机 抽象机是操作语义的核心 既是具体机器的抽象化 又是自动机的高级化 向着直接反映高级语言语义的方向靠近 MaCarthy 比较明确的提出用抽象机表达操作语义 并用它描述了ALGOL60的一个子集的语义 1964年Landin SECD Stack Environment Control Dump 扩充为SM 共享机 描述了ALGOL60完整语义 1968年 Knuth提出属性文法 3 操作语义 操作语义概述 2 传统的操作语义的顶峰是VDL 维也纳定义语言 IBM的维也纳实验室 形式化定义PL 1语言与此同时 英国赫斯利实验室对PL 1语言的形式化被ANSI接受为标准 形式化程度较低 规范的自然语言描述 操作语义的另一个变种是变换语义 用分而治之的思想降低复杂度 抽象复杂度 翻译复杂度 德国CIP小组提出的广谱语言 M5 M4 M3 M2 M11981 Plotkin提出结构化的操作语义 把公理化方法引入操作语义中 基本思想是 复合成分的操作语义可以归结为其各个组成部分的操作语义 4 IMP 一种简单的命令式语言 IMP语言的语法范畴 N 数集 包括正整数 负整数和零带符号位的正负十进制数的集合T 真值集 T true false Loc 存储单元集字母开头的字母数字串Aexp 算术表达式集Bexp 逻辑表达式集Com 命令集 5 IMP 一种简单的命令式语言 语法成分的元变量 约定 n m表示数集N中的元素x y表示存储单元集Loc中的元素a表示算术表达式集Aexp中的元素b表示逻辑表达式集Bexp中的元素c表示命令集Com中的元素可以加上标或下标 6 IMP 一种简单的命令式语言 算术表达式的抽象语法 7 IMP 一种简单的命令式语言 逻辑表达式的抽象语法 8 IMP 一种简单的命令式语言 命令的抽象语法 四种语句空语句赋值语句分支语句循环语句程序命令 程序语句 程序 9 IMP 一种简单的命令式语言 定义2 1 IMP语言的算术表达式 逻辑表达式及命令的抽象语法 10 IMP 一种简单的命令式语言 IMP语言语法扩展 为了讲课方便扩充了一些运算 非本质的 11 IMP 一种简单的命令式语言 例2 1交换程序及其语法树 12 IMP 一种简单的命令式语言 例2 2阶乘程序 13 变迁系统 操作语义通过描述程序在抽象机器上的运行过程来描述程序的语义 运行过程用程序状态和当前要执行的命令的变换序列给出 格局 configuration 程序的运行过程就是格局的变换序列 14 变迁系统 状态 直观模型 存储单元的内容决定了当前的状态状态集合 Loc N x 是状态 下存储单元x的值或内容 程序中所出现的变量 15 变迁系统 格局 程序状态 是一个特殊的格局变迁系统 TransitionSystem 转换系统 变迁系统是二元组 X R 在状态 下将要执行c 语句为空 省略尖括号 变迁系统的状态集 其元素称为状态或格局 R X X状态之间的变迁关系 16 变迁系统 可以将IMP程序理解为运行在一个变迁系统上运行过程是程序状态和下一步要执行的程序语句的变化变迁关系 c1 1 c2 2 程序 命令 c1在状态 1运行后得到状态 2且下一步要执行的程序是c2 c1 1 2 程序 命令 c1在状态 1运行后得到状态 2且没有后续语句要执行 程序结束 17 变迁系统 小结 描述IMP语言的操作语义 格局程序 命令 c在状态下 运行 程序终止的状态 变迁关系定义IMP语言的操作语义就是定义适当格局之间的变迁关系通过定义IMP语言的每个命令所引起的变迁来完成 18 表达式的语义 表达式是IMP语言的最基本的语法成分 包括算术表达式和逻辑表达式程序执行是对程序状态的变换 而表达式的计算并不改变程序状态 可以看作是对程序状态的某种观察 状态 Loc N定义一个新状态 程序变量x在该状态下的值就是v 而其他变量的值不变 未知或不关心 19 表达式的语义 算术表达式的求值 序偶表示状态 下表达式a等待求值求值关系 状态 下表达式a的求值结果为n 20 表达式的语义 算术表达式的求值 求值规则 积 21 表达式的语义 逻辑表达式的求值 求值规则 1 22 表达式的语义 逻辑表达式的求值 求值规则 2 23 表达式的语义 24 表达式的语义 逻辑表达式的求值 最左顺序计算 短路 25 表达式的语义 说明 规则一般包括前提和结论 后面的条件称为附加条件 有些规则没有前提部分 前提为空的规则称为公理 有时在上面加一条实线 由前提推出结论称为规则的一个应用 用特定的数 存储单元 表达式以及状态来替代规则的元变量 就得到一个规则实例 求值过程 推导树 26 表达式的语义 状态 0下表达式 Init 5 7 9 的求值 0 Init 0 推导树由规则的实例构成 每个实例的前提正好是上一层实例的结论 公理位于最顶层 公理的上方没有前提部分 最底层的实例的结论称为整个推导的结论 如果某个推导存在结论 称该结论是从规则可精确推导的 匹配的规则可能有多条 必须考虑所有左部与格局匹配的规则 对于符合条件的所有推导必须并行地构造 27 表达式的语义 状态 下布尔表达式 x y z z x 0 的求值 x 3 y 5 z 7 28 表达式的语义 算术表达式的等价逻辑表达式的等价 29 命令的语义 自然语义 操作语义定义适当格局之间的变迁关系程序 命令 通过执行来改变状态 表示在状态 下执行完命令c终止于终态 例如 30 命令的语义 自然语义 命令的规则 1 原子命令 实例 初始状态下所有存储单元的值均为0 31 命令的语义 自然语义 命令的规则 2 顺序命令 实例 32 命令的语义 自然语义 命令的规则 3 条件命令 33 命令的语义 自然语义 命令的规则 3 条件命令实例 34 命令的语义 自然语义 命令的规则 4 循环命令 35 命令的语义 自然语义 命令的规则 4 循环命令实例 循环体每执行一步的变迁关系 36 命令的语义 自然语义 死循环 这种推导是无穷的 因此 实际上不存在状态 使得 语义无定义 37 命令的语义 自然语义 命令的规则小结 38 命令的语义 自然语义 推导树例1 交换程序 39 命令的语义 自然语义 例2 阶乘程序 0 x 3 0 y 0 40 命令的语义 自然语义 小结 自然语义 可以看作如下形式的函数 对任意的命令c 自然语义函数是从状态集 到 的部分函数有定义 无定义至多存在一个终止状态 41 等价关系及证明 命令的等价 语义等价 例 42 等价关系及证明 命题2 8 P16 证明 对所有的状态 有 两方面 43 等价关系及证明 1 44 等价关系及证明 45 等价关系及证明 46 等价关系及证明 2 47 等价关系及证明 由于 所以 48 等价关系及证明 49 自然语义小结 自然语义 至多存在一个终止状态 语义等价关系 50 自然语义小结 51 自然语义小结 练习 整除程序的推导树 52 自然语义小结 练习 整除程序的推导树 53 另一种语义 结构化操作语义 与自然语义比较自然语义所给出的变迁关系是一步到位的 另一种语义 结构化操作语义 描述程序执行中每一小步的中间状态 54 另一种语义 结构化操作语义 原子命令的结构化操作语义 55 另一种语义 结构化操作语义 顺序命令的结构化操作语义 56 另一种语义 结构化操作语义 条件命令的结构化操作语义 57 另一种语义 结构化操作语义 循环命令的结构化操作语义 58 另一种语义 结构化操作语义 规则 59 另一种语义 结构化操作语义 例1 交换程序 推导序列 60 另一种语义 结构化操作语义 推导序列 61 另一种语义 结构化操作语义 62 另一种语义 结构化操作语义 例2 阶乘程序 63 另一种语义 结构化操作语义 例2 阶乘程序 64 另一种语义 结构化操作语义 例2 阶乘程序 65 另一种语义 结构化操作语义 例2 阶乘程序 66 另一种语义 结构化操作语义 例2 阶乘程序 67 另一种语义 结构化操作语义 例2