2022年程序设计导论讲解如何画算法流程图完整.ppt

Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,*,Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,*,程序设计导论讲解如何画算法流程图,数据,:,是操作的对象,操作的目的,:,是对数据进行加工处理，以得到期望的结果,著名计算机科学家沃思,(Nikiklaus Wirth),提出一个公式：,算法,+,数据结构,=,程序,算法是解决“做什么”和“怎么做”的问题,程序中的操作语句,代码,，是算法的体现,不了解算法就谈不上程序设计,1.,什么是算法,广义地说，为解决一个问题而采取的方法和步骤，就称为“算法”,对同一个问题，可以有不同的解题方法和步骤,为了有效地进行解题，不仅需要保证算法正确，还要考虑算法的质量，选择合适的算法,计算机算法可分为两大类别：,数值运算算法,非数值运算算法,数值运算的目的是求数值解,非数值运算包括的面十分广泛，最常见的是用于事务管理领域,2.,简单的算法举例,例,.1,求,1,2,3,4,5,可以用最原始的方法进行：,步骤,1,：先求,1*2,，得到结果,2,。,步骤,2,：将步骤,1,得到的乘积,2,再乘以,3,，得到结果,6,。,步骤,3,：将,6,再乘以,4,，得,24,。,步骤,4,：将,24,再乘以,5,，得,120,。这就是最后的结果。,例,.1,求,1,2,3,4,5,1000,太繁琐,改进的算法：,设变量,p,为被乘数,变量,i,为乘数,用循环算法求结果,S1,：使,p=1,，或写成,1,p,S2,：使,i=2,，或写成,2,i,S3,：使,p,与,i,相乘，乘积仍放在变量,p,中，可表示为：,p*i,p,S4,：使,i,的值加,1,，即,i+1,i,S5,：如果,i,不大于,5,，返回重新执行,S3,；否则，算法结束,最后得到,p,的值就是,5!,的值,若是,1000,，求什么？,例:判定20002500年中的每一年是否闰年，并将结果输出。,闰年的条件：,(1)能被4整除，但不能被100整除的年份都是闰年，如 、2048年,(2)能被400整除的年份是闰年，如2000年,不符合这两个条件的年份不是闰年,例如 、2100年,设,year,为被检测的年份。算法表示如下：,S1,：,2000,year,S2,：若,year,不能被,4,整除，则输出,year,的值和“不是闰年”。然后转到,S6,S3,：若,year,能被,4,整除，不能被,100,整除，则输出,year,的值和“是闰年”。然后转到,S6,S4,：若,year,能被,400,整除，,则,输出,year,的值和“是闰年”，然后转到,S6,S5:,其他情况,输出,year,的值和“不是闰年”,S6,：,year+1,year,S7,：当,year,2500,时，转,S2,，否则停止,year,不能被,4,整除,非闰年,year,被,4,整除，但不能被,100,整除,闰年,year,被,100,整除，又能被,400,整除,闰年,其他,非闰年,逐渐缩小判断的范围,例,:,给出一个大于或等于,3,的正整数，判断它是不是一个素数。,所谓素数,(prime),，是指除了,1,和该数本身之外，不能被其他任何整数整除的数,例如，,13,是素数，因为它不能被,2,，,3,，,4,，,12,整除。,判断一个数,n(n,3),是否素数：将,n,作为被除数，将,2,到,(n-1),各个整数先后作为除数，如果都不能被整除，则,n,为素数,S1,：输入,n,的值,S2,：,i=2,（,i,作为除数）,S3,：,n,被,i,除，得余数,r,S4,：如果,r=0,，表示,n,能被,i,整除，则输出,n,“不是素数”，算法结束；否则执行,S5,S5,：,i+1,i,S6,：如果,i,n-1,，返回,S3,；否则输出,n,“是素数”，然后结束。,可改为,n/2,十进制数转换成二进制数（整数部分）,方法,:,除,2,取余,2,14,0,2,7,.0,2,2,2,3,.1,1,1,.1,0,28,余数,高位,低位,你能用算法步骤将,此算法描述出来吗,?,S1:,S2:,3.,算法的特性,一个有效算法应该具有以下特点,：,(1),有穷性。一个算法应包含有限的操作步骤，而不能是无限的。,(2),确定性。算法中的每一个步骤都应当是确定的，而不应当是含糊的、模棱两可的。,一个有效算法应该具有以下特点,：,(3),有零个或多个输入。所谓输入是指在执行算法时需要从外界取得必要的信息。,(4),有一个或多个输出。算法的目的是为了求解，“解”就是输出。,没有输出的算法是没有意义的。,(5),有效性。算法中的每一个步骤都应当能有效地执行，并得到确定的结果。,对于一般最终用户来说,:,他们并不需要在处理每一个问题时都要自己设计算法和编写程序,可以使用别人已设计好的现成算法和程序,只需根据已知算法的要求给予必要的输入，就能得到输出的结果,输入,3,个数,黑箱子,3,个数中最大数,求,3,个数的最大数,4.,怎样表示一个算法,常用的方法有：,自然语言,传统流程图,结构化流程图,伪代码,(1),用自然语言表示算法,(2),用流程图表示算法,(3),用,N-S,流程图表示算法,(4),用伪代码表示算法,(5),用计算机语言表示算法,(1),用自然语言表示算法,以上几个方面介绍的算法是用自然语言表示的,用自然语言表示通俗易懂，但文字冗长，容易出现歧义性,用自然语言描述包含分支和循环的算法，不很方便,除了很简单的问题外，一般不用自然语言,(2),用,流程图,表示算法,例,:,将,以下算法,用流程图表示。,求,1,2,3,4,5,如果需要将最后结果输出,:,1,t,i5,开始,2,i,t*i,t,i+1,i,结束,N,Y,(4),用伪代码表示算法,伪代码是用介于自然语言和计算机语言之间的文字和符号来描述算法,用伪代码写算法并无固定的、严格的语法规则，可以用英文，也可以中英文混用,例,:,求,5!,begin (,算法开始,),1,t,2,i,while i,5,t*i,t,i+1,i,print t,end (,算法结束,),(5),用计算机语言表示算法,要完成一项工作，包括设计算法和实现算法两个部分。,设计算法的目的是为了实现算法。,不仅要考虑如何设计一个算法，也要考虑如何实现一个算法。,例,:,（求,5!,）用,C,语言表示。,#include,int main(),int i,t;,t=1;,i=2;,while(i,输出,n,是素数,Y,N,通过以上例子可以看出流程图是表示算法的较好的工具,一个流程图包括以下几部分,：,(1),表示相应操作的框,(2),带箭头的流程线,(3),框内外必要的文字说明,流程线不要忘记画箭头，,否则,难以判定各框的执行次序,2.,三种基本结构和改进的流程图,的画法,1,）,.,传统流程图的弊端,传统的流程图用流程线指出各框的执行顺序，对流程线的使用没有严格限制,使用者可以毫不受限制地使流程随意地转来转去，使人难以理解算法的逻辑,2),三种基本结构,(1),顺序结构,A,B,(2),选择结构,A,B,Y,p,N,A,Y,p,N,(3),循环结构,当型循环结构,A,Y,p1,N,Y,x5,N,0,x,输出,x,的值,x+1,x,输出,1,2,3,4,5,直到型循环结构,A,Y,p2,N,Y,x5,N,0,x,输出,x,的值,x+1,x,输出,1,2,3,4,5,以上三种基本结构，有以下共同特点：,(1),只有一个入口,(2),只有一个出口,一个判断框有两个出口,一个选择结构只有一个出口,(3),结构内的每一部分都有机会被执行到。也就是说，对每一个框来说，都应当有一条从入口到出口的路径通过它,(4),结构内不存在“死循环”,由三种基本结构派生出来的结构：,A,N,p2,Y,B,根据表达式,p,的值进行选择,A,B,p=p1,p=p2,M,N,p=pm,p=pn,求质数（素数）,3.,三种基本结构流程图,的画法举例,例,例,程序设计方法学六,跨越源之识规律,创新根植辨短长,汪成为院士,11/22/2025,63,软件自动化的三个层次,软件自动化（自动程序设计）,广义：尽可能地借助计算机系统实现软件开发,狭义：从形式化的软件功能规范到可执行程序代码 这一过程的自动化,从软件需求规范,软件功能、性能规范的转换,解决从 “非形式”,“形式”,难度很大，寄希望于受限自然语言方面的突破,从软件功能、性能规范,软件设计,从“做什么”,“如何做“,从软件设计规范,高级语言,已有相当的进展，出现了许多工具,11/22/2025,64,1 概述,一、重要意义,软件发展中的问题：,整体功能不强、缺乏智能、质量欠佳、生产效率低,软件自动化是提高软件生产率的根本途径,软件自动化的前提是形式化,因此将形式化的理论和方法用于需求分析与规格说明是实现软件自动化的前提,11/22/2025,65,二、发展状况,有30多年,Dijkstra、Hoare程序验证,Scott、Stratchey 程序语义,形式化方法(Formal Method)：,通过严格的规范化的数学理论来描述软件系统“做什么”的方法。需要形式规范语言的支持。,形式规范语言：,提供了一个称为语法域的记号系统。一个称为语义域的目标集合，以及一组精确定义的哪些目标系统满足那个规范的规则。,11/22/2025,66,因此，形式化方法是在软件系统的开发过程中使用一种形式系统来表示模型的方法。,形式系统是二元组（,L,，,C,n,）,L,：语言（形式规范语言）,C,n,：对应关系，由推理规则构成,在软件规范方法方面的代表性成果有：,基于异调代数的代数方法,特点：用抽象代数中的公理化方法来刻画抽象数据类型中运算的性质，而不涉及数据的具体表示。,基本理论：代数语义,11/22/2025,67,抽象模型方法,特点：基于某些已知的,ADT,来给出待定义的,ADT,的抽象模型，用抽象模型来刻画待 定义的,ADT,中运算的功能。,基本理论：指称语义,状态机方法,特点：通过状态的转换来刻画输入与输出间的 关系,基本理论：操作语义,高阶软件方法（,HOS,）,基于控制公理,基本理论：公理语义,11/22/2025,68,在软件规范语言方面的代表性成果有：,一阶谓词演算组成语言,80,年代：,Z,语言、,Larch,语言、,VDM,语言,90,年代：面向实时及分布式的,LOTOS,语言、,面向对象的,Z,+,、,Object-Z,、,VDM,+,等,三、分类,基于模型的方法,给出系统（程序）状态和状态变换与操作的显式的表示但亦是抽象的定义，不涉及并发的行为。,如：,Z,、,VDM,11/22/2025,69,代数方法,通过联系不同的操作间的行为关系给出操作的隐式定义，未给出并发的显式表示。,如：,OBJ,、,Larch,过程代数方法,给出并发过程的一个显式模型，并通过过程间允许的可观察的通信上的限制来约束表示行为。,如：,CSP,（通信顺序进程）和,CCS,（通信系统计算）,基于逻辑的方法,采用逻辑来描述系统的特性，包括程序行为的低级规范和系统时间的行为规范。,如：时态逻辑、模态逻辑,11/22/2025,70,基于网络的方法,根据网络中的数据流显式地给出系统的并发模型，包括数据从一个结点流向另一个结点的条件。,如：,Petri,网、谓词变换网,11/22/2025,71,四、形式化软件开发方法,采用软件生命周期的变换模型，其实质是将现实世界的需求反映成软件的模型化过程。涉及三方面模型：现实世界，模型表示和计算机系统。因此开发的过程就是从三方面对系统进行描述和转换的过程。,开发过程中的任务为：,模型获取：从现实世界向模型表示的过程，涉及如何提取、表示模型。对应需求分析、设计等活动。,模型验证：对得到的模型表示进行检验，判断是否捕获了所有的需求，该模型是否具有所期望的特性。,模型变换：是向计算机系统变换的过程，关键的任务是一致性检测。对应实现和测试。,11/22/2025,72,三项任务分别对应三方面的活动：,1.,形式化规范（规格）：,软件规范是指对软件系统对象及用来对系统对象进行操作的方法的集合。以及对所开发系统中的各对象在生命周期间的集体行为的描述。,对应与软件生命周期的各个阶段，规范应该理解为是一个多阶段的行为。见例图,规范可以采用非、半形式化的方法来描述，形式化规范精确地描述了用户的需求、软件系统的功能及各种性质，其描述的是“做什么”，而不考虑“如何做”。因此，在理解、掌握形式规范语言和方法的基础上对所描述的系统的全面、深入的了解，给出恰如其分的描述上至关重要的。,11/22/2025,73,包含各规格阶段的生命周期模型例,需求分析,BS,SRD,系统设计,1,DS,系统设计,2,PS,软件开发,代码实现,软件测试,运行,SRD,：软件需求文档,BS,：行为规范,DS,：设计规范,PS,：程序规范,11/22/2025,74,软件系统规范的形式化方法,从形式化规范到目标软件系统的可实现和可执行角度，可分为三类：,操作类：此类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型执行而得到验证。如：有限状态机、,Statecharts,、,Petri,网等。,描述类：此类方法基于数学公理和概念，通过逻辑或代数给出系统状态空间，具有高度抽象的特点，便于通过自动工具进行验证。如：基于代数的,Z,、,VDM,、,Larch,等，基于逻辑的命题线性时态逻辑、一阶线性时态逻辑、计算树逻辑等。,双重类：此类方法兼具二者的特点，如：扩展状态机,/,实时时态逻辑等。,11/22/2025,75,形式化规范的成功案例,IBM,商用信息系统，牛津大学和,Hursley,实验室使用,Z,语言。总体成本降低,9,，获皇家技术成就奖。,Praxis,公司使用,VDM,开发的伦敦机场信息显示系统，软件质量大为提高，故障率,0.75(220),每,K,行代码。,其他领域：,数据库：,HP,医用仪器实时数据库系统,电子仪器：,Tektronix,系列谐波发生器,硬件：,INMOS,浮点处理器、,INMOS,中,T9000,系列虚拟信道处理器,运输系统：巴黎地铁自动火车保护系统、以色列机载航空电子软件等等,11/22/2025,76,形式化验证,软件开发中错误发现的越晚修改的代价越大，与传统方法不同的是形式化方法要求在完成形式规范后就进行形式验证。,形式验证主要技术包括模型检验和定理证明。,模型验证是一种基于有限状态机模型并检验该模型的期望特性的技术。即对模型的状态空间进行搜索，以确认该系统具有某些性质。终止性依赖于模型的有限性。优点是：完全自动化、速度快，可用于系统的部分规范。缺点是：“状态爆炸问题”因而极大地限制其实际使用范围。,有序二叉决策图（,Ordered Binary Decision Diagrams),是一种表述状态转移系统的高效率的方法。目前可以处理,100,200,个状态变量、状态数达,10,120,的系统。,11/22/2025,77,模型检验需要工具的支持，已有的工具有：,时态逻辑模型检验工具，如：,EMC,、,CESAR,、,SMV,、,Nurphi,、,SPIN,、,UV,等。,行为一致检验工具，如：,FRD,、,Cospan/Formal Check,等,复合检验工具，如：,HSIS,、,VIS,、,STcP,等,贝尔实验室用,FormalCheck,对其高级数据链路控制器进行验证，从,6,个性能的规范中发现一个失败，进而发现一个影响信道流量的,Bug,。,基于,SMV,输入语言建立了,IEEE Futurebus,896.1,1991,标准下,cache,一致协议精确模型，通过,SMV,的验证，发现了原先未找到和潜在的错误。此工作是第一次从,IEEE,标准中发现错误。,11/22/2025,78,定理证明采用逻辑公式来规范系统及其性质，这儿的逻辑由一个具有公理或推理规则的形式系统给出，进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。,定理证明可以处理无限状态空间问题，粗略地分为自动和交互两种类型，,自动定理证明系统是通用搜索过程，在解决各种组合问题中比较成功。,交互式定理证明系统需要与用户进行交互，要求用户能提供验证中创造性最强的部分（如断言等），因此效率较低，较难用于大系统的验证。,11/22/2025,79,现有的定理证明器有：,用户导引自动推理工具，如：,ACL2,，,Eves,、,LP,、,Nqthn,和,RRL,等它们由引理或定义序列导引，每一个定理采用已建立的推演、引理驱动重写和简化启发式来自动证明。,证明检验器，如：,Coq,、,HOL,、,LEGO,等。,复合证明器，如：,Analytica,中将定理证明和符号代数系统,Mathematica,复合，,PVS,和,Step,将决策过程，模型检验和交互式证明复合在一起。,基于符号代数运算的自动证明用于证明,Pentium,中,SRT,算法的正确性，查出了一个由故障商数字选择表引起的错误,。,11/22/2025,80,程序求精（又称程序变换）,是将自动推理和形式化方法相结合而形成的一门新技术，研究从抽象的形式规范推演出具体的面向计算机的程序代码的全过程。,基本思想是：用一个抽象程度低、过程性强的程序去替代一个抽象程度高、过程性弱的程序，并保持二者功能的一致性。这儿的“程序”是广义的“程序”，是对规范、设计文档、程序代码的统称。,按这种观点，程序开发的过程就是从最高层的程序开始，通过一系列的求精变换，每一次都降低一些抽象程度或增加一些可执行性，最终得到能指导计算机明确执行的程序代码。,11/22/2025,81,在进行求精的过程中必须要保证程序的正确性，即保证程序是满足最初的形式规范的。,程序的这种正确性可以通过求精过程中所遵循的一系列规则来保证，也可以采用验证工具来证明。,程序求精技术是形式化方法研究的一个热点，尽管目前真正用于实际软件开发过程中并不多，但是这是一个很重要的方向。,典型的方法有：,IBM Hursley,公司和牛津大学,PRG,程序设计研究组提出的针对,Z,规范的求精方法，,Carroll Morgan,的规则求精方案（见,Programming from Specifications,一书）。,11/22/2025,82,五、认识,形式化方法成长至今争议声不断，应正确地认识形式化方法，在结合到具体的软件开发过程时应考虑：,应用的类型，考虑问题领域的特点和模型的复杂性,规模和结构，较适应中等规模的系统，大型系统应考虑具有良好的结构,类型的选择，应从所确定的目标出发考虑采用的形式化方法的类型,形式化的级别，应先确定应用的关键程度、项目规模、可用资源等确定采用非、半或高度形式化的描述,11/22/2025,83,使用范围，尽管形式化可以适应所有的开发阶段，但通常应有选择的使用，对那些安全性、可信性要求高的构件应用高度的形式化,工具，工具的支持在形式化方法中具有重要的位置，应根据具体项目，综合上述因素选择合适的工具,11/22/2025,84,Hall,提出在形式化方法上的几个误区,事实上,形式化方法能保证软件是完全正确的,也可能出错,全部是程序证明,规范,只适用与安全要求很高的系统,有助于任何系统,要求有很好的数学基础,规范所需的数学是简单、容易的,增加了开发的费用,长远看，可降低费用,对用户来说是不可接收的,可帮助用户理解软件系统,未能应用于真正的大型软件开发中,每天都应用于工业项目中,11/22/2025,85,结论：形式化的方法不是灵丹妙药，而是一种改进系统可靠性的方法。,11/22/2025,86,2.基于代数方法的规范语言OBJ,该方法的理论工作由,Guttage,提出,基本格式：（语法定义、语义定义、限制说明）,语法定义指出类型的语法信息和检查信息,作用：定义了类型与函数,语义定义指出了类型和操作间的公理,作用：定义了类型的语义,限制说明给出各种限制，防止二义性,作用：和语义定义一起给出重写规则,基础抽象,是,整数集，函数定义,了,它们之间的相互关系,，这样,规范的值与函数形成一个抽象代数。,11/22/2025,87,形式定义：,代数规范是三元组（,S,、,、,E,）,其中：,S,、,是标记，,S,是类集，,是操作集，,E,是有限个方程的集合，形式为,L=R,，其中,L,、,R,S,，称为项。,项的定义,S,中的变元是项,常量是项,项经过操作集,中的操作后也是项,有工具支持的二个代数规范语言是：,AFFIRM,、,OBJ,11/22/2025,88,一OBJ简介,一种代数形式规范语言，最基本的概念是,ADT,（抽象数据类型），每个,ADT,描述一个客体。,具有很强的独立定义和数据抽象的机制。,支持层次化设计，即在定义高层,ADT,时可以使用下层已定义的,ADT,。,用,OBJ,书写形式规范的过程就是用代数等式（方程）定义,ADT,的过程。,是一种基于代数方程逻辑的代数形式语义，又具有一种基于把代数方程解释为重写规则的操作语义。（可利用这种语义证明程序的正确性）。,11/22/2025,89,二、基本形式,一个OBJ的形式规范说明是诸多ADT定义的集合，每个ADT具有如下形式：,关键字,含义,备注,obj,类型名,ADT,名用于高层定义,sorts,类型体,ADT,客体名,ops,运算符,定义域,值域,vars,变量定义,eqns,运算功能定义,=,jbo,描述结束符,其中,obj,与,jbo,是必须的，其余部分任选。,11/22/2025,90,例,1,定义,ADT NATURAL,obj NATURAL,sorts nat,ops,0,:,nat /*0,无定义域，常量*,/,succ(-):nat,nat /*nat,上的一目运算，,-,表示运算对象 *,/,jbo,在定义,ADT,时若需要用到低层已定义,ADT L,中的运算，可在,obj,处用,/L,指出，多个时用空格分隔。,例子,11/22/2025,91,例,2.,在,NATURAL,的基础上定义,ADD,obj ADD/NATURAL,ops -+-:nat nat,nat,vars x,y:nat,eqns (0+x=x),(succ(x)+y=succ(x+y),jbo,下面将给出一个较大的形式规范定义,对整数序列进行分类。在规范中自底向上的顺序分别定义了多个,ADT,。如：,Boolean,、,Integer,、,seq_INT,、,sort_seq_INT,等。,11/22/2025,92,例,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,11/22/2025,93,2.,整型,ADT/,对下述十个运算的规则容易给出，故省略了,objInteger/Boolean,sortsINT,ops-,-,:INT,INT,-+-:INT INT,INT,-,-,-:INT INT,INT,-*-:INT INT,INT,-div-:INT INT,INT,-mod-:INT INT,INT,-:INT INT,Boolean,-=-:INT INT,Boolean,jbo,11/22/2025,94,3.,定义整型字符串,ADT,obj seq_INT/Integer,sorts seq_INT,ops:,seq_INT /,空,-:,seq_INT /,常量,-,-:seq_INT seq_INT,seq_INT /,链接,hd-:seq_INT,INT /,头元素,tl-:seq_INT,seq_INT /,尾串,len-:seq_INT,INT /,长度,varsi:INT s:seq_INT,11/22/2025,95,eqns (,s=s),(s,=s),(hd=0),(hdi=i),(hd(i,s)=i),(tl=),(tli=),(tl(i,s)=s),(len=0),(len s=succ(len(tl s)if s),jbo,11/22/2025,96,4,定义比较,ADT,objsort_seq_split/seq_INT Integer,ops -=-:seq_INT,INT,seq_INT,varss:seq_INTi,x:INT,eqns(x=),(i=x),(ix=i if ix),(i,s)=x),(i,s)x=i,sx if i=x=),(i=x=if i=x=i,(s=x)if i=x),jbo,11/22/2025,97,5,定义分类,ADT,的规范,obj sort_seq_INT/sort_seg_split seq_INT Integer Boolean,opssort-:seq_INT,seq_INT,is_sorted-:seq_INT,Boolean,varss,s1,s2:seq_INT i,j,x:INT,eqns,(is_sorted=T),(is_sortedi=T),(is_sortedi,j=i=j),(is_sortedi,j,s=ij),(sort(i,j),s=sort(j,i,s)if ij),(sort(s,i,j)=sort(s,j,i)if ij),(sort(s1,i,j,s2)=sort(s1,j,i,s2 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,11/22/2025,99,三、运算的性质,从功能上可以将运算分为四类：,初始化运算,不以任何别的类型客体作为它的输入，其结果是具有自身类型的值。如：,seq_INT-,2,.,构造运算,以自身类型客体和别的类型客体为输入，产生具有自身类型的结果。如：,-,-,3.,修改运算,修改自身类型客体的变量如：,tl,4.,观察运算,以自身类型客体为输入，得出具有别的类型客体的结果。,如：,len,11/22/2025,100,四、抽象的计算程序,例,4,定义自然数类型的栈运算的,ADT,objStack/Integer Boolean,sortsstack,ops,create:,stack/*,空栈*,/,push-:stack INT,stack,pop-:stack,stack,top-:stack,INTERR,empty-:stack,Boolean,11/22/2025,101,varss:stackn:INT,eqns,(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,11/22/2025,102,抽象计算程序的计算可以归结为代数系统中的重写规则的应用，而得到计算的结果。,例,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(s,5)=5,由此可知，这种方法可以机械执行。,11/22/2025,103,正确性证明,依赖相应的,ADT,中定义的运算规范，可以证明程序的正确性。方法为：将代数等式视为重写规则，即将等式,L=R,视为,L,R,（,L,被定义为,R,）。就可以用于程序的正确性证明。,11/22/2025,104,3.,基于模型方法的规范语言,VDM,The Vienna Development Method,一、概况,VDM,由,IBM,的,Vienna,实验室,20,世纪,70,年代提出的的一种形式化方法。最初是为了解决用形式化方法来开发编译系统，使语言的语法、语义的定义更为严格、更加系统化（如实现,PL/1,语言的语义规范）。当时用,VDL,用于语言的注释。得到广泛的应用,VDM,在欧洲得到发展，从,70,年代末到,90,年代在欧美许多研究机构和大学得到广泛的应用（如曼彻斯特大学讲其作为必修课），以后逐渐称为一般的软件开发方法。,11/22/2025,105,1996,年国际标准化组织（,ISO,）制定了,VDM,的国际化版本,VDM,SL,（,VDM Specification Language),。目前,VDM,已称为应用最为广泛的形式化规范语言。,VDM,是一种功能构造性规范技术。由一阶谓词逻辑和已经建立的,ADT,来描述每个运算或函数的功能。基本思想是,ADT,、数学概念和符号来规定运算或函数的功能，而且这种规定的过程是结构化的，其目的是要在系统实现之前简单而又明确地指出软件系统要完成的功能。,支持程序正确性的证明。用,Hoare,的前,/,后断言描述运算的规范。,11/22/2025,106,二、VDM的形式规范的基本组成形式,VDM,形式规范由三部分组成：,状态、类型不变式、运算功能,是一种基于抽象模型的方法，由：,表示（数据）抽象,系统的状态描述 和,运算（操作）抽象,用前,/,后断言 所组成。,模型规范的形式定义：,M=(,，,0,，,),是,M,的状态集（含有不变式）,0,是初始状态,是运算集合,其实质是将软件系统视为基本状态的运算类型。,11/22/2025,107,1、系统状态规则,基本形式：类型,ID=,类型定义实体,其中：,ID,是新定义的一个类型名,实体是基本类型定义的一个新类型。,基本类型：,基本型：,N,R,B(,自然数，实数，,Boolean),运算是常见的算术和逻辑运算,集合型：形式为：,X=set of Q,Q,是已定义类型或基本类型，,X,是集合型,ID,运算有：并（,）、交（,）、差（,/,）、元素个数（,card,）、属于（,）、子集（,）、真子集（,）等,11/22/2025,108,表型：有序集合，每个元素有确定位置，可重复出现，定义形式为：,S=seq of Q,S,为新类型的,ID,，,Q,为,S,的元素类型,运算有：求头（,hd,）、求尾（,tl),、长度（,len),、连接（,conj,）、元素集（,elem),、索引集（,inds),等,映射：有限、可列集的一个函数，通常以对偶集合形式表示，定义形式为：,M=Map of Q,M,为新类型的,ID,，,Q,为,M,的元素类型,运算有：求定义域（,dom,），求值域（,rng,）,限定定义域（），定义域元素删除（）等,11/22/2025,109,复合型：,P=Compose P of,e,1,:Q,1,e,2,:Q,2,end,P,为新类型的,ID,，,e,i,、,Q,i,（,i=1,）分别为,P,的分量名和分量类型,运算：求复合类型值（,mk_P,）、改变分量值、求分量的值。,11/22/2025,110,例一个教师职称提升系统的ADT定义,Studentdata=Compose Studentdata of,Name:String,T_score_list:Seq of Choice,end,Researchdata=Compose Researchdata of,Name1:String,R_Score_List:Seq of N,end,Teacher=Compose Teacher of,T_name:String,T_score:R,R_score:R,end,11/22/2025,111,2、类型不变式规则,类型不变式是指对状态规则中规定的类型给出其应满足的性质。,表示形式：,设,ST,是在类型规范中所定义的一个类型,ID,。,Inv_ST(S)=P(S),其中：,P(S),是一个一阶谓词公式，,S,ST,，即,ST,中任一元素,S,应满足的条件,例,2.,例,1,中,ADT Studentdata,描述了对一个教师的评价：,Inv_Studentdata,mk_Studentdata(n,t),S,tudentdata.n,t,Inv_Choice,t,C,hoicelen t=4,11/22/2025,112,3、运算功能规则,运算功能规则,VDM,形式规范中的主要形式，其一般形式为：,OP,（,m,1,:Tm,1,m,2,:Tm,2,m,n,:Tm,n,）,r,1,:Tr,1,r,e,Tr,e,extP V,1,:Tv,1,P V,k,:Tv,k,pre C,1,/C,1,表示为（,m,j,r,k,),post C,2,/C,2,表示为（,m,j,V,i,r,k,V,i,),其中：,OP,是运算名，,m,i,是输入参量，,r,i,是输出参量，,ext,表示,V,i,外部量；,P,wr,rd,，表示可读或可写；,pre,是前置谓词，,post,是后置谓词。,注：,V,i,是执行,OP,前状态值，,V,i,是执行,OP,后状态值。,11/22/2025,113,例3简单计算器规范,reg:N/,初始时外部变量,reg=0,LOAD(i:N),ext wr reg:N,pre true,post reg=i,SHOW()r:N,ext rd reg:N,pre true,post r=reg,11/22/2025,114,ADD(i:N),ext wr reg:N,pre true,post reg=reg+i,DIVIDE(d:N)r:N,ext wr reg:N,pre d0,post d*r+reg=reg,0,reg t ,Inv_Researchdata,mk_Researchdata(n,r),Researchdata.n =r ,Inv_choice,t,choice.len t=4,11/22/2025,122,函数及运算,Teacher_Promotion(tsl:Studentdata_list,rsl:Researchdata_list,m,：,N)P:Teacher_list,ext wr output:Teacher_list,Pre len tsl=len rsl,i,inds tsl.name(tsli)=name1(rsli),/*,教学、科研二个表中名字相同*,/,Post P=Get_Persons(Teacher_order,(Teacher_list_production(ts1,rs1),m),output=output conj P,11/22/2025,123,/*,从已排序的教师序列表,td,中取出总成绩最高的,n,位教师，从高到低次序放入,tt,表中*,/,Get_Persons(td:Teacher_order_list,n:N),tt:Teacher_list,Pre td len tdn,i,j,inds td i,total_score(tdi)total_score(tdj),Post len tt=nelem tt,elem td,i,jidns tt i,total_score(tti)total_score(ttj),x,elem tt,y,elem td/elem tt total_score(x)total_score(y),11/