程序设计方法学.ppt

《程序设计方法学.ppt》由会员分享，可在线阅读，更多相关《程序设计方法学.ppt（71页珍藏版）》请在三一办公上搜索。

1、2023/9/28,华东师大计算机科学技术系,1,第六章 程序设计的形式化方法,软件新技术智能化技术 扩大软件功能的关键途径自动化技术 提高软件生产率的根本途径集成化技术 助于提高生产率、提高质量并行化技术 提高系统实效的关键技术自然化技术 实现社会信息化,2023/9/28,华东师大计算机科学技术系,2,重要方向 攻克的关键教技术网络体系 传感器网与因特网的高效融合集成芯片 从System on chip到Chip on demount虚拟计算 资源聚合的有效性和可靠性验证软件工程 基于网络环境的需求工程知识处理 挖掘从消息到知识到决策的元知识高效系统 在高性（效）能计算系统中系列关注 信息

2、安全信息教育,2023/9/28,华东师大计算机科学技术系,3,跨越源之识规律,创新根植辨短长,汪成为院士,2023/9/28,华东师大计算机科学技术系,4,软件自动化的三个层次,软件自动化（自动程序设计）广义：尽可能地借助计算机系统实现软件开发狭义：从形式化的软件功能规范到可执行程序代码 这一过程的自动化 从软件需求规范 软件功能、性能规范的转换解决从“非形式”“形式”难度很大，寄希望于受限自然语言方面的突破从软件功能、性能规范 软件设计从“做什么”“如何做“从软件设计规范 高级语言 已有相当的进展，出现了许多工具,2023/9/28,华东师大计算机科学技术系,5,1 概述,一、重要意义 软

3、件发展中的问题：整体功能不强、缺乏智能、质量欠佳、生产效率低软件自动化是提高软件生产率的根本途径软件自动化的前提是形式化因此将形式化的理论和方法用于需求分析与规格说明是实现软件自动化的前提,2023/9/28,华东师大计算机科学技术系,6,二、发展状况有30多年历史Dijkstra、Hoare程序验证 Scott、Stratchey 程序语义 形式化方法(Formal Method)：通过严格的规范化的数学理论来描述软件系统“做什么”的方法。需要形式规范语言的支持。形式规范语言：提供了一个称为语法域的记号系统。一个称为语义域的目标集合，以及一组精确定义的哪些目标系统满足那个规范的规则。,202

4、3/9/28,华东师大计算机科学技术系,7,因此，形式化方法是在软件系统的开发过程中使用一种形式系统来表示模型的方法。形式系统是二元组（L，Cn）L：语言（形式规范语言）Cn：对应关系，由推理规则构成在软件规范方法方面的代表性成果有：基于异调代数的代数方法 特点：用抽象代数中的公理化方法来刻画抽象数据类型中运算的性质，而不涉及数据的具体表示。基本理论：代数语义,2023/9/28,华东师大计算机科学技术系,8,抽象模型方法 特点：基于某些已知的ADT来给出待定义的 ADT的抽象模型，用抽象模型来刻画待 定义的ADT中运算的功能。基本理论：指称语义状态机方法 特点：通过状态的转换来刻画输入与输出

5、间的 关系 基本理论：操作语义高阶软件方法（HOS）基于控制公理 基本理论：公理语义,2023/9/28,华东师大计算机科学技术系,9,在软件规范语言方面的代表性成果有：一阶谓词演算组成语言 80年代：Z语言、Larch语言、VDM语言 90年代：面向实时及分布式的LOTOS语言、面向对象的Z+、Object-Z、VDM+等三、分类基于模型的方法 给出系统（程序）状态和状态变换与操作的显式的表示但亦是抽象的定义，不涉及并发的行为。如：Z、VDM,2023/9/28,华东师大计算机科学技术系,10,代数方法 通过联系不同的操作间的行为关系给出操作的隐式定义，未给出并发的显式表示。如：OBJ、La

6、rch过程代数方法 给出并发过程的一个显式模型，并通过过程间允许的可观察的通信上的限制来约束表示行为。如：CSP（通信顺序进程）和CCS（通信系统计算）基于逻辑的方法 采用逻辑来描述系统的特性，包括程序行为的低级规范和系统时间的行为规范。如：时态逻辑、模态逻辑,2023/9/28,华东师大计算机科学技术系,11,基于网络的方法 根据网络中的数据流显式地给出系统的并发模型，包括数据从一个结点流向另一个结点的条件。如：Petri网、谓词变换网,2023/9/28,华东师大计算机科学技术系,12,四、形式化软件开发方法采用软件生命周期的变换模型，其实质是将现实世界的需求反映成软件的模型化过程。涉及三

7、方面模型：现实世界，模型表示和计算机系统。因此开发的过程就是从三方面对系统进行描述和转换的过程。开发过程中的任务为：模型获取：从现实世界向模型表示的过程，涉及如何提取、表示模型。对应需求分析、设计等活动。模型验证：对得到的模型表示进行检验，判断是否捕获了所有的需求，该模型是否具有所期望的特性。模型变换：是向计算机系统变换的过程，关键的任务是一致性检测。对应实现和测试。,2023/9/28,华东师大计算机科学技术系,13,三项任务分别对应三方面的活动：1.形式化规范（规格）：软件规范是指对软件系统对象及用来对系统对象进行操作的方法的集合。以及对所开发系统中的各对象在生命周期间的集体行为的描述。对

8、应与软件生命周期的各个阶段，规范应该理解为是一个多阶段的行为。见例图规范可以采用非、半形式化的方法来描述，形式化规范精确地描述了用户的需求、软件系统的功能及各种性质，其描述的是“做什么”，而不考虑“如何做”。因此，在理解、掌握形式规范语言和方法的基础上对所描述的系统的全面、深入的了解，给出恰如其分的描述上至关重要的。,2023/9/28,华东师大计算机科学技术系,14,包含各规格阶段的生命周期模型例,需求分析,BS,SRD,系统设计1,DS,系统设计2,PS,软件开发,代码实现,软件测试,运行,SRD：软件需求文档BS：行为规范DS：设计规范PS：程序规范,2023/9/28,华东师大计算机科

9、学技术系,15,软件系统规范的形式化方法,从形式化规范到目标软件系统的可实现和可执行角度，可分为三类：操作类：此类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型执行而得到验证。如：有限状态机、Statecharts、Petri网等。描述类：此类方法基于数学公理和概念，通过逻辑或代数给出系统状态空间，具有高度抽象的特点，便于通过自动工具进行验证。如：基于代数的Z、VDM、Larch等，基于逻辑的命题线性时态逻辑、一阶线性时态逻辑、计算树逻辑等。双重类：此类方法兼具二者的特点，如：扩展状态机/实时时态逻辑等。,2023/9/28,华东师大计算机科学技术系,16,形式化

10、规范的成功案例,IBM商用信息系统，牛津大学和Hursley实验室使用Z语言。总体成本降低9，获皇家技术成就奖。Praxis公司使用VDM开发的伦敦机场信息显示系统，软件质量大为提高，故障率0.75(220)每K行代码。其他领域：数据库：HP医用仪器实时数据库系统电子仪器：Tektronix系列谐波发生器硬件：INMOS浮点处理器、INMOS中T9000系列虚拟信道处理器运输系统：巴黎地铁自动火车保护系统、以色列机载航空电子软件等等,2023/9/28,华东师大计算机科学技术系,17,形式化验证软件开发中错误发现的越晚修改的代价越大，与传统方法不同的是形式化方法要求在完成形式规范后就进行形式验

11、证。形式验证主要技术包括模型检验和定理证明。模型验证是一种基于有限状态机模型并检验该模型的期望特性的技术。即对模型的状态空间进行搜索，以确认该系统具有某些性质。终止性依赖于模型的有限性。优点是：完全自动化、速度快，可用于系统的部分规范。缺点是：“状态爆炸问题”因而极大地限制其实际使用范围。有序二叉决策图（Ordered Binary Decision Diagrams)是一种表述状态转移系统的高效率的方法。目前可以处理100200个状态变量、状态数达10120的系统。,2023/9/28,华东师大计算机科学技术系,18,模型检验需要工具的支持，已有的工具有：时态逻辑模型检验工具，如：EMC、C

12、ESAR、SMV、Nurphi、SPIN、UV等。行为一致检验工具，如：FRD、Cospan/Formal Check等 复合检验工具，如：HSIS、VIS、STcP等 贝尔实验室用FormalCheck对其高级数据链路控制器进行验证，从6个性能的规范中发现一个失败，进而发现一个影响信道流量的Bug。基于SMV输入语言建立了IEEE Futurebus896.11991标准下cache一致协议精确模型，通过SMV的验证，发现了原先未找到和潜在的错误。此工作是第一次从IEEE标准中发现错误。,2023/9/28,华东师大计算机科学技术系,19,定理证明采用逻辑公式来规范系统及其性质，这儿的逻辑由

13、一个具有公理或推理规则的形式系统给出，进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。定理证明可以处理无限状态空间问题，粗略地分为自动和交互两种类型，自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功。交互式定理证明系统需要与用户进行交互，要求用户能提供验证中创造性最强的部分（如断言等），因此效率较低，较难用于大系统的验证。,2023/9/28,华东师大计算机科学技术系,20,现有的定理证明器有：用户导引自动推理工具，如：ACL2，Eves、LP、Nqthn和RRL等它们由引理或定义序列导引，每一个定理采用已建立的推演、引理驱动重写和简化启发式来自动证明。证明检验

14、器，如：Coq、HOL、LEGO等。复合证明器，如：Analytica中将定理证明和符号代数系统Mathematica复合，PVS和Step将决策过程，模型检验和交互式证明复合在一起。基于符号代数运算的自动证明用于证明Pentium中SRT算法的正确性，查出了一个由故障商数字选择表引起的错误。,2023/9/28,华东师大计算机科学技术系,21,程序求精（又称程序变换）是将自动推理和形式化方法相结合而形成的一门新技术，研究从抽象的形式规范推演出具体的面向计算机的程序代码的全过程。基本思想是：用一个抽象程度低、过程性强的程序去替代一个抽象程度高、过程性弱的程序，并保持二者功能的一致性。这儿的“程

15、序”是广义的“程序”，是对规范、设计文档、程序代码的统称。按这种观点，程序开发的过程就是从最高层的程序开始，通过一系列的求精变换，每一次都降低一些抽象程度或增加一些可执行性，最终得到能指导计算机明确执行的程序代码。,2023/9/28,华东师大计算机科学技术系,22,在进行求精的过程中必须要保证程序的正确性，即保证程序是满足最初的形式规范的。程序的这种正确性可以通过求精过程中所遵循的一系列规则来保证，也可以采用验证工具来证明。程序求精技术是形式化方法研究的一个热点，尽管目前真正用于实际软件开发过程中并不多，但是这是一个很重要的方向。典型的方法有：IBM Hursley公司和牛津大学PRG程序设

16、计研究组提出的针对Z规范的求精方法，Carroll Morgan的规则求精方案（见Programming from Specifications一书）。,2023/9/28,华东师大计算机科学技术系,23,五、认识 形式化方法成长至今争议声不断，应正确地认识形式化方法，在结合到具体的软件开发过程时应考虑：应用的类型，考虑问题领域的特点和模型的复杂性规模和结构，较适应中等规模的系统，大型系统应考虑具有良好的结构类型的选择，应从所确定的目标出发考虑采用的形式化方法的类型形式化的级别，应先确定应用的关键程度、项目规模、可用资源等确定采用非、半或高度形式化的描述,2023/9/28,华东师大计算机科学

17、技术系,24,使用范围，尽管形式化可以适应所有的开发阶段，但通常应有选择的使用，对那些安全性、可信性要求高的构件应用高度的形式化工具，工具的支持在形式化方法中具有重要的位置，应根据具体项目，综合上述因素选择合适的工具,2023/9/28,华东师大计算机科学技术系,25,2023/9/28,华东师大计算机科学技术系,26,结论：形式化的方法不是灵丹妙药，而是一种改进系统可靠性的方法。,2023/9/28,华东师大计算机科学技术系,27,2.基于代数方法的规范语言OBJ,该方法的理论工作由Guttage提出基本格式：（语法定义、语义定义、限制说明）语法定义指出类型的语法信息和检查信息 作用：定义了

18、类型与函数语义定义指出了类型和操作间的公理 作用：定义了类型的语义限制说明给出各种限制，防止二义性 作用：和语义定义一起给出重写规则基础抽象是整数集，函数定义了它们之间的相互关系，这样规范的值与函数形成一个抽象代数。,2023/9/28,华东师大计算机科学技术系,28,形式定义：代数规范是三元组（S、E）其中：S、是标记，S是类集，是操作集，E是有限个方程的集合，形式为L=R，其中L、RS，称为项。项的定义S中的变元是项常量是项项经过操作集中的操作后也是项有工具支持的二个代数规范语言是：AFFIRM、OBJ,2023/9/28,华东师大计算机科学技术系,29,一OBJ简介,一种代数形式规范语言

19、，最基本的概念是ADT（抽象数据类型），每个ADT描述一个客体。具有很强的独立定义和数据抽象的机制。支持层次化设计，即在定义高层ADT时可以使用下层已定义的ADT。用OBJ书写形式规范的过程就是用代数等式（方程）定义ADT的过程。是一种基于代数方程逻辑的代数形式语义，又具有一种基于把代数方程解释为重写规则的操作语义。（可利用这种语义证明程序的正确性）。,2023/9/28,华东师大计算机科学技术系,30,二、基本形式,一个OBJ的形式规范说明是诸多ADT定义的集合，每个ADT具有如下形式：,其中obj与jbo是必须的，其余部分任选。,2023/9/28,华东师大计算机科学技术系,31,例1定义

20、ADT NATURAL obj NATURAL sorts nat ops 0:nat/*0无定义域，常量*/succ(-):natnat/*nat上的一目运算，-表示运算对象*/jbo在定义ADT时若需要用到低层已定义ADT L中的运算，可在obj处用/L指出，多个时用空格分隔。,例子,2023/9/28,华东师大计算机科学技术系,32,例2.在NATURAL的基础上定义ADDobj ADD/NATURALops-+-:nat nat natvars x,y:nateqns(0+x=x)(succ(x)+y=succ(x+y)jbo下面将给出一个较大的形式规范定义对整数序列进行分类。在规范中

21、自底向上的顺序分别定义了多个ADT。如：Boolean、Integer、seq_INT、sort_seq_INT等。,2023/9/28,华东师大计算机科学技术系,33,例3对一个整型数列分类的形式规范1.objBoolean/TRUTH/TRUTH是OBJ内部已 varsa:Boolean/定义的ADT，它具有 eqns(not(T)=F)/T和F两个常量(not(F)=T)(not(not(a)=a)(T and a=a)(a and F=F)(T or a=T)(F or a=a)jbo,2023/9/28,华东师大计算机科学技术系,34,2.整型ADT/对下述十个运算的规则容易给出，故

22、省略了 objInteger/Boolean sortsINT ops-:INTINT-+-:INT INTINT-:INT INTINT-*-:INT INTINT-div-:INT INTINT-mod-:INT INT INT-:INT INT Boolean-=-:INT INT Boolean jbo,2023/9/28,华东师大计算机科学技术系,35,3.定义整型字符串ADT obj seq_INT/Integer sorts seq_INT ops:seq_INT/空-:seq_INT/常量-:seq_INT seq_INT seq_INT/链接 hd-:seq_INT INT/

23、头元素 tl-:seq_INT seq_INT/尾串 len-:seq_INT INT/长度 varsi:INT s:seq_INT,2023/9/28,华东师大计算机科学技术系,36,eqns(s=s)(s=s)(hd=0)(hdi=i)(hd(is)=i)(tl=)(tli=)(tl(i s)=s)(len=0)(len s=succ(len(tl s)if s)jbo,2023/9/28,华东师大计算机科学技术系,37,4定义比较ADT objsort_seq_split/seq_INT Integer ops-=-:seq_INT,INTseq_INT varss:seq_INTi,x

24、:INT eqns(=x)(i=x)(is)=x=)(i=x=if i=x=i(s=x)if i=x)jbo,2023/9/28,华东师大计算机科学技术系,38,5定义分类ADT的规范obj sort_seq_INT/sort_seg_split seq_INT Integer Boolean opssort-:seq_INTseq_INTis_sorted-:seq_INTBoolean varss,s1,s2:seq_INT i,j,x:INT eqns(is_sorted=T)(is_sortedi=T)(is_sortedij=i=j)(is_sortedijs=i=j and is_

25、sorted(js)(sort s=s if is_sorted s),2023/9/28,华东师大计算机科学技术系,39,(sort(ij)=sort(ji)if ij)(sort(ij)s=sort(ji s)if ij)(sort(s ij)=sort(s ji)if ij)(sort(s1i js2)=sort(s1j is2 if ij)(sort(tl s=hd s)=sort s if s)(s=x=(tl s=x)if s and hd s=x=hd s(tl s=x)if s and hd s=x)(s=x)(sx=hd s(tl sx)if s and hd sx)jbo,

26、2023/9/28,华东师大计算机科学技术系,40,三、运算的性质,从功能上可以将运算分为四类：初始化运算不以任何别的类型客体作为它的输入，其结果是具有自身类型的值。如：seq_INT-2.构造运算以自身类型客体和别的类型客体为输入，产生具有自身类型的结果。如：-3.修改运算修改自身类型客体的变量如：tl 4.观察运算 以自身类型客体为输入，得出具有别的类型客体的结果。如：len,2023/9/28,华东师大计算机科学技术系,41,四、抽象的计算程序,例4定义自然数类型的栈运算的ADTobjStack/Integer Booleansortsstackopscreate:stack/*空栈*/

27、push-:stack INTstackpop-:stackstacktop-:stackINTERRempty-:stackBoolean,2023/9/28,华东师大计算机科学技术系,42,varss:stackn:INTeqns(empty(create)=T)(empty(push s,n)=F)(pop(create)=create)(pop(push(s,n)=s)(top(create)=ERR)(top(push(s,n)=n)jbo,2023/9/28,华东师大计算机科学技术系,43,抽象计算程序的计算可以归结为代数系统中的重写规则的应用，而得到计算的结果。例5：设抽象计算程

28、序为：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(s,5)=5由此可知，这种方法可以机械执行。,2023/9/28,华东师大计算机科学技术系,44,正确性证明,依赖相应的ADT中定义的运算规范，可以证明程序的正确性。方法为：将代数等式视为重写规则，即将等式 L=R 视为LR（L被定义为R）。就可以用于程序的正确性证明。,2023/9/28,华东师大计算机科学技术系,45,3.基于模型方法的规范语言VDMThe Vienn

29、a Development Method,一、概况VDM由IBM的Vienna实验室20世纪70年代提出的的一种形式化方法。最初是为了解决用形式化方法来开发编译系统，使语言的语法、语义的定义更为严格、更加系统化（如实现PL/1语言的语义规范）。当时用VDL用于语言的注释。得到广泛的应用VDM在欧洲得到发展，从70年代末到90年代在欧美许多研究机构和大学得到广泛的应用（如曼彻斯特大学讲其作为必修课），以后逐渐称为一般的软件开发方法。,2023/9/28,华东师大计算机科学技术系,46,1996年国际标准化组织（ISO）制定了VDM的国际化版本VDMSL（VDM Specification Lan

30、guage)。目前VDM已称为应用最为广泛的形式化规范语言。VDM 是一种功能构造性规范技术。由一阶谓词逻辑和已经建立的ADT来描述每个运算或函数的功能。基本思想是ADT、数学概念和符号来规定运算或函数的功能，而且这种规定的过程是结构化的，其目的是要在系统实现之前简单而又明确地指出软件系统要完成的功能。支持程序正确性的证明。用Hoare的前/后断言描述运算的规范。,2023/9/28,华东师大计算机科学技术系,47,二、VDM的形式规范的基本组成形式,VDM形式规范由三部分组成：状态、类型不变式、运算功能是一种基于抽象模型的方法，由：表示（数据）抽象系统的状态描述 和运算（操作）抽象用前/后断

31、言 所组成。模型规范的形式定义：M=(，0,，)是M的状态集（含有不变式）0是初始状态是运算集合其实质是将软件系统视为基本状态的运算类型。,2023/9/28,华东师大计算机科学技术系,48,1、系统状态规则,基本形式：类型ID=类型定义实体 其中：ID是新定义的一个类型名实体是基本类型定义的一个新类型。基本类型：基本型：N,R,B(自然数，实数，Boolean)运算是常见的算术和逻辑运算集合型：形式为：X=set of Q Q是已定义类型或基本类型，X是集合型ID 运算有：并（）、交（）、差（/）、元素个数（card）、属于（）、子集（）、真子集（）等,2023/9/28,华东师大计算机科学

32、技术系,49,表型：有序集合，每个元素有确定位置，可重复出现，定义形式为：S=seq of Q S为新类型的ID，Q为S的元素类型 运算有：求头（hd）、求尾（tl)、长度（len)、连接（conj）、元素集（elem)、索引集（inds)等映射：有限、可列集的一个函数，通常以对偶集合形式表示，定义形式为：M=Map of Q M为新类型的ID，Q为M的元素类型运算有：求定义域（dom），求值域（rng）限定定义域（），定义域元素删除（）等,2023/9/28,华东师大计算机科学技术系,50,复合型：P=Compose P of e1:Q1e2:Q2 end P为新类型的ID，ei、Qi（i=

33、1）分别为P的分量名和分量类型运算：求复合类型值（mk_P）、改变分量值、求分量的值。,2023/9/28,华东师大计算机科学技术系,51,例一个教师职称提升系统的ADT定义,Studentdata=Compose Studentdata of Name:String T_score_list:Seq of ChoiceendResearchdata=Compose Researchdata of Name1:String R_Score_List:Seq of NendTeacher=Compose Teacher ofT_name:StringT_score:RR_score:Rend,2

34、023/9/28,华东师大计算机科学技术系,52,2、类型不变式规则,类型不变式是指对状态规则中规定的类型给出其应满足的性质。表示形式：设ST是在类型规范中所定义的一个类型ID。Inv_ST(S)=P(S)其中：P(S)是一个一阶谓词公式，SST，即ST中任一元素S应满足的条件例2.例1中ADT Studentdata描述了对一个教师的评价：Inv_Studentdatamk_Studentdata(n,t)Studentdata.n t Inv_ChoicetChoicelen t=4,2023/9/28,华东师大计算机科学技术系,53,3、运算功能规则,运算功能规则VDM形式规范中的主要形

35、式，其一般形式为：OP（m1:Tm1,m2:Tm2,mn:Tmn）r1:Tr1,re,Tre extP V1:Tv1 P Vk:Tvkpre C1/C1表示为（mj,rk,)post C2/C2表示为（mj,Vi,rk,Vi)其中：OP是运算名，mi是输入参量，ri是输出参量，ext表示Vi外部量；Pwr,rd，表示可读或可写；pre是前置谓词，post是后置谓词。注：Vi是执行OP前状态值，Vi是执行OP后状态值。,2023/9/28,华东师大计算机科学技术系,54,例3简单计算器规范,reg:N/初始时外部变量 reg=0LOAD(i:N)ext wr reg:N pre true pos

36、t reg=iSHOW()r:Next rd reg:N pre true post r=reg,2023/9/28,华东师大计算机科学技术系,55,ADD(i:N)ext wr reg:N pre true post reg=reg+iDIVIDE(d:N)r:N ext wr reg:N pre d0 post d*r+reg=reg0regd,2023/9/28,华东师大计算机科学技术系,56,为了描述方便，在前/后断言中可以出现的一些结构：let_in Q 含义：在let后定义一些临时变量，有效范围是Qif e then P else Q 条件表达式调用定义的函数，函数的规范为：显式定

37、义：f:p1:Tp1p2:Tp2pn:TpnTrf(p1,pn)function body其中：pi是f的参量，类型为Tpi，Tr为f的返回值,2023/9/28,华东师大计算机科学技术系,57,隐式定义：f(p1:Tp1,p2:Tp2,pn:Tpn)r:TrPre_f Post_ 其中：Pre是f的前置谓词 Post是f的后置谓词,2023/9/28,华东师大计算机科学技术系,58,例4一个分类运算的VDM规范,Index_entries=seq of NSORT(S:Index_entries)r:Index_entriesext wr output:Index_entries pre s

38、 post elem r=elem S is_sorted(r)output=output conjr其中：is_sorted(r)是一个函数，判断自然数表是否已经分类。,2023/9/28,华东师大计算机科学技术系,59,三、VDM的程序正确性证明机制,关于函数的正确性证明 f:PTPTr 函数f满足规范，当且仅当pTp，Pre_f(p)f(p)Tr Post_f(p,f(p)关于运算的正确性证明 设运算op的规范为：令表示所有状态的集合，=TpTv1 Tv2Tr证明机制为：V pre_OP(V)rTr V post_OP(V,V)其中：V=exec(OP,r)，即OP执行后的状态,2023

39、/9/28,华东师大计算机科学技术系,60,四、一个VDM规范的例子,例5.用VDM为一个“教师职称提升系统”书写形式规范需求：该系统最终被定义为“Teacher-Promotion”的运算。根据所要提升的名额（m）和全体教师的教学、科研评分表，选出总成绩最好的前m名教师。并输出教师的相关信息各运算及其函数的意义Get_persons:取名额函数Teacher_order:教师排序函数Score_sum:教师积分计算函数 Teacher_list_production:教师序列生成函数Teaching_Research_score:评分科研数据采集函数,2023/9/28,华东师大计算机科学技

40、术系,61,类型说明,String=seq of charChoice=seq of R TeacherSum=Compose TeacherSum of Name2:StringTotal_score:REndTeacher_list=Seq of TeacherSumStudentdata_list=Seq of StudentdataReseachdata_list=Seq of Researchdata 注：其他的说明已在例1中给出,2023/9/28,华东师大计算机科学技术系,62,类型不变式,Inv_studentdata mk_Studentdata(n,t)Studentdat

41、a.n=t Inv_Researchdata mk_Researchdata(n,r)Researchdata.n=r Inv_choice t choice.len t=4,2023/9/28,华东师大计算机科学技术系,63,函数及运算,Teacher_Promotion(tsl:Studentdata_list,rsl:Researchdata_list,m：N)P:Teacher_listext wr output:Teacher_list Pre len tsl=len rsl i inds tsl.name(tsli)=name1(rsli)/*教学、科研二个表中名字相同*/Post

42、 P=Get_Persons(Teacher_order(Teacher_list_production(ts1,rs1),m)output=output conj P,2023/9/28,华东师大计算机科学技术系,64,/*从已排序的教师序列表td中取出总成绩最高的n位教师，从高到低次序放入tt表中*/Get_Persons(td:Teacher_order_list,n:N)tt:Teacher_listPre td len tdni,jinds td i total_score(tdi)total_score(tdj)Post len tt=nelem ttelem tdi,jidns

43、tt itotal_score(tti)total_score(ttj)xelem tt yelem td/elem tt total_score(x)total_score(y),2023/9/28,华东师大计算机科学技术系,65,/*将 输入的tl表中按总成绩从高到低排序后放入另一个表d中*/Teacher_order(tl:Teacher_list)d:Teacher_listPre len tl 0Post elem d=elem tl i,j inds itotal_score(di)=total_score(dj)/*教学得分+科研得分总成绩*/score_sum(te:Teach

44、er)ts:TeachersumPret_name(te)Postt_name(te)=name2(ts)total_score(ts)=t_score(te)+r_score(te),2023/9/28,华东师大计算机科学技术系,66,/*一个递归函数，通过引用score_sum 和 Teacher_Research_Score 计算所有教师的总成绩，并将教师的名字连同其成绩排列在教师表t中作结果*/Teacher_list_production(tsl:Studentdata_list,rsl:Researchdata_list)t:Teacher_listPre len tsl=len

45、rsliinds tsl name(tsli)=name1(rsli)Post if tsl=then t=elset=score_sum(Teacher_Research_Score(hd tsl,hd rsl)conjscore_sum(Teacher_Research_score(tl tsl,tl rsl),2023/9/28,华东师大计算机科学技术系,67,/*计算一个教师的教师评分表和科研评分表后分别得出该教师教学科研的分，并连教师名一同放入变量te中*/Teaching_Research_Score(ts:studentdata,vs:Researchdata)te:Teache

46、rPrer_score_list(vs)t_score_list(ts)Post let mk_Teacher(n,t,r)=te inlet mk_Studentdata(nl,sl)=ts inlet AVE(si)=total inlet mk_Researdatach(n2,rl)=rs inn=nl n=n2 t=total/len sl v=rlj,2023/9/28,华东师大计算机科学技术系,68,/*从四个方面按比例将学生对教师的评分计算出来*/Ave(c:choice)v:RPre truePostif len c=4 thenv=c1*60+c2*20%+c3*10+c4*10else v=0,2023/9/28,华东师大计算机科学技术系,69,五、VDM与OBJ,VDM的优缺点：优点：只告诉计算机“做什么”提供了正确性的证明机制 规范描述简练、精确缺点：运算冗余 描述机制有待完善 不易理解,2023/9/28,华东师大计算机科学技术系,70,OBJ的优缺点：优点：无运算冗余 以性质引导规范 正确性证明过程简单缺点：定义运算的不确定性 程序的执行效率低,2023/9/28,华东师大计算机科学技术系,71,VDM与OBJ之比较,