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

《形式语义学-程序设计语言原理ppt课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、形式语义学FormalSemantics本PPT参考了金英老师的课程内容2021/7/2812021/7/282代数语义学理论基础函数式描述方法程序设计语言形式语义指称语义学操作语义学公理语义学代数功能执行逻辑关系模型2021/7/283离散数学程序设计语言形式语义编译原理程序设计语言理论基础语义形式化语法形式化2021/7/284软件开发方法程序设计语言形式语义程序设计方法程序设计语言理解抽象能力FormalMethodFormalSpecificationFormalVerification2021/7/285前言：“形式语义学”概述What？形式语义学：给出对

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

3、<表达式><表达式>

4、<变量名>.<表达式>

5、(<表达式>

6、)2021/7/289关于Lambda演算变换规则（三种变换）变换：设E是表达式，x是变量，则称下面变换为α变换（其中y不在FV(x.E)中）x.E------〉y.[y/x]E变换：设(x.E)和E0为表达式，则称下面变换为β变换（称β变换规则的左部表达式为β基）(x.E)E0E[E0/x]变换：假设x.Mx是一个表达式，且满足条件xFV(M)，则称下面变换为η变换:(x.Mx)M2021/7/2810关于Lambda演算自由变量（计算一个表达式的自由变量集合）表达式E中变量名x的一次出现称为自由出现，如果E中任何一个形如x.E

7、’的子表达式包含该出现；y(xy.y(x.xy))(z(x.xx))的自由变量集合{y,z}替换（计算）设E和E0是表达式，x是变量名，替换E[E0/x]是表示把E中的所有x的自由出现替换成E0。需要明确变量的自由出现计算规则(y.x+y)[y/x]=z.y+z2021/7/2811关于Lambda演算范式（性质及其计算）假设E是一个表达式，且其中没有任何一个归约基，则称该表达式为范式。范式的存在性：如果有范式，则最左归约法一定能求出范式。范式的唯一性：如果有范式则在变换下一定唯一。2021/7/2812函数式描述方法2021/7/2813关于函数式描述

8、方法函数式语言的特点引用透明性；高阶性；模式匹配；并行性；函数式语言的组成部分程序结构类型及其操作表达式用函数式语言来描述算法（解释器）函数空间函数定义（方程）2021/7/2814关于函数式描述方法函数式语言的组成部分程序结构函数定义目标表达式类型及其操作标准类型-集合类型幂集类型-元组类型联合类型-序列类型函数类型-递归类型抽象类型2021/7/2815关于函数式描述方法函数式语言的组成部分表达式非let表达式（常量，变量，表达式，条件表达式，以及各种操作）let表达式letx=E’inEletrec表达式letrecx=E1inE在表达式中增加类型说明202

9、1/7/2816关于函数式描述方法用函数式语言来描述算法函数空间：INT*INTBOOL函数定义（方程）lookupLa=(nullL→FALSE，a=hdL→TRUE，lookup(tlL)a)2021/7/2817操作语义学2021/7/28182021/7/2819操作语义学三种方法解释器方法抽象机归约方法（归约系统）从实现的角度，通过程序的执行过程来定义程序设计语言的语义；2021/7/2820操作语义学抽象机方法2021/7/2821主要思想：针对计算机语言，定义一个抽象机来解释执行将该语言的程序；抽象机的定义包括两个部分：抽象机组成的抽象定义–状态

10、结构执行机制的形式定义--状态转换规则针对如下语言结构给出抽象机定义表达式语句输入输出声明Block过程/函数2021/7/2822状态结构（形式定义）栈（保存中间计算结果）语句控制区表达式控制区静态环境区动态环境去堆区（保存中断现场）初始状态和终止状态状态转换规则针对每个语法结构给出执行过程状态到状态的映射基于抽象机的操作语义的定义过程2021/7/2823操作语义学归约方法2021/7/2824归约方法的主要思想：一种结构化方法（只依赖于成分的结果）根据语言的成分给出归约系统的方法归约系统是由以下部分组成的：一组归约公理一组推理规则，称为归约规则归约的对象