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

1、2022-12-211本PPT参考了金英老师的课程内容2022-12-2122022-12-213代数语义学代数语义学理论基础理论基础函数式描述方法函数式描述方法程序设计语言程序设计语言形式语义形式语义指称语义学指称语义学操作语义学操作语义学公理语义学公理语义学代数代数功能功能执行执行逻辑逻辑 关系关系模型模型2022-12-214离散数学离散数学程序设计语言程序设计语言形式语义形式语义编译原理编译原理程序设计语言程序设计语言理论理论基础基础语义形式化语义形式化语法形式化语法形式化2022-12-215软件开发方法软件开发方法程序设计语言程序设计语言形式语义形式语义程序设计方法程序设计方法程序

2、设计语言理解程序设计语言理解抽象能力抽象能力Formal MethodFormal SpecificationFormal Verification2022-12-216lWhatWhat？形式语义学：给出对形式语义学：给出对(形式形式)语言及其程序采语言及其程序采用用形式系统方法形式系统方法进行语义定义的方法。进行语义定义的方法。l分类：分类：从不同的角度研究程序的含义从不同的角度研究程序的含义操作语义学操作语义学（执行）执行）指称语义学指称语义学（功能）（功能）公理语义学公理语义学（逻辑）（逻辑）代数语义学代数语义学（代数，抽象数据结构（代数，抽象数据结构）其他其他2022-12-2172

3、022-12-218l 表达式表达式l自由变量（计算一个自由变量（计算一个 表达式的自由变量表达式的自由变量集合集合）l替换（计算）替换（计算）l变换规则变换规则 （三种变换）（三种变换）l归约归约 l范式（性质及其计算）范式（性质及其计算）2022-12-219l 表达式表达式 一个一个 表达式表达式由变量名、抽象符号由变量名、抽象符号，.以及括号等符以及括号等符号构成，号构成，其语法为：其语法为：:=|.|()2022-12-2110l变换规则变换规则 （三种变换）（三种变换）l 变换：设变换：设E是是 表达式，表达式，x是变量，则称下面变换为是变量，则称下面变换为变换变换（其中（其中y不

4、在不在 FV(x.E)中）中）x.E-y.y/x E l 变换：设变换：设(x.E)和和E0为为 表达式，则称下面变换为表达式，则称下面变换为变换变换（称（称变换规则的左部表达式为变换规则的左部表达式为基）基）(x.E)E0 EE0/xl 变换：假设变换：假设 x.Mx是一个表达式，且满足条件是一个表达式，且满足条件x FV(M)，则称下面变换为则称下面变换为变换变换:(x.M x)M 2022-12-2111l自由变量（计算一个自由变量（计算一个 表达式的自由变量集合表达式的自由变量集合）l表达式表达式E中变量名中变量名x的一次出现称为的一次出现称为自由出现自由出现，如果，如果E中任何一个形

5、如中任何一个形如 x.E的子表达式包含该出现；的子表达式包含该出现；ly(x y.y(x.x y)(z(x.x x)的自由变量集合的自由变量集合y,zl替换（计算）替换（计算）设设E和和E0是表达式，是表达式，x是变量名，是变量名，替换替换EE0/x是表示是表示 把把E中的所有中的所有x的自由出现替换成的自由出现替换成E0。l需要明确变量的自由出现需要明确变量的自由出现l计算规则计算规则l(y.x+y)y/x=z.y+z2022-12-2112l范式（性质及其计算）范式（性质及其计算）l假设假设E是一个表达式，且其中没有任何一个是一个表达式，且其中没有任何一个归约基，则称该表达式为归约基，则称

6、该表达式为范式范式。l范式范式的存在性：如的存在性：如果有范式，则最左归约法果有范式，则最左归约法一定能求出范式。一定能求出范式。l范式范式的唯一性：如的唯一性：如果有范式则在果有范式则在 变换下一变换下一定唯一。定唯一。2022-12-2113函数式描述方法函数式描述方法2022-12-2114l函数式语言的特点函数式语言的特点引用透明性；高阶性；模式匹配；并行性；引用透明性；高阶性；模式匹配；并行性；l函数式语言的组成部分函数式语言的组成部分程序结构程序结构类型及其操作类型及其操作表达式表达式l用函数式语言来描述算法（解释器）用函数式语言来描述算法（解释器）函数空间函数空间函数定义（方程）

7、函数定义（方程）2022-12-2115l函数式语言的组成部分函数式语言的组成部分程序结构程序结构l函数定义函数定义l目标表达式目标表达式类型及其操作类型及其操作 标准类型标准类型 -集合类型集合类型 幂集类型幂集类型 -元组类型元组类型 联合类型联合类型 -序列类型序列类型 函数类型函数类型 -递归类型递归类型 抽象类型抽象类型2022-12-2116l函数式语言的组成部分函数式语言的组成部分表达式表达式l非非letlet表达式（常量，变量，表达式（常量，变量，表达式，条件表达表达式，条件表达式，式，以及各种操作）以及各种操作）lletlet表达式表达式 letlet x=E x=E ini

8、n E E lletrecletrec表达式表达式 letrecletrec x=E x=E1 1 inin E El在表达式中增加类型说明在表达式中增加类型说明 2022-12-2117l用函数式语言来描述算法用函数式语言来描述算法函数空间：函数空间：INT*INT BOOL函数定义（方程）函数定义（方程）lookup L a=(null LFALSE，a=hd LTRUE，lookup(tl L)a)2022-12-21182022-12-21192022-12-2120l三种方法三种方法解释器方法解释器方法抽象机抽象机归约方法（归约系统）归约方法（归约系统）l从实现的角度，通过程序的执行

9、过程来定义从实现的角度，通过程序的执行过程来定义程序设计语言的语义；程序设计语言的语义；2022-12-21212022-12-2122l主要思想：主要思想：针对计算机语言，定义一个抽象机来解释执行将该语言的针对计算机语言，定义一个抽象机来解释执行将该语言的程序；程序；l抽象机的定义包括两个部分：抽象机的定义包括两个部分：抽象机组成的抽象定义抽象机组成的抽象定义 状态结构状态结构执行机制的形式定义执行机制的形式定义-状态转换规则状态转换规则l针对如下语言结构给出抽象机定义针对如下语言结构给出抽象机定义表达式表达式语句语句输入输出输入输出声明声明Block过程过程/函数函数2022-12-212

10、3l状态结构（形式定义）状态结构（形式定义）栈（保存中间计算结果）栈（保存中间计算结果）语句控制区语句控制区表达式控制区表达式控制区静态环境区静态环境区动态环境去动态环境去堆区（保存中断现场）堆区（保存中断现场）l初始状态和终止状态初始状态和终止状态l状态转换规则状态转换规则针对每个语法结构给出执行过程针对每个语法结构给出执行过程状态到状态的映射状态到状态的映射2022-12-21242022-12-2125l归约方法的主要思想：归约方法的主要思想：一种一种结构化结构化方法（只依赖于成分的结果）方法（只依赖于成分的结果）根据语言的成分给出归约系统的方法根据语言的成分给出归约系统的方法l归约系统

11、是由以下部分组成的：归约系统是由以下部分组成的：一组一组归约公理归约公理一组一组推理规则推理规则，称为，称为归约规则归约规则l归约的对象为归约的对象为格局格局（configurationconfiguration），归约），归约的结果也是格局；的结果也是格局；l初始格局和终止格局；初始格局和终止格局；2022-12-2126l格局的形式格局的形式：comp，通过模式给出，通过模式给出l初始格局和终止格局初始格局和终止格局l一组归约公理一组归约公理：configureconfigure1 1 configureconfigure2 2 l一组归约规则一组归约规则形：形：A A1 1,A An n

12、 条件公理条件公理configureconfigure1 1 configureconfigure2 2 推导出的公理推导出的公理其中其中A A1 1,A An n是关于是关于configureconfigure1 1中成分的公理，而中成分的公理，而configureconfigure2 2中的成分只能从中的成分只能从configureconfigure1 1和和A A1 1,A An n中的结果格局中得到；中的结果格局中得到；2022-12-21272022-12-21282022-12-21292022-12-21302022-12-21312022-12-21322022-12-2133

13、2022-12-2134l直接指称语义直接指称语义l两个方面两个方面定义指称语义（五个部分）定义指称语义（五个部分）l完整语言完整语言 l某个语法单位某个语法单位给出具体语法元素的指称语义解释（语义函数）给出具体语法元素的指称语义解释（语义函数）l根据该语法元素所属的语法域的具体的语义指派函数；根据该语法元素所属的语法域的具体的语义指派函数；l确定已知条件（静态环境，动态环境）确定已知条件（静态环境，动态环境）l给出语义解释（函数；值给出语义解释（函数；值）2022-12-2135l主要原理：主要原理：从从功能功能角度出发，对每一个角度出发，对每一个语法单位语法单位（如程序、声明、语（如程序、

14、声明、语句、表达式、变量、整数、标识符等），给出其功能的严句、表达式、变量、整数、标识符等），给出其功能的严格形式化描述，即定义格形式化描述，即定义功能函数功能函数；功能函数功能函数是描述一个语法单位的语义，因此称为是描述一个语法单位的语义，因此称为语义函数语义函数（语义物）（语义物）；本质上是建立本质上是建立语法域语法域到到语义函数域语义函数域的映射；的映射；语法域语法域语义函数域语义函数域语义指派函数语义指派函数2022-12-2136l直接指称语义的定义包括：直接指称语义的定义包括：语法域语法域 （Syntax Domain）抽象语法抽象语法（Abstract Syntax）语义域语义域

15、 （Semantic Domain）语义函数语义函数（Semantic Functions）预定义函数预定义函数（Predefined Functions）l关键：掌握好每个语法单位的功能；关键：掌握好每个语法单位的功能；l语言不一样，相同的语法单位其语义也不尽相同；语言不一样，相同的语法单位其语义也不尽相同；2022-12-2137l语法域（根据语言定义应给出具体定义）语法域（根据语言定义应给出具体定义）程序程序声明（还可以细化）声明（还可以细化）语句语句Block表达式表达式常量常量类型类型2022-12-2138l语义域（根据语言定义应给出具体定义）语义域（根据语言定义应给出具体定义）环

16、境域环境域 l静态环境静态环境l动态环境动态环境值域值域存储域存储域2022-12-2139l语义函数语义函数针对每个语法单位语义指派函数空间针对每个语法单位语义指派函数空间针对每个语法单位定义语义指派函数针对每个语法单位定义语义指派函数l针对每个语法单位中的每种语法元素，定义相应的针对每个语法单位中的每种语法元素，定义相应的语义方程语义方程2022-12-21402022-12-2141l主要思想主要思想公理语义学公理语义学是基于谓词逻辑中的逻辑归纳方法，是基于谓词逻辑中的逻辑归纳方法，一个程序的语义是建立在每次程序运行时都成一个程序的语义是建立在每次程序运行时都成立的关于变量的值之间关系的

17、断言；立的关于变量的值之间关系的断言；l定义过程定义过程为计算机语言建立一个公理系统公理系统由两为计算机语言建立一个公理系统公理系统由两部分组成：部分组成：（1）一组公理；（）一组公理；（2）一组推理规则）一组推理规则l局限性局限性2022-12-21422022-12-21432022-12-21442022-12-21452022-12-21462022-12-21472022-12-2148l公理和命题的形式：公理和命题的形式：P S Q l推理规则的形式推理规则的形式 lHoare公理系统由五条规则公理系统由五条规则赋值公理赋值公理复合推理规则复合推理规则条件推理规则条件推理规则循环推

18、理规则循环推理规则推论规则推论规则F1，,FnF2022-12-21492022-12-2150l求求WP(S,q)WP(S,q)WP(skip,q)=q;WP(skip,q)=q;WP(x:=e,q)=qe/x;WP(x:=e,q)=qe/x;WP(s1;s2,q)=WP(s1,WP(s2,q);WP(s1;s2,q)=WP(s1,WP(s2,q);WP(if(e,s1,s2),q)=WP(if(e,s1,s2),q)=(e (e WP(s1,q)WP(s1,q)(e e WP(s2,q)WP(s2,q)l为什么没有给出为什么没有给出whilewhile语句的语句的WPWP求法？求法？比较复

19、杂比较复杂2022-12-2151l求求SP(p,S)SP(p,S)SP(p,skip)=p;SP(p,skip)=p;SP(p,x:=e)=SP(p,x:=e)=x x(px(px/x/x x=ex x=ex/x)/x);SP(p,s1;s2)=SP(SP(s1,p),s2);SP(p,s1;s2)=SP(SP(s1,p),s2);SP(p,if(e,s1,s2)=SP(p,if(e,s1,s2)=(SP(p(SP(p e,e,s1)s1)SP(pSP(pe,e,s2)s2)2022-12-21522022-12-2153l程序正确性证明程序正确性证明目的目的l证明验证公式证明验证公式pSq

20、pSq成立成立lp p是程序的前提条件（初始条件）是程序的前提条件（初始条件）lq q是程序结束时应满足的条件（目标条件）是程序结束时应满足的条件（目标条件）采用的方法采用的方法 （应用（应用HoareHoare公理系统，公理系统，SPSP，WPWP）lForwardForwardlBackwardBackwardlMeet in the middleMeet in the middle难点难点:循环不变式循环不变式2022-12-2154l步骤：步骤：从循环语句出发，手工找出一些循环不变式；从循环语句出发，手工找出一些循环不变式；然后将它们合取，从而构造出更强的循环不然后将它们合取，从而构造出更强的循环不变式；变式；检查强度，直至找到合适的循环不变式；检查强度，直至找到合适的循环不变式；