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

2023/9/181形式语义学

FormalSemantics本PPT参考了金英老师的课程内容2023/8/61形式语义学

FormalSemantic2023/9/1822023/8/622023/9/183代数语义学理论基础函数式描述方法程序设计语言形式语义指称语义学操作语义学公理语义学代数功能执行逻辑

关系模型2023/8/63代数语义学理论基础函数式描述方法程序设计语2023/9/184离散数学程序设计语言形式语义编译原理程序设计语言理论基础语义形式化语法形式化2023/8/64离散数学程序设计语言编译原理程序设计语言理2023/9/185软件开发方法程序设计语言形式语义程序设计方法程序设计语言理解抽象能力FormalMethodFormalSpecificationFormalVerification2023/8/65软件开发方法程序设计语言程序设计方法程序设2023/9/186前言：“形式语义学”概述What？形式语义学：给出对(形式)语言及其程序采用形式系统方法进行语义定义的方法。分类：从不同的角度研究程序的含义操作语义学（执行）指称语义学（功能）公理语义学（逻辑）代数语义学（代数，抽象数据结构）其他2023/8/66前言：“形式语义学”概述What？2023/9/187Lambda演算2023/8/67Lambda演算2023/9/188关于Lambda演算

表达式自由变量（计算一个表达式的自由变量集合）替换（计算）变换规则（三种变换）归约范式（性质及其计算）2023/8/68关于Lambda演算表达式2023/9/189关于Lambda演算

表达式

一个表达式由变量名、抽象符号，.以及括号等符号构成，其语法为：

<表达式>::=<变量名> |<表达式><表达式>|<变量名>.<表达式>|(<表达式>)2023/8/69关于Lambda演算表达式2023/9/1810关于Lambda演算变换规则（三种变换）变换：设E是表达式，x是变量，则称下面变换为α变换（其中y不在FV(x.E)中）

x.E------〉y.[y/x]E

变换：设(x.E)和E0为表达式，则称下面变换为β变换（称β变换规则的左部表达式为β基）

(x.E)E0E[E0/x]

变换：假设x.Mx是一个表达式，且满足条件xFV(M)，则称下面变换为η变换:(x.Mx)M

2023/8/610关于Lambda演算变换规则（三种变换2023/9/1811关于Lambda演算自由变量（计算一个表达式的自由变量集合）表达式E中变量名x的一次出现称为自由出现，如果E中任何一个形如x.E’的子表达式包含该出现；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+z2023/8/611关于Lambda演算自由变量（计算一个2023/9/1812关于Lambda演算范式（性质及其计算）假设E是一个表达式，且其中没有任何一个归约基，则称该表达式为范式。范式的存在性：如果有范式，则最左归约法一定能求出范式。范式的唯一性：如果有范式则在变换下一定唯一。2023/8/612关于Lambda演算范式（性质及其计算）2023/9/1813函数式描述方法2023/8/613函数式描述方法2023/9/1814关于函数式描述方法函数式语言的特点引用透明性；高阶性；模式匹配；并行性；函数式语言的组成部分程序结构类型及其操作表达式用函数式语言来描述算法（解释器）函数空间函数定义（方程）2023/8/614关于函数式描述方法函数式语言的特点2023/9/1815关于函数式描述方法函数式语言的组成部分程序结构函数定义目标表达式类型及其操作标准类型-集合类型幂集类型-元组类型联合类型-序列类型函数类型-递归类型抽象类型2023/8/615关于函数式描述方法函数式语言的组成部分2023/9/1816关于函数式描述方法函数式语言的组成部分表达式非let表达式（常量，变量，表达式，条件表达式，以及各种操作）let表达式

letx=E’

inEletrec表达式

letrecx=E1

inE在表达式中增加类型说明

2023/8/616关于函数式描述方法函数式语言的组成部分2023/9/1817关于函数式描述方法用函数式语言来描述算法函数空间：INT*INTBOOL函数定义（方程）

lookupLa=(nullL→FALSE，

a=hdL→TRUE，lookup(tlL)a)2023/8/617关于函数式描述方法用函数式语言来描述算法2023/9/1818操作语义学2023/8/618操作语义学2023/9/18192023/8/6192023/9/1820操作语义学三种方法解释器方法抽象机归约方法（归约系统）从实现的角度，通过程序的执行过程来定义程序设计语言的语义；2023/8/620操作语义学三种方法2023/9/1821操作语义学

抽象机方法2023/8/621操作语义学

抽象机方法2023/9/1822主要思想：针对计算机语言，定义一个抽象机来解释执行将该语言的程序；抽象机的定义包括两个部分：抽象机组成的抽象定义–状态结构执行机制的形式定义--状态转换规则针对如下语言结构给出抽象机定义表达式语句输入输出声明Block过程/函数2023/8/622主要思想：2023/9/1823状态结构（形式定义）栈（保存中间计算结果）语句控制区表达式控制区静态环境区动态环境去堆区（保存中断现场）初始状态和终止状态状态转换规则针对每个语法结构给出执行过程状态到状态的映射基于抽象机的操作语义的定义过程2023/8/623状态结构（形式定义）基于抽象机的操作语义2023/9/1824操作语义学

归约方法2023/8/624操作语义学

归约方法2023/9/1825归约方法的主要思想：一种结构化方法（只依赖于成分的结果）根据语言的成分给出归约系统的方法归约系统是由以下部分组成的：一组归约公理一组推理规则，称为归约规则归约的对象为格局（configuration），归约的结果也是格局；初始格局和终止格局；2023/8/625归约方法的主要思想：2023/9/1826基于归约方法的操作语义的定义过程格局的形式：<comp1,…,compn>，通过模式给出初始格局和终止格局一组归约公理：

configure1

configure2

一组归约规则形：

A1,……,An

条件公理

configure1

configure2推导出的公理 其中A1,……,An是关于configure1中成分的公理，而configure2中的成分只能从configure1和A1,……,An中的结果格局中得到；2023/8/626基于归约方法的操作语义的定义过程格局的形2023/9/18272023/8/6272023/9/18282023/8/6282023/9/18292023/8/6292023/9/18302023/8/6302023/9/18312023/8/6312023/9/1832指称语义学2023/8/632指称语义学2023/9/18332023/8/6332023/9/1834指称语义学直接指称语义两个方面定义指称语义（五个部分）完整语言某个语法单位给出具体语法元素的指称语义解释（语义函数）根据该语法元素所属的语法域的具体的语义指派函数；确定已知条件（静态环境，动态环境）给出语义解释（函数；值……）2023/8/634指称语义学直接指称语义2023/9/1835直接指称语义主要原理：从功能角度出发，对每一个语法单位（如程序、声明、语句、表达式、变量、整数、标识符等），给出其功能的严格形式化描述，即定义功能函数；功能函数是描述一个语法单位的语义，因此称为语义函数（语义物）；本质上是建立语法域到语义函数域的映射；语法域语义函数域语义指派函数2023/8/635直接指称语义主要原理：语法域语义函数域语2023/9/1836直接指称语义直接指称语义的定义包括：语法域（SyntaxDomain）抽象语法（AbstractSyntax）语义域（SemanticDomain）语义函数（SemanticFunctions）预定义函数（PredefinedFunctions）关键：掌握好每个语法单位的功能；语言不一样，相同的语法单位其语义也不尽相同；2023/8/636直接指称语义直接指称语义的定义包括：关键2023/9/1837过程式语言的直接指称语义语法域（根据语言定义应给出具体定义）程序声明（还可以细化）语句Block表达式常量类型2023/8/637过程式语言的直接指称语义语法域（根据语言2023/9/1838过程式语言的直接指称语义语义域（根据语言定义应给出具体定义）环境域静态环境动态环境值域存储域2023/8/638过程式语言的直接指称语义语义域（根据语言2023/9/1839过程式语言的直接指称语义语义函数针对每个语法单位语义指派函数空间针对每个语法单位定义语义指派函数针对每个语法单位中的每种语法元素，定义相应的语义方程2023/8/639过程式语言的直接指称语义语义函数2023/9/1840公理语义学2023/8/640公理语义学2023/9/1841主要思想公理语义学是基于谓词逻辑中的逻辑归纳方法，一个程序的语义是建立在每次程序运行时都成立的关于变量的值之间关系的断言；定义过程为计算机语言建立一个公理系统公理系统由两部分组成：（1）一组公理；（2）一组推理规则局限性2023/8/641主要思想2023/9/18422023/8/6422023/9/18432023/8/6432023/9/18442023/8/6442023/9/18452023/8/6452023/9/18462023/8/6462023/9/1847Hoare公理系统2023/8/647Hoare公理系统2023/9/1848公理和命题的形式：{P}S{Q}推理规则的形式

Hoare公理系统由五条规则赋值公理复合推理规则条件推理规则循环推理规则推论规则F1，……,FnF2023/8/648公理和命题的形式：{P}S{2023/9/1849最弱前置条件和最强后置条件2023/8/649最弱前置条件和最强后置条件2023/9/1850最弱前置条件的计算规则求WP(S,q)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)=(eWP(s1,q))

(

eWP(s