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

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 指称语义学 * * * * 指称语义学 直接指称语义 两个方面 定义指称语义（五个部分） 完整语言 某个语法单位 给出具体语法元素的指称语义解释（语义函数） 根据该语法元素所属的语法域的具体的语义指派函数； 确定已知条件（静态环境，动态环境） 给出语义解释（函数；值……） * * 直接指称语义 主要原理： 从功能角度出发，对每一个语法单位（如程序、声明、语句、表达式、变量、整数、标识符等），给出其功能的严格形式化描述，即定义功能函数； 功能函数是描述一个语法单位的语义，因此称为语义函数（语义物）； 本质上是建立语法域到语义函数域的映射； 语法域 语义函数域 语义指派函数 * * 直接指称语义 直接指称语义的定义包括： 语法域 （Syntax Domain） 抽象语法 （Abstract Syntax） 语义域 （Semantic Domain） 语义函数 （Semantic Functions） 预定义函数 （Predefined Functions） 关键：掌握好每个语法单位的功能； 语言不一样，相同的语法单位其语义也不尽相同； * * 过程式语言的直接指称语义 语法域（根据语言定义应给出具体定义） 程序 声明（还可以细化） 语句 Block 表达式 常量 类型 * * 过程式语言的直接指称语义 语义域（根据语言定义应给出具体定义） 环境域 静态环境 动态环境 值域 存储域 * * 过程式语言的直接指称语义 语义函数 针对每个语法单位语义指派函数空间 针对每个语法单位定义语义指派函数 针对每个语法单位中的每种语法元素，定义相应的语义方程 * * 公理语义学 * * 主要思想 公理语义学是基于谓词逻辑中的逻辑归纳方法，一个程序的语义是建立在每次程序运行时都成立的关于变量的值之间关系的断言； 定义过程 为计算机语言建立一个公理系统公理系统由两部分组成： （1）一组公理；（2）一组推理规则 局限性 * * * * * * * * * * * * Hoare 公理系统 * * 公理和命题的形式：{ P } S { Q } 推理规则的形式 Hoare公理系统由五条规则 赋值公理 复合推理规则 条件推理规则 循环推理规则 推论规则 F1，…… , Fn F * * 最弱前置条件和最强后置条件 * * 最弱前置条件的计算规则 求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) = (e ? WP(s1,q)) ? (?e ? WP(s2,q)) 为什么没有给出while语句的WP求法？ 比较复杂 * * 最强后置条件的计算规则 求SP(p,S) SP(p,skip) = p; SP(p,x:=e) = ?x’(p[x’/x] ? x=e[x’/x]); SP(p,s1;s2) = SP(SP(s1,p),s2); SP(p,if(e,s1,s2)) = (SP(p?e,s1) ? SP(p??e,s2)) * * 程序正确性证明 * * 程序正确性证明 程序正确性证明 目的 证明验证公式{p}S{q}成立 p是程序的前提条件（初始条件） q是程序结束时应满足的条件（目标条件） 采用的方法 （应用Hoare公理系统，SP，WP） Forward Backward Meet in the middle 难点:循环不变式 * * 求循环不变式过程 步骤： 从循环语句出发，手工找出一些循环不变式； 然后将它们合取，从而构造出更强的循环不变式； 检查强度，直至找到合适的循环不变式； * * * * * * * * * * 形式语义学Formal Semantics 本PPT参考了金英老师的课程内容 * * * * 代数语义学 理论基础 函数式描述方法 程序设计语言 形式语义 指称语义学 操作语义学 公理语义学 代数 功能 执行 逻辑 关系 模型 * * 离散数学 程序设计语言 形式语义 编译原理 程序设计语言 理论基础 语义形式化 语法形式化 * * 软件开发方法 程序设计语言 形式语义 程序设计方法 程序设计语言理解 抽象能力 Formal Method Formal Specification Formal Verification * * 前言：“形式语义学”概述 What？ 形式语义学：给出对(形式)语言及其程序采用形式系统方法进行语