形式语义学程序设计语言原理课件

1、2022/8/71形式语义学Formal Semantics本PPT参考了金英老师的课程内容2022/8/722022/8/73代数语义学理论基础函数式描述方法程序设计语言形式语义指称语义学操作语义学公理语义学代数功能执行逻辑 关系模型2022/8/74离散数学程序设计语言形式语义编译原理程序设计语言理论基础语义形式化语法形式化2022/8/75软件开发方法程序设计语言形式语义程序设计方法程序设计语言理解抽象能力Formal MethodFormal SpecificationFormal Verification2022/8/76前言：“形式语义学”概述What？形式语义学：给出对(形式)语

2、言及其程序采用形式系统方法进行语义定义的方法。分类：从不同的角度研究程序的含义操作语义学（执行）指称语义学（功能）公理语义学（逻辑）代数语义学（代数，抽象数据结构）其他2022/8/77Lambda演算2022/8/78关于Lambda演算表达式自由变量（计算一个表达式的自由变量集合） 替换（计算） 变换规则 （三种变换）归约 范式（性质及其计算）2022/8/79关于Lambda演算表达式 一个表达式由变量名、抽象符号，.以及括号等符号构成， 其语法为： := | | . | ( )2022/8/710关于Lambda演算变换规则 （三种变换）变换：设E是表达式，x是变量，则称下面变换为变换

3、（其中y不在 FV( x.E )中） x.E - y.y/x E 变换：设 (x.E)和E0为表达式，则称下面变换为变换（称变换规则的左部表达式为基） (x.E)E0 EE0/x变换：假设x.Mx是一个表达式，且满足条件xFV(M)，则称下面变换为变换: (x.M x) M 2022/8/711关于Lambda演算自由变量（计算一个表达式的自由变量集合） 表达式E中变量名x的一次出现称为自由出现，如果E中任何一个形如x. E的子表达式包含该出现；y (x y. y (x. x y ) ) (z (x. x x) )的自由变量集合y, z替换（计算） 设E和E0是表达式，x是变量名，替换EE0/

4、x是表示 把E中的所有x的自由出现替换成E0。需要明确变量的自由出现计算规则( y. x+y) y/x = z. y+z2022/8/712关于Lambda演算范式（性质及其计算）假设E是一个表达式，且其中没有任何一个归约基，则称该表达式为范式。范式的存在性：如果有范式，则最左归约法一定能求出范式。范式的唯一性：如果有范式则在变换下一定唯一。2022/8/713函数式描述方法2022/8/714关于函数式描述方法函数式语言的特点引用透明性；高阶性；模式匹配；并行性；函数式语言的组成部分程序结构类型及其操作表达式用函数式语言来描述算法（解释器）函数空间函数定义（方程）2022/8/715关于函数

5、式描述方法函数式语言的组成部分程序结构函数定义目标表达式类型及其操作标准类型 - 集合类型幂集类型 - 元组类型联合类型 - 序列类型函数类型 - 递归类型抽象类型2022/8/716关于函数式描述方法函数式语言的组成部分表达式非let表达式（常量，变量，表达式，条件表达式，以及各种操作） let表达式 let x = E in E letrec表达式 letrec x = E1 in E在表达式中增加类型说明 2022/8/717关于函数式描述方法用函数式语言来描述算法函数空间：INT* INT BOOL函数定义（方程） lookup L a = (null LFALSE， a=hd LTR

6、UE，lookup (tl L) a )2022/8/718操作语义学2022/8/7192022/8/720操作语义学三种方法解释器方法抽象机归约方法（归约系统）从实现的角度，通过程序的执行过程来定义程序设计语言的语义；2022/8/721操作语义学抽象机方法2022/8/722主要思想：针对计算机语言，定义一个抽象机来解释执行将该语言的程序；抽象机的定义包括两个部分：抽象机组成的抽象定义 状态结构执行机制的形式定义 - 状态转换规则针对如下语言结构给出抽象机定义表达式语句输入输出声明Block过程/函数2022/8/723状态结构（形式定义）栈（保存中间计算结果）语句控制区表达式控制区静态

7、环境区动态环境去堆区（保存中断现场）初始状态和终止状态状态转换规则针对每个语法结构给出执行过程状态到状态的映射基于抽象机的操作语义的定义过程2022/8/724操作语义学归约方法2022/8/725归约方法的主要思想：一种结构化方法（只依赖于成分的结果）根据语言的成分给出归约系统的方法归约系统是由以下部分组成的：一组归约公理一组推理规则，称为归约规则归约的对象为格局（configuration），归约的结果也是格局；初始格局和终止格局；2022/8/726基于归约方法的操作语义的定义过程格局的形式：，通过模式给出初始格局和终止格局一组归约公理：configure1 configure2 一组归

8、约规则形： A1,An 条件公理configure1 configure2 推导出的公理其中A1,An是关于configure1中成分的公理，而configure2中的成分只能从configure1和A1,An中的结果格局中得到；2022/8/7272022/8/7282022/8/7292022/8/7302022/8/7312022/8/732指称语义学2022/8/7332022/8/734指称语义学直接指称语义两个方面定义指称语义（五个部分）完整语言 某个语法单位给出具体语法元素的指称语义解释（语义函数）根据该语法元素所属的语法域的具体的语义指派函数；确定已知条件（静态环境，动态环境）

9、给出语义解释（函数；值）2022/8/735直接指称语义主要原理：从功能角度出发，对每一个语法单位（如程序、声明、语句、表达式、变量、整数、标识符等），给出其功能的严格形式化描述，即定义功能函数；功能函数是描述一个语法单位的语义，因此称为语义函数（语义物）；本质上是建立语法域到语义函数域的映射；语法域语义函数域语义指派函数2022/8/736直接指称语义直接指称语义的定义包括：语法域 （Syntax Domain）抽象语法 （Abstract Syntax）语义域 （Semantic Domain）语义函数 （Semantic Functions）预定义函数 （Predefined Funct

10、ions）关键：掌握好每个语法单位的功能；语言不一样，相同的语法单位其语义也不尽相同；2022/8/737过程式语言的直接指称语义语法域（根据语言定义应给出具体定义）程序声明（还可以细化）语句Block表达式常量类型2022/8/738过程式语言的直接指称语义语义域（根据语言定义应给出具体定义）环境域 静态环境动态环境值域存储域2022/8/739过程式语言的直接指称语义语义函数针对每个语法单位语义指派函数空间针对每个语法单位定义语义指派函数针对每个语法单位中的每种语法元素，定义相应的语义方程2022/8/740公理语义学2022/8/741主要思想公理语义学是基于谓词逻辑中的逻辑归纳方法，一

11、个程序的语义是建立在每次程序运行时都成立的关于变量的值之间关系的断言；定义过程为计算机语言建立一个公理系统公理系统由两部分组成：（1）一组公理；（2）一组推理规则局限性2022/8/7422022/8/7432022/8/7442022/8/7452022/8/7462022/8/747Hoare 公理系统2022/8/748公理和命题的形式： P S Q 推理规则的形式 Hoare公理系统由五条规则赋值公理复合推理规则条件推理规则循环推理规则推论规则F1， , FnF2022/8/749最弱前置条件和最强后置条件2022/8/750最弱前置条件的计算规则求WP(S,q)WP(skip,q)

12、= q;WP(x:=e,q) = qe/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求法？比较复杂2022/8/751最强后置条件的计算规则求SP(p,S)SP(p,skip) = p;SP(p,x:=e) = x(px/x x=ex/x);SP(p,s1;s2) = SP(SP(s1,p),s2);SP(p,if(e,s1,s2) = (SP(pe,s1) SP(pe,s2)2022/8/752程序正确性证明2022/8/753程序正确性证明程序正确性证明目的证明验