软件形式化方法第1章 绪论

第章 绪论,1.1 形式化方法概述 1.2 软件开发中的形式化方法,什么是形式化方法？,“形式化”是相对“非形式化”或“半形式化”而言的一种分析问题、解决问题的思维方法。 “形式化”是为了获得对问题(研究对象)的本质(逻辑的或数学的)认识，将问题(研究对象)从形形色色的具体背景中抽象出来，加以纯粹“符号化”以及严格“数学化”处理的思维方法和过程。,什么是形式化方法？,”形式化”可以定义为: 完全彻底的 抽象化+符号化+公理化 思维的过程,返 回,什么是形式化方法？,形式化方法是按照严格的数学逻辑规范对问题(研究对象)的本质进行形式化的抽象、定义、描述、建模、推理和验证等一整套理论和方法的总称。,形式化方法的起源,形式化方法的起源与现代逻辑学、语言学以及数学基础等领域的发展有着十分密切的关系。 我们知道，逻辑上的严密性和表达上的简洁性，即避免出现所谓的逻辑悖论和不必要的冗余，是任何现代科学理论体系都不可或缺的生命力和价值所在。 形式化方法的正是为了追求上述领域理论体系的严密性和简洁性而逐步发展起来的。 随着现代科学技术的发展，形式化已成为许多学科领域，特别是数学和计算科学中最基本的研究方法和科学规范。,形式化方法的特征,研究手段：高度抽象 表现形式：完全符号化 表达方式：高度简洁 内部过程：严格精确 方法结果：普遍适用,高度的抽象性,抽象是任何一门科学乃至全部人类思维都具有的基本特性，然而，形式化方法的抽象程度远远超过自然科学中的一般抽象。 其最大特点在于将现实事物从形形色色的具体背景中抽取出来，而仅仅以“纯符号化”的形式加以表现。,返 回,逻辑的严密性,形式化方法的高度抽象性和逻辑的严密性紧密相关。 若没有逻辑的严密性，在自身理论中矛盾重重，漏洞百出，那么用形式化方法对问题(研究对象)进行抽象就失去了意义。 正是由于形式化方法的逻辑严密性，我们在运用形式化方法解决问题时，只有严格遵守形式逻辑的基本法则，才能保证结论的正确性和可靠性。,返 回,结果的普遍适用性,形式化方法的高度抽象性和逻辑的严密性决定了其结果的普遍适用性。,返 回,形式化方法的作用,为系统开发提供精确简洁的形式化语言。 为系统开发提供严格规范的形式化模型。 为系统开发提供有效的逻辑推理工具。,返 回,形式化理论,形式化理论是由基本概念、基本原理或定律（联系这些概念的判断）以及由这些概念与原理逻辑推理出来的结论组成的体现，可以形式化地定义为： T= 其中： T表示理论； C表示基本概念的集合； P表示基本原理或定律的集合； S表示由这些概念与原理逻辑推理出来的结论的集合。,公理化方法,公理化方法，是一种构造理论体系的演绎方法，它是从尽可能少的基本概念、公理出发，运用演绎推理规则，推出一系列的命题，从而建立整个理论体系的思想方法。,公理化方法,用公理化构建的理论体系称为公理系统，公理系统需要满足无矛盾性、独立性和完备性等3个条件： （1）无矛盾性：这是公理系统的基本要求，即不允许在一个公理系统中出现相互矛盾的命题，否则这个公理系统就没有价值。 （2）独立性：公理系统中的所有的公理都必须是独立的，即任何一个公理都不能从其他公理推导出来。 （3）完备性：公理系统必须是完备的，即从公理系统出发，能推出（或判定）该领域所有的命题。,公理化方法,为了保证公理系统的无矛盾性和独立性，一般要尽可能使公理系统简单化。 简单化将使无矛盾性和独立性的证明成为可能。 简单化也是科学研究追求的目标之一。,具体公理系统和抽象公理系统,在欧氏几何公理系统中，原始概念（点、线、面）和所有的公理都有直观的背景或客观的意义，像这样有现实世界背景的公理系统，一般被称为具体公理系统。 由于非欧几何的出现，使人们感到具体公理系统过于受直觉的局限。 因而，在19世纪末和20世纪初，一些数学家和逻辑学家开始了对抽象公理系统的研究。,具体公理系统和抽象公理系统,在抽象公理系统中，原始概念的直觉意义被抽象掉，甚至没有任何预先设定的意义，而公理也无需以任何实际意义为背景，它们无非是一些形式约定的符号串。 这使得抽象公理系统可以有多种解释。,具体公理系统和抽象公理系统,例如，形式化的运算规则1+1可以解释为一个苹果加一个苹果，或者为一本书加一本书。 布尔代数抽象公理系统可以解释为有关命题真值的命题代数，或者有关电路设计研究的开关代数。 在这些解释中，抽象符号X可以分别被看作“命题X”、“电路X”等，“0”和“1”分别被用于表示命题的“假”和“真”，或者电路的“开”和“闭”。,在欧几里德的几何原本中，用公理化方法对当时的数学知识（平面几何）作了系统化、理论化的总结。 他以点、线、面为原始概念，以5条公设和5条公理为原始命题，给出了平面几何中的119个定义，465条命题及其证明，构成了历史上第一个数学公理体系。,下一页,例：平面几何（欧氏几何）的 公理化概括,原始概念： 点、线、面 原始命题（公设）： 公设1：两点之间可作一条直线； 公设2：一条有限直线可不断延长； 公设3：以任意中心和直径可以画圆； 公设4：凡直角都彼此相等； 公设5：在平面上，过给定直线之外的一点，存在且仅存在一条平行线，即所谓的“平行公设（公理）,下一页,例：平面几何（欧氏几何）的 公理化概括,原始命题（公理）： 公理1：等于同量的量彼此相等 公理2：等量加等量，和相等 公理3：等量减等量，差相等 公理4：彼此重合的图形全等 公理5：整体大于部分,返 回,例：平面几何（欧氏几何）的 公理化概括,公理化方法在计算学科中的应用,公理化方法主要用于计算学科理论形态方面的研究。 在计算学科各分支领域，均采用了公理化方法，如: 形式语义学 关系数据库理论 计算认知领域 ,形式化系统,任何按照形式化思想建立的具有“符号化”和“公理化”特征的抽象系统都可以称为形式化系统。,下一页,形式化系统,一个形式化系统一般由下面几个部分组成： 初始符号：初始符号不具有任何意义。 形式规则：形式规则规定一种程序，借以判定哪些符号串是本系统中的公式，哪些不是。 公理：即在本系统的公式中，确定不加推导就可以断定的公式集。 变形规则：变形规则亦称演绎规则或推导规则。变形规则规定，从已被断定的公式，如何得出新的被断定公式，被断定的公式又称为系统中的定理。,下一页,在以上4个组成部分中，前两个部分定义了一个形式语言，后两个部分在该形式语言上定义了一个演绎结构。 形式化系统由形式语言和定义于其上的演绎结构组成。,返 回,形式化系统,从某种意义上讲，任何计算机系统软硬件都是一种形式化系统，它们的结构可以用形式化方法描述。 程序设计语言也是一种形式语言系统。,返 回,形式化系统,抽象性 抽象是人们认识客观世界的基本方法，虽然抽象性并不是形式化系统的专利，但形式化系统具有更强的抽象性。,返 回,形式化系统的基本特点,符号化 形式化系统的抽象性表现在它自身仅仅是一个符号系统，除了表示符号间的关系（字符号串的变换）外，不表示任何别的意义。,返 回,形式化系统的基本特点,形式化系统的基本特点,严格性 形式化系统中，任何初始符号和推导过程都要进行严格的定义。 机械化 形式化系统采用的是一种纯形式的机械方法，因此它的严格性高于一般的数学推导。,下一页,形式化方法的局限性,形式化方法并不是“完美无缺”的“灵丹妙药”。 可以证明，任何一个形式化系统，如果它是无矛盾的，那么，它就具有下面两个局限性。,下一页,形式化方法的局限性,不完备性 1931年，哥德尔提出的关于形式化系统的“不完备性定理”，指出：如果一个形式的数学理论是足够复杂的（复杂到所有的递归函数在其中都能够表示），而且它是无矛盾的，那么在这一理论中必存在一个语句，这一语句在这一理论中既不能证明，也不能否证。,下一页,31,哥德尔不完备定理,哥德尔不完备定理是库尔特·哥德尔（Kurt Gödel 19061978）于1931年证明并发表的两条定理。 第一定理： 任何一个相容的数学形式化理论中，只要它强到足以蕴涵皮亚诺算术公理，就可以在其中构造在体系中既不能证明也不能否证的命题。 第二定理： 任何相容的形式体系不能用于证明它本身的相容性。,32,歌德尔不完全定理对认知科学哲学的影响,哥德尔不完备定理的结论影响了数学哲学以及形式化主义（使用形式符号描述原理）中的一些观点。 我们可以将第一定理解释为：“我们永远不能发现一个万能的公理系统，能够证明一切数学真理，而不能证明任何谬误。” 我们可以将第一定理解释为：“如果一个（强度足以证明基本算术公理的）公理系统可以用来证明它自身的相容性，那么它就是不相容的。”,不可判定性 如果对一类语句C而言，存在一个算法AL，使得对C中的任一语句S而言，可以利用算法AL来判定其是否成立，则C称为可判定的，否则，称为不可判定的。 著名的“停机问题”就是一个不可判定性的问题。该问题是指一个任给的图灵机对于一个任给的输入而言是否停机的问题，图灵证明了这类问题是不可判定的。 计算机系统是一种形式化系统，因此，计算机系统一样也具有形式化系统的局限性。,返 回,形式化方法的局限性,形式化与公理化,形式化不一定导致公理化，公理系统也不一定是形式系统。 如欧氏几何公理系统就不是形式系统。 形式化与公理化虽然不同，但在近代数学中，形式系统大都是形式化的公理系统。,第章 绪论,1.1 形式化方法概述 1.2 软件开发中的形式化方法,计算机软件一般指计算机系统中的程序及文档 程序:以计算机语言表达的软件系统 文档:以人类语言(自然的或形式化的)表达的软件系统 二者互相配合共同构成了完整的软件系统 人类的经验、抽象知识正逐步由软件予以精确地体现,什么是软件？,万物皆数?,通过软件，人们可以对其所认识到的任何一种事物进行“编码”。 以产生它的一个数字化的虚拟“实例”。,软件本质：逻辑产品,理论基础： Universal TM（图灵机） von Neumann architecture PL virtual machines,软件 是人类脑力劳动的产物 是系统逻辑的体现 但又必须依附于一定的载体 例如：纸张、软盘、硬盘、光盘等 其它物品呢？需不需要载体？ 理解软件的关键是什么？,软件本质：逻辑产品,软件作为逻辑产品的特点： 优势： 易于变化，适应性强 复制成本低，适合规模经济 劣势： 不易被理解 容易出错 找错、排错困难,软件本质：逻辑产品,41,软件开发过程,软件开发 把现实世界的需求模型化成软件并予以实现的过程 软件开发的主要步骤（大致，有不同说法）： 问题和需求分析 设计： 功能设计 结构设计 编码（构建） 调试 发布、维护和升级,人们在实践中提出了许多开发模型：如传统的瀑布模型，较新近的有快速原型、迭代式开发模型等等,-42-,软件开发的历史,软件开发的三个阶段 程序设计阶段（1946年-1956年） 科学计算、机器语言及汇编语言、个体编程 编程技巧、程序效率 没有文档、软件一词尚未出现 程序系统阶段（1956年-1968年） 1956年，J.Backus Fortran语言诞生 大量数据处理、小组开发 “软件”一词出现：程序及其说明 60年代中期，软件危机。 软件工程阶段（1968年以来） 1968年NATO会议，提出“软件工程”术语 工程化方法、描述语言、团队开发,43,软件开发：实际情况,软件开发的实际情况并不乐观。 项目经常延误，预算经常超支。 开发的后续阶段常发现许多前期设计错误，更正的代价高昂。 发布运行的软件中常常存在着许多错误，时常崩溃 软件维护和更新工作的代价很高。,44,软件开发：实际情况,Therac-25 放射线治疗仪 1985-87 年 过量辐射 (6 个死亡 / 截肢)！,45,软件开发：实际情况,航空器控制系统 功能错误 (飞机撞毁)！,46,软件的本质问题,复杂性 规模：成万、成百万、甚至成千万行代码 系统组成部分之间异常复杂的直接与间接相互作用 静态结构与动态性质之间难以把握的复杂关系 不确定性/多变性 需求的不断提升和变化 异常丰富多彩的应用需求 困境 要求较低的开发成本