《程序设计方法学》PPT课件.ppt

《《程序设计方法学》PPT课件.ppt》由会员分享，可在线阅读，更多相关《《程序设计方法学》PPT课件.ppt（71页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、第六章第六章 程序设计的形式化方法程序设计的形式化方法 软件新技术软件新技术智能化技术智能化技术扩大软件功能的关键途径扩大软件功能的关键途径自动化技术自动化技术提高软件生产率的根本途径提高软件生产率的根本途径集成化技术集成化技术助于提高生产率、提高质量助于提高生产率、提高质量并行化技术并行化技术提高系统实效的关键技术提高系统实效的关键技术自然化技术自然化技术实现社会信息化实现社会信息化10/26/20221重要方向重要方向攻克的关键教技术攻克的关键教技术网络体系网络体系传感器网与因特网的高效融合传感器网与因特网的高效融合集成芯片集成芯片从从Systemonchip到到Chipondemount

2、虚拟计算虚拟计算资源聚合的有效性和可靠性验证资源聚合的有效性和可靠性验证软件工程软件工程基于网络环境的需求工程基于网络环境的需求工程知识处理知识处理挖掘从消息到知识到决策的元知识挖掘从消息到知识到决策的元知识高效系统高效系统在高性（效）能计算系统中系列关注在高性（效）能计算系统中系列关注信息安全信息安全信息教育信息教育10/26/20222跨跨越越源源之之识识规规律律创创新新根根植植辨辨短短长长汪成为院士10/26/20223软件自动化的三个层次软件自动化的三个层次软件自动化（自动程序设计）软件自动化（自动程序设计）广义：尽可能地借助计算机系统实现软件开发广义：尽可能地借助计算机系统实现软件开

3、发狭义：从形式化的软件功能规范到可执行程序代码狭义：从形式化的软件功能规范到可执行程序代码 这一过程的自动化这一过程的自动化从软件需求规范从软件需求规范软件功能、性能规范的转换软件功能、性能规范的转换解决从解决从“非形式非形式”“形式形式”难度很大，寄希望于受限自然语言方面的突破难度很大，寄希望于受限自然语言方面的突破从软件功能、性能规范从软件功能、性能规范软件设计软件设计从从“做什么做什么”“如何做如何做“从软件设计规范从软件设计规范高级语言高级语言已有相当的进展，出现了许多工具已有相当的进展，出现了许多工具10/26/202241概述概述一、重要意义一、重要意义软件发展中的问题：软件发展中

4、的问题：整体功能不强、缺乏智能、质量欠佳、生产效整体功能不强、缺乏智能、质量欠佳、生产效率低率低软件自动化是提高软件生产率的根本途径软件自动化是提高软件生产率的根本途径软件自动化的前提是形式化软件自动化的前提是形式化因此将形式化的理论和方法用于需求分析与规格因此将形式化的理论和方法用于需求分析与规格说明是实现软件自动化的前提说明是实现软件自动化的前提10/26/20225二、发展状况二、发展状况有有30多年历史多年历史Dijkstra、Hoare程序验证程序验证Scott、Stratchey程序语义程序语义形式化方法形式化方法(FormalMethod)：通通过过严严格格的的规规范范化化的的数

5、数学学理理论论来来描描述述软软件件系系统统“做做什么什么”的方法。需要形式规范语言的支持。的方法。需要形式规范语言的支持。形式规范语言：形式规范语言：提提供供了了一一个个称称为为语语法法域域的的记记号号系系统统。一一个个称称为为语语义义域域的的目目标标集集合合，以以及及一一组组精精确确定定义义的的哪哪些些目目标标系系统统满足那个规范的规则。满足那个规范的规则。10/26/20226因此，形式化方法是在软件系统的开发过程中使用因此，形式化方法是在软件系统的开发过程中使用一种形式系统来表示模型的方法。一种形式系统来表示模型的方法。形式系统是二元组（形式系统是二元组（L，Cn）L：语言（形式规范语言

6、）：语言（形式规范语言）Cn：对应关系，由推理规则构成：对应关系，由推理规则构成在软件规范方法方面的代表性成果有：在软件规范方法方面的代表性成果有：基于异调代数的代数方法基于异调代数的代数方法 特点：用抽象代数中的公理化方法来刻画抽象数特点：用抽象代数中的公理化方法来刻画抽象数据据类类型型中中运运算算的的性性质质，而而不不涉涉及及数数据据的的具具体表示。体表示。基本理论：代数语义基本理论：代数语义10/26/20227抽象模型方法抽象模型方法特点：基于某些已知的特点：基于某些已知的ADT来给出待定义的来给出待定义的ADT的抽象模型，用抽象模型来刻画待的抽象模型，用抽象模型来刻画待定义的定义的A

7、DT中运算的功能。中运算的功能。基本理论：指称语义基本理论：指称语义状态机方法状态机方法特点：通过状态的转换来刻画输入与输出间的特点：通过状态的转换来刻画输入与输出间的关系关系基本理论：操作语义基本理论：操作语义高阶软件方法（高阶软件方法（HOS）基于控制公理基于控制公理基本理论：公理语义基本理论：公理语义10/26/20228在软件规范语言方面的代表性成果有：在软件规范语言方面的代表性成果有：一阶谓词演算组成语言一阶谓词演算组成语言 80年代：年代：Z语言、语言、Larch语言、语言、VDM语言语言90年代：面向实时及分布式的年代：面向实时及分布式的LOTOS语言、语言、面向对象的面向对象的

8、Z+、Object-Z、VDM+等等三、分类三、分类基于模型的方法基于模型的方法 给给出出系系统统（程程序序）状状态态和和状状态态变变换换与与操操作作的的显显式式的的表示但亦是抽象的定义，不涉及并发的行为。表示但亦是抽象的定义，不涉及并发的行为。如：如：Z、VDM10/26/20229代数方法代数方法通通过过联联系系不不同同的的操操作作间间的的行行为为关关系系给给出出操操作作的的隐隐式定义，未给出并发的显式表示。式定义，未给出并发的显式表示。如：如：OBJ、Larch过程代数方法过程代数方法给给出出并并发发过过程程的的一一个个显显式式模模型型，并并通通过过过过程程间间允允许的可观察的通信上的限

9、制来约束表示行为。许的可观察的通信上的限制来约束表示行为。如：如：CSP（通信顺序进程）和（通信顺序进程）和CCS（通信系统计算）（通信系统计算）基于逻辑的方法基于逻辑的方法采采用用逻逻辑辑来来描描述述系系统统的的特特性性，包包括括程程序序行行为为的的低低级规范和系统时间的行为规范。级规范和系统时间的行为规范。如：时态逻辑、模态逻辑如：时态逻辑、模态逻辑10/26/202210基于网络的方法基于网络的方法根根据据网网络络中中的的数数据据流流显显式式地地给给出出系系统统的的并并发发模模型，包括数据从一个结点流向另一个结点的条件。型，包括数据从一个结点流向另一个结点的条件。如：如：Petri网、谓

10、词变换网网、谓词变换网10/26/202211四、形式化软件开发方法四、形式化软件开发方法采用软件生命周期的变换模型，其实质是将现实世界采用软件生命周期的变换模型，其实质是将现实世界的需求反映成软件的模型化过程。涉及三方面模型：的需求反映成软件的模型化过程。涉及三方面模型：现实世界，模型表示和计算机系统。因此开发的过程现实世界，模型表示和计算机系统。因此开发的过程就是从三方面对系统进行描述和转换的过程。就是从三方面对系统进行描述和转换的过程。开发过程中的任务为：开发过程中的任务为：(1)模型获取：从现实世界向模型表示的过程，涉及如何模型获取：从现实世界向模型表示的过程，涉及如何提取、表示模型。

11、对应需求分析、设计等活动。提取、表示模型。对应需求分析、设计等活动。(2)模型验证：对得到的模型表示进行检验，判断是否捕模型验证：对得到的模型表示进行检验，判断是否捕获了所有的需求，该模型是否具有所期望的特性。获了所有的需求，该模型是否具有所期望的特性。(3)模型变换：是向计算机系统变换的过程，模型变换：是向计算机系统变换的过程，关键的任关键的任务是一致性检测。对应实现和测试。务是一致性检测。对应实现和测试。10/26/202212三项任务分别对应三方面的活动：三项任务分别对应三方面的活动：1.形式化规范（规格）：形式化规范（规格）：软件规范是指对软件系统对象及用来对系统对软件规范是指对软件系

12、统对象及用来对系统对象进行操作的方法的集合。以及对所开发系统象进行操作的方法的集合。以及对所开发系统中的各对象在生命周期间的集体行为的描述。中的各对象在生命周期间的集体行为的描述。对应与软件生命周期的各个阶段，规范应该理对应与软件生命周期的各个阶段，规范应该理解为是一个多阶段的行为。见例图解为是一个多阶段的行为。见例图规范可以采用非、半形式化的方法来描述，形规范可以采用非、半形式化的方法来描述，形式化规范精确地描述了用户的需求、软件系统式化规范精确地描述了用户的需求、软件系统的功能及各种性质，其描述的是的功能及各种性质，其描述的是“做什么做什么”，而不考虑而不考虑“如何做如何做”。因此，在理解

13、、掌握形。因此，在理解、掌握形式规范语言和方法的基础上对所描述的系统的式规范语言和方法的基础上对所描述的系统的全面、深入的了解，给出恰如其分的描述上至全面、深入的了解，给出恰如其分的描述上至关重要的。关重要的。10/26/202213包含各规格阶段的生命周期模型例包含各规格阶段的生命周期模型例需求分析需求分析BSSRD系统设计系统设计1DS系统设计系统设计2PS软件开发软件开发代码实现代码实现软件测试软件测试运行运行SRD：软件需求文档：软件需求文档BS：行为规范：行为规范DS：设计规范：设计规范PS：程序规范：程序规范10/26/202214软件系统规范的形式化方法软件系统规范的形式化方法从

14、形式化规范到目标软件系统的可实现和可执行角从形式化规范到目标软件系统的可实现和可执行角度，可分为三类：度，可分为三类：(1)操作类：此类方法基于状态和转移，通过可执行操作类：此类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型来描述系统，模型本身能够采用静态分析和模型执行而得到验证。如：有限状态机、模型执行而得到验证。如：有限状态机、Statecharts、Petri网等。网等。(2)描述类：此类方法基于数学公理和概念，通过逻描述类：此类方法基于数学公理和概念，通过逻辑或代数给出系统状态空间，具有高度抽象的特辑或代数给出系统状态空间，具有高度抽象的特点，便于通过自动

15、工具进行验证。如：基于代数点，便于通过自动工具进行验证。如：基于代数的的Z、VDM、Larch等，基于逻辑的命题线性时态等，基于逻辑的命题线性时态逻辑、一阶线性时态逻辑、计算树逻辑等。逻辑、一阶线性时态逻辑、计算树逻辑等。(3)双重类：此类方法兼具二者的特点，如：扩展状双重类：此类方法兼具二者的特点，如：扩展状态机态机/实时时态逻辑等。实时时态逻辑等。10/26/202215形式化规范的成功案例形式化规范的成功案例IBM商用信息系统，牛津大学和商用信息系统，牛津大学和Hursley实验室使用实验室使用Z语言。总体成本降低语言。总体成本降低9，获皇家技术成就奖。，获皇家技术成就奖。Praxis公

16、司使用公司使用VDM开发的伦敦机场信息显示系统，开发的伦敦机场信息显示系统，软件质量大为提高，故障率软件质量大为提高，故障率0.75(220)每每K行代码。行代码。其他领域：其他领域：数据库：数据库：HP医用仪器实时数据库系统医用仪器实时数据库系统电子仪器：电子仪器：Tektronix系列谐波发生器系列谐波发生器硬件：硬件：INMOS浮点处理器、浮点处理器、INMOS中中T9000系列系列虚拟信道处理器虚拟信道处理器运输系统：巴黎地铁自动火车保护系统、以色列机运输系统：巴黎地铁自动火车保护系统、以色列机载航空电子软件等等载航空电子软件等等10/26/2022162.形式化验证形式化验证软件开发

17、中错误发现的越晚修改的代价越大，软件开发中错误发现的越晚修改的代价越大，与传统方法不同的是形式化方法要求在完成形与传统方法不同的是形式化方法要求在完成形式规范后就进行形式验证。式规范后就进行形式验证。形式验证主要技术包括模型检验和定理证明。形式验证主要技术包括模型检验和定理证明。(1)模型验证是一种基于有限状态机模型并检验该模模型验证是一种基于有限状态机模型并检验该模型的期望特性的技术。即对模型的状态空间进行型的期望特性的技术。即对模型的状态空间进行搜索，以确认该系统具有某些性质。终止性依赖搜索，以确认该系统具有某些性质。终止性依赖于模型的有限性。优点是：完全自动化、速度快，于模型的有限性。优

18、点是：完全自动化、速度快，可用于系统的部分规范。缺点是：可用于系统的部分规范。缺点是：“状态爆炸问状态爆炸问题题”因而极大地限制其实际使用范围。因而极大地限制其实际使用范围。有序二叉决策图（有序二叉决策图（OrderedBinaryDecisionDiagrams)是一种表述状态转移系统的高效率是一种表述状态转移系统的高效率的方法。目前可以处理的方法。目前可以处理100200个状态变量、个状态变量、状态数达状态数达10120的系统。的系统。10/26/202217模型检验需要工具的支持，已有的工具有：模型检验需要工具的支持，已有的工具有：时态逻辑模型检验工具，如：时态逻辑模型检验工具，如：EM

19、C、CESAR、SMV、Nurphi、SPIN、UV等。等。行为一致检验工具，如：行为一致检验工具，如：FRD、Cospan/FormalCheck等等复合检验工具，如：复合检验工具，如：HSIS、VIS、STcP等等贝尔实验室用贝尔实验室用FormalCheck对其高级数据链路控对其高级数据链路控制器进行验证，从制器进行验证，从6个性能的规范中发现一个失个性能的规范中发现一个失败，进而发现一个影响信道流量的败，进而发现一个影响信道流量的Bug。基于基于SMV输入语言建立了输入语言建立了IEEEFuturebus1991标准下标准下cache一致协议精确模型，通过一致协议精确模型，通过SMV的

20、验证，发现了原先未找到和潜在的错误。此工的验证，发现了原先未找到和潜在的错误。此工作是第一次从作是第一次从IEEE标准中发现错误。标准中发现错误。10/26/202218(2)定理证明采用逻辑公式来规范系统及其性质，这定理证明采用逻辑公式来规范系统及其性质，这儿的逻辑由一个具有公理或推理规则的形式系统儿的逻辑由一个具有公理或推理规则的形式系统给出，进行定理证明的过程就是应用这些公理或给出，进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。推理规则来证明系统具有某些性质。定理证明可以处理无限状态空间问题，粗略地定理证明可以处理无限状态空间问题，粗略地分为自动和交互两种类型，分为

21、自动和交互两种类型，自动定理证明系统是通用搜索过程，在解决各自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功。种组合问题中比较成功。交互式定理证明系统需要与用户进行交互，要交互式定理证明系统需要与用户进行交互，要求用户能提供验证中创造性最强的部分（如断求用户能提供验证中创造性最强的部分（如断言等），因此效率较低，较难用于大系统的验言等），因此效率较低，较难用于大系统的验证。证。10/26/202219现有的定理证明器有：现有的定理证明器有：(1)用户导引自动推理工具，如：用户导引自动推理工具，如：ACL2，Eves、LP、Nqthn和和RRL等它们由引理或定义序列导等它们由引理或定

22、义序列导引，每一个定理采用已建立的推演、引理驱动引，每一个定理采用已建立的推演、引理驱动重写和简化启发式来自动证明。重写和简化启发式来自动证明。(2)证明检验器，如：证明检验器，如：Coq、HOL、LEGO等。等。(3)复合证明器，如：复合证明器，如：Analytica中将定理证明和符中将定理证明和符号代数系统号代数系统Mathematica复合，复合，PVS和和Step将决将决策过程，模型检验和交互式证明复合在一起。策过程，模型检验和交互式证明复合在一起。基于符号代数运算的自动证明用于证明基于符号代数运算的自动证明用于证明Pentium中中SRT算法的正确性，查出了一个由故障商数算法的正确性

23、，查出了一个由故障商数字选择表引起的错误字选择表引起的错误。10/26/2022203.程序求精（又称程序变换）程序求精（又称程序变换）是将自动推理和形式化方法相结合而形成的一门是将自动推理和形式化方法相结合而形成的一门新技术，研究从抽象的形式规范推演出具体的面新技术，研究从抽象的形式规范推演出具体的面向计算机的程序代码的全过程。向计算机的程序代码的全过程。基本思想是：用一个抽象程度低、过程性强的基本思想是：用一个抽象程度低、过程性强的程序去替代一个抽象程度高、过程性弱的程序，程序去替代一个抽象程度高、过程性弱的程序，并保持二者功能的一致性。这儿的并保持二者功能的一致性。这儿的“程序程序”是是

24、广义的广义的“程序程序”，是对规范、设计文档、程序，是对规范、设计文档、程序代码的统称。代码的统称。按这种观点，程序开发的过程就是从最高层的按这种观点，程序开发的过程就是从最高层的程序开始，通过一系列的求精变换，每一次都程序开始，通过一系列的求精变换，每一次都降低一些抽象程度或增加一些可执行性，最终降低一些抽象程度或增加一些可执行性，最终得到能指导计算机明确执行的程序代码。得到能指导计算机明确执行的程序代码。10/26/202221在进行求精的过程中必须要保证程序的正确性，在进行求精的过程中必须要保证程序的正确性，即保证程序是满足最初的形式规范的。即保证程序是满足最初的形式规范的。程序的这种正

25、确性可以通过求精过程中所遵循的程序的这种正确性可以通过求精过程中所遵循的一系列规则来保证，也可以采用验证工具来证明。一系列规则来保证，也可以采用验证工具来证明。程序求精技术是形式化方法研究的一个热点，尽程序求精技术是形式化方法研究的一个热点，尽管目前真正用于实际软件开发过程中并不多，但管目前真正用于实际软件开发过程中并不多，但是这是一个很重要的方向。是这是一个很重要的方向。典型的方法有：典型的方法有：IBMHursley公司和牛津大学公司和牛津大学PRG程序设计研究组提出的针对程序设计研究组提出的针对Z规范的求精方规范的求精方法，法，CarrollMorgan的规则求精方案（见的规则求精方案（

26、见ProgrammingfromSpecifications一书）。一书）。10/26/202222五、认识五、认识 形式化方法成长至今争议声不断，应正确地认识形形式化方法成长至今争议声不断，应正确地认识形式化方法，在结合到具体的软件开发过程时应考式化方法，在结合到具体的软件开发过程时应考虑：虑：应用的类型，考虑问题领域的特点和模型的复应用的类型，考虑问题领域的特点和模型的复杂性杂性规模和结构，较适应中等规模的系统，大型系规模和结构，较适应中等规模的系统，大型系统应考虑具有良好的结构统应考虑具有良好的结构类型的选择，应从所确定的目标出发考虑采用类型的选择，应从所确定的目标出发考虑采用的形式化方

27、法的类型的形式化方法的类型形式化的级别，应先确定应用的关键程度、项形式化的级别，应先确定应用的关键程度、项目规模、可用资源等确定采用非、半或高度形目规模、可用资源等确定采用非、半或高度形式化的描述式化的描述10/26/202223使用范围，尽管形式化可以适应所有的开发阶使用范围，尽管形式化可以适应所有的开发阶段，但通常应有选择的使用，对那些安全性、段，但通常应有选择的使用，对那些安全性、可信性要求高的构件应用高度的形式化可信性要求高的构件应用高度的形式化工具，工具的支持在形式化方法中具有重要的工具，工具的支持在形式化方法中具有重要的位置，应根据具体项目，综合上述因素选择合位置，应根据具体项目，

28、综合上述因素选择合适的工具适的工具10/26/20222410/26/202225结论：结论：形式化的方法不是灵丹妙药，形式化的方法不是灵丹妙药，而是一种改进系统可靠性的方法。而是一种改进系统可靠性的方法。10/26/2022262.基于代数方法的规范语言基于代数方法的规范语言OBJ该方法的理论工作由该方法的理论工作由GuttageGuttage提出提出基本格式：基本格式：（语法定义、语义定义、限制说明）（语法定义、语义定义、限制说明）语法定义指出类型的语法信息和检查信息语法定义指出类型的语法信息和检查信息 作用：定义了类型与函数作用：定义了类型与函数语义定义指出了类型和操作间的公理语义定义指

29、出了类型和操作间的公理 作用：定义了类型的语义作用：定义了类型的语义限制说明给出各种限制，防止二义性限制说明给出各种限制，防止二义性 作用：和语义定义一起给出重写规则作用：和语义定义一起给出重写规则基基础础抽抽象象是是整整数数集集，函函数数定定义义了了它它们们之之间间的的相相互互关关系系，这样这样规规范的范的值值与函数形成一个抽象代数。与函数形成一个抽象代数。10/26/202227形式定义：形式定义：代数规范是三元组（代数规范是三元组（S S、E E）其其中中：S S、是是标标记记，S是是类类集集，是是操操作作集集，E是是有有限限个个方方程程的的集集合合，形形式式为为L=R，其其中中L、R

30、S，称称为项。为项。项的定义项的定义 S中的变元是项中的变元是项 常量是项常量是项 项经过操作集项经过操作集 中的操作后也是项中的操作后也是项有工具支持的二个代数规范语言是：有工具支持的二个代数规范语言是：AFFIRM、OBJ10/26/202228一一OBJ简介简介一一种种代代数数形形式式规规范范语语言言，最最基基本本的的概概念念是是ADT（抽抽象数据类型），每个象数据类型），每个ADT描述一个客体。描述一个客体。具有很强的独立定义和数据抽象的机制。具有很强的独立定义和数据抽象的机制。支支持持层层次次化化设设计计，即即在在定定义义高高层层ADTADT时时可可以以使使用用下下层层已定义的已定义

31、的ADTADT。用用OBJOBJ书书写写形形式式规规范范的的过过程程就就是是用用代代数数等等式式（方方程程）定义定义ADTADT的过程。的过程。是是一一种种基基于于代代数数方方程程逻逻辑辑的的代代数数形形式式语语义义，又又具具有有一一种种基基于于把把代代数数方方程程解解释释为为重重写写规规则则的的操操作作语语义义。（可利用这种语义证明程序的正确性）。（可利用这种语义证明程序的正确性）。10/26/202229二、基本形式二、基本形式一个一个OBJ的形式规范说明是诸多的形式规范说明是诸多ADT定义的集合，定义的集合，每个每个ADT具有如下形式：具有如下形式：其中其中obj与与jbo是必须的，其余

32、部分任选。是必须的，其余部分任选。10/26/202230例例1 1定义定义ADT NATURALADT NATURAL obj NATURAL obj NATURAL sorts nat sorts nat ops ops 0:nat/*0无定义域，常量无定义域，常量*/succ(-):natnat/*nat上上的的一一目目运运算算，-表表示示运运算对象算对象*/jbo jbo在在定定义义ADT时时若若需需要要用用到到低低层层已已定定义义ADTL中中的的运算，可在运算，可在obj处用处用/L指出，多个时用空格分隔。指出，多个时用空格分隔。例子例子10/26/202231例例2.在在NATUR

33、AL的基础上定义的基础上定义ADDobjADD/NATURALops-+-:natnatnatvarsx,y:nateqns(0+x=x)(succ(x)+y=succ(x+y)jbo下下面面将将给给出出一一个个较较大大的的形形式式规规范范定定义义对对整整数数序序列列进进行行分分类类。在在规规范范中中自自底底向向上上的的顺顺序序分分别别定定义义了了多多个个ADT。如如：Boolean、Integer、seq_INT、sort_seq_INT等。等。10/26/202232例例3对一个整型数列分类的形式规范对一个整型数列分类的形式规范1.objBoolean/TRUTH/TRUTH是是OBJ内内

34、部部已已 varsa:Boolean/定义的定义的ADT，它具有，它具有eqns(not(T)=F)/T和和F两个常量两个常量(not(F)=T)(not(not(a)=a)(Tanda=a)(aandF=F)(Tora=T)(Fora=a)jbo10/26/2022332.整型整型ADT/对下述十个运算的规则容易给出，故省略了对下述十个运算的规则容易给出，故省略了objInteger/Booleansorts INTops-:INTINT-+-:INTINTINT-:INTINTINT-*-:INTINTINT-div-:INTINTINT-mod-:INTINTINT-:INTINTBoo

35、lean-=-:INTINTBooleanjbo10/26/2022343.定义整型字符串定义整型字符串ADTobj seq_INT/Integersortsseq_INTops:seq_INT/空空-:seq_INT/常量常量-:seq_INTseq_INTseq_INT/链接链接hd-:seq_INTINT/头元素头元素tl-:seq_INTseq_INT/尾串尾串len-:seq_INTINT/长度长度vars i:INTs:seq_INT10/26/202235eqns(s=s)(s=s)(hd=0)(hdi=i)(hd(i s)=i)(tl=)(tli=)(tl(i s)=s)(le

36、n=0)(lens=succ(len(tls)ifs)jbo10/26/2022364定义比较定义比较ADTobjsort_seq_split/seq_INTIntegerops-=-:seq_INT,INTseq_INTvars s:seq_INTi,x:INTeqns(x=)(i=x)(ix=iifix)(i s)x=s=x)(i s)x=i sxifi=x=)(i=x=ifi=x=i(s=x)ifi=x)jbo10/26/2022375定义分类定义分类ADT的规范的规范objsort_seq_INT/sort_seg_splitseq_INTIntegerBooleanops sort-

37、:seq_INTseq_INTis_sorted-:seq_INTBooleanvarss,s1,s2:seq_INTi,j,x:INTeqns(is_sorted=T)(is_sortedi=T)(is_sortedi j=i=j)(is_sortedi j s=ij)(sort(i j)s=sort(j i s)ifij)(sort(s i j)=sort(s j i)ifij)(sort(s1 i j s2)=sort(s1 j i s2ifij)(sort(tls=hds)=sortsifs)(s=x=(tls=x)ifsandhds=x=hds(tls=x)ifsandhds=x)(

38、sx=(tls=x)(sx=hds(tlsx)ifsandhdsx)jbo10/26/202239三、运算的性质三、运算的性质从功能上可以将运算分为四类：从功能上可以将运算分为四类：1.初始化运算初始化运算不不以以任任何何别别的的类类型型客客体体作作为为它它的的输输入入，其其结结果果是是具具有有自身类型的值。自身类型的值。如：如：seq_INT-2.构造运算构造运算以以自自身身类类型型客客体体和和别别的的类类型型客客体体为为输输入入，产产生生具具有有自自身类型的结果。身类型的结果。如：如：-3.修改运算修改运算修改自身类型客体的变量修改自身类型客体的变量 如：如：tl4.观察运算观察运算以以自

39、自身身类类型型客客体体为为输输入入，得得出出具具有有别别的的类类型型客客体体的的结果。结果。如：如：len10/26/202240四、抽象的计算程序四、抽象的计算程序例例4定义自然数类型的栈运算的定义自然数类型的栈运算的ADTobjStack/IntegerBooleansorts stackopscreate:stack/*空栈空栈*/push-:stackINTstackpop-:stackstacktop-:stackINTERRempty-:stackBoolean10/26/202241vars s:stackn:INTeqns(empty(create)=T)(empty(push

40、s,n)=F)(pop(create)=create)(pop(push(s,n)=s)(top(create)=ERR)(top(push(s,n)=n)jbo10/26/202242抽象计算程序的计算可以归结为代数系统中的重写抽象计算程序的计算可以归结为代数系统中的重写规则的应用，而得到计算的结果。规则的应用，而得到计算的结果。例例5：设抽象计算程序为：设抽象计算程序为：create()push(s,5)push(s,3)pop(s)top(s)则则top(s)=top(pop(s)=top(pop(push(s,3)=top(pop(push(push(s,5),3)=top(push(

41、s,5)=5由此可知，这种方法可以机械执行。由此可知，这种方法可以机械执行。10/26/202243正确性证明正确性证明依赖相应的依赖相应的ADT中定义的运算规范，可以证明程序中定义的运算规范，可以证明程序的正确性。方法为：将代数等式视为重写规则，即的正确性。方法为：将代数等式视为重写规则，即将等式将等式L=R视为视为LR（L被定义为被定义为R）。就可以用）。就可以用于程序的正确性证明。于程序的正确性证明。10/26/2022443.基于模型方法的规范语言基于模型方法的规范语言VDMTheViennaDevelopmentMethod一、概况一、概况VDM由由IBM的的Vienna实实验验室室

42、20世世纪纪70年年代代提提出出的的的的一一种种形形式式化化方方法法。最最初初是是为为了了解解决决用用形形式式化化方方法法来来开开发发编编译译系系统统，使使语语言言的的语语法法、语语义义的的定定义义更更为为严严格格、更更加加系系统统化化（如如实实现现PL/1语语言言的的语语义义规规范范）。当时用当时用VDL用于语言的注释。得到广泛的应用用于语言的注释。得到广泛的应用VDM在在欧欧洲洲得得到到发发展展，从从70年年代代末末到到90年年代代在在欧欧美美许许多多研研究究机机构构和和大大学学得得到到广广泛泛的的应应用用（如如曼曼彻彻斯斯特特大大学学讲讲其其作作为为必必修修课课），以以后后逐逐渐渐称称为

43、为一一般般的的软软件件开发方法。开发方法。10/26/2022451996年国际标准化组织（年国际标准化组织（ISO）制定了）制定了VDM的国际的国际化版本化版本VDMSL（VDMSpecificationLanguage)。目前目前VDM已称为应用最为广泛的形式化规范语言。已称为应用最为广泛的形式化规范语言。VDM是一种功能构造性规范技术。由一阶谓词逻是一种功能构造性规范技术。由一阶谓词逻辑和已经建立的辑和已经建立的ADT来描述每个运算或函数的功能。来描述每个运算或函数的功能。基本思想是基本思想是ADTADT、数学概念和符号来规定运算或函数、数学概念和符号来规定运算或函数的功能，而且这种规定

44、的过程是结构化的，其目的的功能，而且这种规定的过程是结构化的，其目的是要在系统实现之前简单而又明确地指出软件系统是要在系统实现之前简单而又明确地指出软件系统要完成的功能。要完成的功能。支持程序正确性的证明。用支持程序正确性的证明。用Hoare的前的前/后断言描述后断言描述运算的规范。运算的规范。10/26/202246二、二、VDM的形式规范的基本组成形式的形式规范的基本组成形式VDM形式规范由三部分组成：形式规范由三部分组成：状态、类型不变式、运算功能状态、类型不变式、运算功能是一种基于抽象模型的方法，是一种基于抽象模型的方法，由：由：表示（数据）抽象表示（数据）抽象系统的状态描述系统的状态

45、描述和和运算（操作）抽象运算（操作）抽象用前用前/后断言后断言所组成。所组成。模型规范的形式定义：模型规范的形式定义：M=(，0,，)是是M的状态集（含有不变式）的状态集（含有不变式）0是初始状态是初始状态是运算集合是运算集合其实质是将软件系统视为基本状态的运算类型。其实质是将软件系统视为基本状态的运算类型。10/26/2022471、系统状态规则系统状态规则基本形式：类型基本形式：类型ID=类型定义实体类型定义实体其中：其中：ID是新定义的一个类型名是新定义的一个类型名实体是基本类型定义的一个新类型。实体是基本类型定义的一个新类型。基本类型：基本类型：基本型：基本型：N,R,B(自然数，实数

46、，自然数，实数，Boolean)运算是常见的算术和逻辑运算运算是常见的算术和逻辑运算集合型：形式为：集合型：形式为：X=setofQQ是已定义类型或基本类型，是已定义类型或基本类型，X是集合型是集合型ID运运算算有有：并并（）、交交（）、差差（/）、元元素素个个数数（card）、属属于于（）、子子集集（）、真真子子集集（）等）等10/26/202248表表型型：有有序序集集合合，每每个个元元素素有有确确定定位位置置，可可重重复复出出现，定义形式为：现，定义形式为：S=seqofQS为新类型的为新类型的ID，Q为为S的元素类型的元素类型运运算算有有：求求头头（hd）、求求尾尾（tl)、长长度度（

47、len)、连连接（接（conj）、元素集（）、元素集（elem)、索引集（、索引集（inds)等等映映射射：有有限限、可可列列集集的的一一个个函函数数，通通常常以以对对偶偶集集合合形式表示，定义形式为：形式表示，定义形式为：M=MapofQM为新类型的为新类型的ID，Q为为M的元素类型的元素类型运算有：求定义域（运算有：求定义域（dom），求值域（），求值域（rng）限定定义域（限定定义域（），定义域元素删除（），定义域元素删除（）等）等10/26/202249复合型：复合型：P=ComposePofe1:Q1e2:Q2endP为为新新类类型型的的ID，ei、Qi（i=1）分分别别为为P的的分

48、分量量名和分量类型名和分量类型运运算算：求求复复合合类类型型值值（mk_P）、改改变变分分量量值值、求求分分量的值。量的值。10/26/202250例一个教师职称提升系统的例一个教师职称提升系统的ADT定义定义Studentdata=ComposeStudentdataofName:StringT_score_list:SeqofChoiceendResearchdata=ComposeResearchdataofName1:StringR_Score_List:SeqofNendTeacher=ComposeTeacherofT_name:StringT_score:RR_score:Ren

49、d10/26/2022512、类型不变式规则、类型不变式规则类型不变式是指对状态规则中规定的类型给出其应类型不变式是指对状态规则中规定的类型给出其应满足的性质。满足的性质。表示形式：表示形式：设设ST是在类型规范中所定义的一个类型是在类型规范中所定义的一个类型ID。Inv_ST(S)=P(S)其其中中：P(S)是是一一个个一一阶阶谓谓词词公公式式，S ST，即即ST中中任任一元素一元素S应满足的条件应满足的条件例例2.例例1中中ADTStudentdata描述了对一个教师的评价：描述了对一个教师的评价：Inv_Studentdata mk_Studentdata(n,t)S t Inv_Cho

50、ice t Choicelent=410/26/2022523、运算功能规则、运算功能规则运算功能规则运算功能规则VDM形式规范中的主要形式，其一般形式规范中的主要形式，其一般形式为：形式为：OP（m1:Tm1,m2:Tm2,mn:Tmn）r1:Tr1,re,TreextPV1:Tv1PVk:TvkpreC1/C1表示为（表示为（mj,rk,)postC2/C2表示为（表示为（mj,Vi,rk,Vi)其中：其中：OP是运算名，是运算名，mi是输入参量，是输入参量，ri是输出参量，是输出参量，ext表示表示Vi外部量；外部量；P wr,rd，表示可读或可写；，表示可读或可写；pre是前置谓词，是