形式语义学 Formal Semantics 本PPT参考了金英老师的课程内容 形式语义学 Formal Semantics 2019/4/26

2019/4/26

操作语义学 代数语义学 公理语义学 程序设计语言 形式语义 指称语义学 函数式描述方法 理论基础 执行 公理语义学 程序设计语言 形式语义 代数 逻辑 关系 模型 功能 指称语义学 函数式描述方法 理论基础 2019/4/26

程序设计语言 编译原理 程序设计语言 形式语义 离散数学 语义形式化 语法形式化 程序设计语言 形式语义 理论基础 离散数学 2019/4/26

程序设计语言理解 程序设计方法 抽象能力 程序设计语言 形式语义 软件开发方法 Formal Method 程序设计语言理解 程序设计方法 抽象能力 程序设计语言 形式语义 Formal Verification 软件开发方法 Formal Specification 2019/4/26

前言：“形式语义学”概述 What？ 分类：从不同的角度研究程序的含义 形式语义学：给出对(形式)语言及其程序采用形式系统方法进行语义定义的方法。 分类：从不同的角度研究程序的含义 操作语义学（执行） 指称语义学（功能） 公理语义学（逻辑） 代数语义学（代数，抽象数据结构） 其他 2019/4/26

Lambda演算 2019/4/26

关于Lambda演算 表达式 自由变量（计算一个表达式的自由变量集合） 替换（计算） 变换规则 （三种变换） 归约 范式（性质及其计算） 2019/4/26

关于Lambda演算 表达式 < 表达式> ::= <变量名> 一个表达式由变量名、抽象符号，.以及括号等符号构成， 其语法为： < 表达式> ::= <变量名> | < 表达式> < 表达式> |  <变量名>.< 表达式> | (< 表达式> ) 2019/4/26

关于Lambda演算 变换规则 （三种变换） 变换：设E是表达式，x是变量，则称下面变换为α变换（其中y不在 FV( x.E )中） x.E ------〉 y.[y/x] E 变换：设 (x.E)和E0为表达式，则称下面变换为β变换（称β变换规则的左部表达式为β基） (x.E)E0 E[E0/x] 变换：假设x.Mx是一个表达式，且满足条件xFV(M)，则称下面变换为η变换: (x.M x) M    2019/4/26

关于Lambda演算 自由变量（计算一个表达式的自由变量集合） 替换（计算） 表达式E中变量名x的一次出现称为自由出现，如果E中任何一个形如x. E’的子表达式包含该出现； y (x y. y (x. x y ) ) (z (x. x x) )的自由变量集合{y, z} 替换（计算） 设E和E0是表达式，x是变量名，替换E[E0/x]是表示 把E中的所有x的自由出现替换成E0。 需要明确变量的自由出现 计算规则 ( y. x+y) [y/x] = z. y+z 2019/4/26

关于Lambda演算 范式（性质及其计算） 假设E是一个表达式，且其中没有任何一个归约基，则称该表达式为范式。 范式的存在性：如果有范式，则最左归约法一定能求出范式。 范式的唯一性：如果有范式则在变换下一定唯一。 2019/4/26

函数式描述方法 2019/4/26

关于函数式描述方法 函数式语言的特点 函数式语言的组成部分 用函数式语言来描述算法（解释器） 引用透明性；高阶性；模式匹配；并行性； 程序结构 类型及其操作 表达式 用函数式语言来描述算法（解释器） 函数空间 函数定义（方程） 2019/4/26

关于函数式描述方法 函数式语言的组成部分 程序结构 类型及其操作 函数定义 目标表达式 标准类型 - 集合类型 幂集类型 - 元组类型 标准类型 - 集合类型 幂集类型 - 元组类型 联合类型 - 序列类型 函数类型 - 递归类型 抽象类型 2019/4/26

关于函数式描述方法 函数式语言的组成部分 表达式 非let表达式（常量，变量，表达式，条件表达式，以及各种操作） let表达式 let x = E’ in E letrec表达式 letrec x = E1 in E 在表达式中增加类型说明 2019/4/26

关于函数式描述方法 用函数式语言来描述算法 函数空间：INT*  INT  BOOL 函数定义（方程） lookup L a = (null L→FALSE， a=hd L→TRUE，lookup (tl L) a ) 2019/4/26

操作语义学 2019/4/26

2019/4/26

操作语义学 三种方法 从实现的角度，通过程序的执行过程来定义程序设计语言的语义； 解释器方法 抽象机 归约方法（归约系统） 2019/4/26

操作语义学 抽象机方法 2019/4/26

主要思想： 抽象机的定义包括两个部分： 针对如下语言结构给出抽象机定义 针对计算机语言，定义一个抽象机来解释执行将该语言的程序； 抽象机组成的抽象定义 – 状态结构 执行机制的形式定义 -- 状态转换规则 针对如下语言结构给出抽象机定义 表达式 语句 输入输出 声明 Block 过程/函数 2019/4/26

基于抽象机的操作语义的定义过程 状态结构（形式定义） 初始状态和终止状态 状态转换规则 栈（保存中间计算结果） 语句控制区 表达式控制区 静态环境区 动态环境去 堆区（保存中断现场） 初始状态和终止状态 状态转换规则 针对每个语法结构给出执行过程 状态到状态的映射 2019/4/26

操作语义学 归约方法 2019/4/26

归约的对象为格局（configuration），归约的结果也是格局； 初始格局和终止格局； 归约方法的主要思想： 一种结构化方法（只依赖于成分的结果） 根据语言的成分给出归约系统的方法 归约系统是由以下部分组成的： 一组归约公理 一组推理规则，称为归约规则 归约的对象为格局（configuration），归约的结果也是格局； 初始格局和终止格局； 2019/4/26

基于归约方法的操作语义的定义过程 格局的形式：<comp1,…, compn>，通过模式给出 初始格局和终止格局 一组归约公理： configure1  configure2 一组归约规则形： A1,……,An 条件公理 configure1  configure2 推导出的公理 其中A1,……,An是关于configure1中成分的公理，而configure2中的成分只能从configure1和A1,……,An中的结果格局中得到； 2019/4/26

2019/4/26

2019/4/26

2019/4/26

2019/4/26

2019/4/26

指称语义学 2019/4/26

2019/4/26

指称语义学 直接指称语义 两个方面 定义指称语义（五个部分） 给出具体语法元素的指称语义解释（语义函数） 完整语言 某个语法单位 根据该语法元素所属的语法域的具体的语义指派函数； 确定已知条件（静态环境，动态环境） 给出语义解释（函数；值……） 2019/4/26

直接指称语义 主要原理： 从功能角度出发，对每一个语法单位（如程序、声明、语句、表达式、变量、整数、标识符等），给出其功能的严格形式化描述，即定义功能函数； 功能函数是描述一个语法单位的语义，因此称为语义函数（语义物）； 本质上是建立语法域到语义函数域的映射； 语法域 语义函数域 语义指派函数 2019/4/26

直接指称语义 直接指称语义的定义包括： 语法域 （Syntax Domain） 抽象语法 （Abstract Syntax） 语义域 （Semantic Domain） 语义函数 （Semantic Functions） 预定义函数 （Predefined Functions） 关键：掌握好每个语法单位的功能； 语言不一样，相同的语法单位其语义也不尽相同； 2019/4/26

过程式语言的直接指称语义 语法域（根据语言定义应给出具体定义） 程序 声明（还可以细化） 语句 Block 表达式 常量 类型 2019/4/26

过程式语言的直接指称语义 语义域（根据语言定义应给出具体定义） 环境域 静态环境 动态环境 值域 存储域 2019/4/26

过程式语言的直接指称语义 语义函数 针对每个语法单位语义指派函数空间 针对每个语法单位定义语义指派函数 针对每个语法单位中的每种语法元素，定义相应的语义方程 2019/4/26

公理语义学 2019/4/26

主要思想 公理语义学是基于谓词逻辑中的逻辑归纳方法，一个程序的语义是建立在每次程序运行时都成立的关于变量的值之间关系的断言； 定义过程 为计算机语言建立一个公理系统公理系统由两部分组成： （1）一组公理；（2）一组推理规则 局限性 2019/4/26

2019/4/26

2019/4/26

2019/4/26

2019/4/26

2019/4/26

Hoare 公理系统 2019/4/26

公理和命题的形式：{ P } S { Q } 推理规则的形式 Hoare公理系统由五条规则 F1，…… , Fn F 赋值公理 复合推理规则 条件推理规则 循环推理规则 推论规则 F1，…… , Fn F 2019/4/26

最弱前置条件和最强后置条件 2019/4/26

最弱前置条件的计算规则 求WP(S,q) 为什么没有给出while语句的WP求法？ WP(skip,q) = q; WP(x:=e,q) = q[e/x]; WP(s1;s2,q) = WP(s1,WP(s2,q)); WP(if(e,s1,s2),q) = (e  WP(s1,q))  (e  WP(s2,q)) 为什么没有给出while语句的WP求法？ 比较复杂 2019/4/26

最强后置条件的计算规则 求SP(p,S) SP(p,skip) = p; SP(p,x:=e) = x’(p[x’/x]  x=e[x’/x]); SP(p,s1;s2) = SP(SP(s1,p),s2); SP(p,if(e,s1,s2)) = (SP(pe,s1)  SP(pe,s2)) 2019/4/26

程序正确性证明 2019/4/26

程序正确性证明 程序正确性证明 目的 采用的方法 （应用Hoare公理系统，SP，WP） 难点:循环不变式 证明验证公式{p}S{q}成立 Forward Backward Meet in the middle 难点:循环不变式 2019/4/26

求循环不变式过程 步骤： 从循环语句出发，手工找出一些循环不变式； 然后将它们合取，从而构造出更强的循环不变式； 检查强度，直至找到合适的循环不变式； 2019/4/26