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

1、2018/9/27,1,形式语义学Formal Semantics,本PPT参考了金英老师的课程内容,2018/9/27,2,2018/9/27,3,代数语义学,理论基础,函数式描述方法,程序设计语言形式语义,指称语义学,操作语义学,公理语义学,代数,功能,执行,逻辑 关系,模型,2018/9/27,4,离散数学,程序设计语言形式语义,编译原理,程序设计语言,理论基础,语义形式化,语法形式化,2018/9/27,5,软件开发方法,程序设计语言形式语义,程序设计方法,程序设计语言理解,抽象能力,Formal Method,Formal Specification,Formal Verificat

2、ion,2018/9/27,6,前言：“形式语义学”概述,What？形式语义学：给出对(形式)语言及其程序采用形式系统方法进行语义定义的方法。分类：从不同的角度研究程序的含义操作语义学（执行）指称语义学（功能）公理语义学（逻辑）代数语义学（代数，抽象数据结构）其他,2018/9/27,7,Lambda演算,2018/9/27,8,关于Lambda演算,表达式自由变量（计算一个表达式的自由变量集合） 替换（计算） 变换规则 （三种变换）归约 范式（性质及其计算）,2018/9/27,9,关于Lambda演算,表达式 一个表达式由变量名、抽象符号，.以及括号等符号构成， 其语法为： := | |

3、. | ( ),2018/9/27,10,关于Lambda演算,变换规则 （三种变换）变换：设E是表达式，x是变量，则称下面变换为变换（其中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,2018/9/27,11,关于Lambda演算,自由变量（计算一个表达式的自由变量集合） 表达式E中变量名x的一次出现称为自由出现，如果E中任何一个形如x. E的子表达式包含该出现；y (x

4、 y. y (x. x y ) ) (z (x. x x) )的自由变量集合y, z替换（计算） 设E和E0是表达式，x是变量名，替换EE0/x是表示 把E中的所有x的自由出现替换成E0。需要明确变量的自由出现计算规则( y. x+y) y/x = z. y+z,2018/9/27,12,关于Lambda演算,范式（性质及其计算）假设E是一个表达式，且其中没有任何一个归约基，则称该表达式为范式。范式的存在性：如果有范式，则最左归约法一定能求出范式。范式的唯一性：如果有范式则在变换下一定唯一。,2018/9/27,13,函数式描述方法,2018/9/27,14,关于函数式描述方法,函数式语言的特

5、点引用透明性；高阶性；模式匹配；并行性；函数式语言的组成部分程序结构类型及其操作表达式用函数式语言来描述算法（解释器）函数空间函数定义（方程）,2018/9/27,15,关于函数式描述方法,函数式语言的组成部分程序结构函数定义目标表达式类型及其操作标准类型 - 集合类型幂集类型 - 元组类型联合类型 - 序列类型函数类型 - 递归类型抽象类型,2018/9/27,16,关于函数式描述方法,函数式语言的组成部分表达式非let表达式（常量，变量，表达式，条件表达式，以及各种操作） let表达式 let x = E in E letrec表达式 letrec x = E1 in E在表达式中增加类型

6、说明,2018/9/27,17,关于函数式描述方法,用函数式语言来描述算法函数空间：INT* INT BOOL函数定义（方程） lookup L a = (null LFALSE， a=hd LTRUE，lookup (tl L) a ),2018/9/27,18,操作语义学,2018/9/27,19,2018/9/27,20,操作语义学,三种方法解释器方法抽象机归约方法（归约系统）从实现的角度，通过程序的执行过程来定义程序设计语言的语义；,2018/9/27,21,操作语义学抽象机方法,2018/9/27,22,主要思想：针对计算机语言，定义一个抽象机来解释执行将该语言的程序；抽象机的定义包

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

8、则，称为归约规则归约的对象为格局（configuration），归约的结果也是格局；初始格局和终止格局；,2018/9/27,26,基于归约方法的操作语义的定义过程,格局的形式：，通过模式给出初始格局和终止格局一组归约公理：configure1 configure2 一组归约规则形： A1,An 条件公理configure1 configure2 推导出的公理其中A1,An是关于configure1中成分的公理，而configure2中的成分只能从configure1和A1,An中的结果格局中得到；,2018/9/27,27,2018/9/27,28,2018/9/27,29,2018/9/2

9、7,30,2018/9/27,31,2018/9/27,32,指称语义学,2018/9/27,33,2018/9/27,34,指称语义学,直接指称语义两个方面定义指称语义（五个部分）完整语言 某个语法单位给出具体语法元素的指称语义解释（语义函数）根据该语法元素所属的语法域的具体的语义指派函数；确定已知条件（静态环境，动态环境）给出语义解释（函数；值）,2018/9/27,35,直接指称语义,主要原理：从功能角度出发，对每一个语法单位（如程序、声明、语句、表达式、变量、整数、标识符等），给出其功能的严格形式化描述，即定义功能函数；功能函数是描述一个语法单位的语义，因此称为语义函数（语义物）；本质

10、上是建立语法域到语义函数域的映射；,语义指派函数,2018/9/27,36,直接指称语义,直接指称语义的定义包括：语法域 （Syntax Domain）抽象语法 （Abstract Syntax）语义域 （Semantic Domain）语义函数 （Semantic Functions）预定义函数 （Predefined Functions）,关键：掌握好每个语法单位的功能；语言不一样，相同的语法单位其语义也不尽相同；,2018/9/27,37,过程式语言的直接指称语义,语法域（根据语言定义应给出具体定义）程序声明（还可以细化）语句Block表达式常量类型,2018/9/27,38,过程式语言

11、的直接指称语义,语义域（根据语言定义应给出具体定义）环境域 静态环境动态环境值域存储域,2018/9/27,39,过程式语言的直接指称语义,语义函数针对每个语法单位语义指派函数空间针对每个语法单位定义语义指派函数针对每个语法单位中的每种语法元素，定义相应的语义方程,2018/9/27,40,公理语义学,2018/9/27,41,主要思想公理语义学是基于谓词逻辑中的逻辑归纳方法，一个程序的语义是建立在每次程序运行时都成立的关于变量的值之间关系的断言；定义过程为计算机语言建立一个公理系统公理系统由两部分组成：（1）一组公理；（2）一组推理规则局限性,2018/9/27,42,2018/9/27,4

12、3,2018/9/27,44,2018/9/27,45,2018/9/27,46,2018/9/27,47,Hoare 公理系统,2018/9/27,48,公理和命题的形式： P S Q 推理规则的形式 Hoare公理系统由五条规则赋值公理复合推理规则条件推理规则循环推理规则推论规则,2018/9/27,49,最弱前置条件和最强后置条件,2018/9/27,50,最弱前置条件的计算规则,求WP(S,q)WP(skip,q) = 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

13、WP(s2,q) 为什么没有给出while语句的WP求法？比较复杂,2018/9/27,51,最强后置条件的计算规则,求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),2018/9/27,52,程序正确性证明,2018/9/27,53,程序正确性证明,程序正确性证明目的证明验证公式pSq成立p是程序的前提条件（初始条件）q是程序结束时应满足的条件（目标条件）采用的方法 （应用Hoare公理系统，SP，WP）ForwardBackwardMeet in the middle难点:循环不变式,2018/9/27,54,求循环不变式过程,步骤：从循环语句出发，手工找出一些循环不变式；然后将它们合取，从而构造出更强的循环不变式；检查强度，直至找到合适的循环不变式；,