软件形式化方法第1章-绪论ppt课件.ppt

《软件形式化方法第1章-绪论ppt课件.ppt》由会员分享，可在线阅读，更多相关《软件形式化方法第1章-绪论ppt课件.ppt（105页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、第章绪论第章绪论1.1 形式化方法概述形式化方法概述1.2 软件开发中的形式化方法什么是形式化方法？什么是形式化方法？“形式化形式化”是相对是相对“非形式化非形式化”或或“半形半形式化式化”而言的一种分析问题、解决问题而言的一种分析问题、解决问题的思维方法。的思维方法。“形式化形式化”是为了获得对问题是为了获得对问题(研究对象研究对象)的本质的本质(逻辑的或数学的逻辑的或数学的)认识，将问题认识，将问题(研究对象研究对象)从形形色色的具体背景中抽象从形形色色的具体背景中抽象出来，加以纯粹出来，加以纯粹“符号化符号化”以及严格以及严格“数学化数学化”处理的思维方法和过程。处理的思维方法和过程。什

2、么是形式化方法？什么是形式化方法？”形式化形式化”可以定义为可以定义为: 完全彻底的完全彻底的 抽象化抽象化+符号化符号化+公理化公理化 思维的过程思维的过程返 回什么是形式化方法？什么是形式化方法？形式化方法是按照严格的数学逻辑规范形式化方法是按照严格的数学逻辑规范对问题对问题(研究对象研究对象)的本质进行形式化的抽的本质进行形式化的抽象、定义、描述、建模、推理和验证等象、定义、描述、建模、推理和验证等一整套理论和方法的总称。一整套理论和方法的总称。形式化方法的起源形式化方法的起源 形式化方法的起源与现代逻辑学、语言学以及数形式化方法的起源与现代逻辑学、语言学以及数学基础等领域的发展有着十分

3、密切的关系。学基础等领域的发展有着十分密切的关系。 我们知道，逻辑上的严密性和表达上的简洁性，我们知道，逻辑上的严密性和表达上的简洁性，即避免出现所谓的逻辑悖论和不必要的冗余，是即避免出现所谓的逻辑悖论和不必要的冗余，是任何现代科学理论体系都不可或缺的生命力和价任何现代科学理论体系都不可或缺的生命力和价值所在。值所在。 形式化方法的正是为了追求上述领域理论体系的形式化方法的正是为了追求上述领域理论体系的严密性和简洁性而逐步发展起来的。严密性和简洁性而逐步发展起来的。 随着现代科学技术的发展，形式化已成为许多学随着现代科学技术的发展，形式化已成为许多学科领域，特别是数学和计算科学中最基本的研究科

4、领域，特别是数学和计算科学中最基本的研究方法和科学规范。方法和科学规范。形式化方法的特征形式化方法的特征研究手段：高度抽象研究手段：高度抽象表现形式：完全符号化表现形式：完全符号化表达方式：高度简洁表达方式：高度简洁内部过程：严格精确内部过程：严格精确方法结果：普遍适用方法结果：普遍适用高度的抽象性高度的抽象性抽象是任何一门科学乃至全部人类思维抽象是任何一门科学乃至全部人类思维都具有的基本特性，然而，形式化方法都具有的基本特性，然而，形式化方法的抽象程度远远超过自然科学中的一般的抽象程度远远超过自然科学中的一般抽象。抽象。其最大特点在于将现实事物从形形色色其最大特点在于将现实事物从形形色色的具

5、体背景中抽取出来，而仅仅以的具体背景中抽取出来，而仅仅以“纯纯符号化符号化”的形式加以表现。的形式加以表现。返 回逻辑的严密性逻辑的严密性形式化方法的高度抽象性和逻辑的严密形式化方法的高度抽象性和逻辑的严密性紧密相关。性紧密相关。若没有逻辑的严密性，在自身理论中矛若没有逻辑的严密性，在自身理论中矛盾重重，漏洞百出，那么用形式化方法盾重重，漏洞百出，那么用形式化方法对问题对问题(研究对象研究对象)进行抽象就失去了意义。进行抽象就失去了意义。正是由于形式化方法的逻辑严密性，我正是由于形式化方法的逻辑严密性，我们在运用形式化方法解决问题时，只有们在运用形式化方法解决问题时，只有严格遵守形式逻辑的基本

6、法则，才能保严格遵守形式逻辑的基本法则，才能保证结论的正确性和可靠性。证结论的正确性和可靠性。返 回结果的普遍适用性结果的普遍适用性形式化方法的高度抽象性和逻辑的严形式化方法的高度抽象性和逻辑的严密性决定了其结果的普遍适用性。密性决定了其结果的普遍适用性。返 回形式化方法的作用形式化方法的作用 为系统开发提供精确简洁的形式化语言。为系统开发提供精确简洁的形式化语言。 为系统开发提供严格规范的形式化模型。为系统开发提供严格规范的形式化模型。 为系统开发提供有效的逻辑推理工具。为系统开发提供有效的逻辑推理工具。返 回形式化理论形式化理论形式化理论是由基本概念、基本原理或定律（联形式化理论是由基本概

7、念、基本原理或定律（联系这些概念的判断）以及由这些概念与原理逻辑系这些概念的判断）以及由这些概念与原理逻辑推理出来的结论组成的体现，可以形式化地定义推理出来的结论组成的体现，可以形式化地定义为：为： T=其中：其中：T表示理论；表示理论；C表示基本概念的集合；表示基本概念的集合；P表示基本原理或定律的集合；表示基本原理或定律的集合；S表示由这些概念与原理逻辑推理出来的结论的集合。表示由这些概念与原理逻辑推理出来的结论的集合。公理化方法公理化方法 公理化方法，是一种构造理论体系的演绎公理化方法，是一种构造理论体系的演绎方法，它是从尽可能少的基本概念、公理方法，它是从尽可能少的基本概念、公理出发，

8、运用演绎推理规则，推出一系列的出发，运用演绎推理规则，推出一系列的命题，从而建立整个理论体系的思想方法。命题，从而建立整个理论体系的思想方法。公理化方法公理化方法用公理化构建的理论体系称为公理系统，公理系用公理化构建的理论体系称为公理系统，公理系统需要满足无矛盾性、独立性和完备性等统需要满足无矛盾性、独立性和完备性等3个条个条件：件：（1）无矛盾性：这是公理系统的基本要求，即不）无矛盾性：这是公理系统的基本要求，即不允许在一个公理系统中出现相互矛盾的命题，否允许在一个公理系统中出现相互矛盾的命题，否则这个公理系统就没有价值。则这个公理系统就没有价值。（2）独立性：公理系统中的所有的公理都必须是

9、）独立性：公理系统中的所有的公理都必须是独立的，即任何一个公理都不能从其他公理推导独立的，即任何一个公理都不能从其他公理推导出来。出来。（3）完备性：公理系统必须是完备的，即从公理）完备性：公理系统必须是完备的，即从公理系统出发，能推出（或判定）该领域所有的命题。系统出发，能推出（或判定）该领域所有的命题。公理化方法公理化方法为了保证公理系统的无矛盾性和独立性，为了保证公理系统的无矛盾性和独立性，一般要尽可能使公理系统简单化。一般要尽可能使公理系统简单化。简单化将使无矛盾性和独立性的证明成为简单化将使无矛盾性和独立性的证明成为可能。可能。简单化也是科学研究追求的目标之一。简单化也是科学研究追求

10、的目标之一。具体公理系统和抽象公理系统具体公理系统和抽象公理系统 在欧氏几何公理系统中，原始概念（点、线、在欧氏几何公理系统中，原始概念（点、线、面）和所有的公理都有直观的背景或客观的意面）和所有的公理都有直观的背景或客观的意义，像这样有现实世界背景的公理系统，一般义，像这样有现实世界背景的公理系统，一般被称为具体公理系统。被称为具体公理系统。 由于非欧几何的出现，使人们感到具体公理系由于非欧几何的出现，使人们感到具体公理系统过于受直觉的局限。统过于受直觉的局限。 因而，在因而，在19世纪末和世纪末和20世纪初，一些数学家和世纪初，一些数学家和逻辑学家开始了对抽象公理系统的研究。逻辑学家开始了

11、对抽象公理系统的研究。具体公理系统和抽象公理系统具体公理系统和抽象公理系统 在抽象公理系统中，原始概念的直觉意义在抽象公理系统中，原始概念的直觉意义被抽象掉，甚至没有任何预先设定的意义，被抽象掉，甚至没有任何预先设定的意义，而公理也无需以任何实际意义为背景，它而公理也无需以任何实际意义为背景，它们无非是一些形式约定的符号串。们无非是一些形式约定的符号串。 这使得抽象公理系统可以有多种解释。这使得抽象公理系统可以有多种解释。具体公理系统和抽象公理系统具体公理系统和抽象公理系统例如，形式化的运算规则例如，形式化的运算规则1+1可以解释为一个苹可以解释为一个苹果加一个苹果，或者为一本书加一本书。果加

12、一个苹果，或者为一本书加一本书。布尔代数抽象公理系统可以解释为有关命题真值布尔代数抽象公理系统可以解释为有关命题真值的命题代数，或者有关电路设计研究的开关代数。的命题代数，或者有关电路设计研究的开关代数。在这些解释中，抽象符号在这些解释中，抽象符号X可以分别被看作可以分别被看作“命命题题X”、“电路电路X”等，等，“0”和和“1”分别被用于表分别被用于表示命题的示命题的“假假”和和“真真”，或者电路的，或者电路的“开开”和和“闭闭”。 在欧几里德的在欧几里德的几何原本几何原本中，用公理化方中，用公理化方法对当时的数学知识（平面几何）作了系统法对当时的数学知识（平面几何）作了系统化、理论化的总结

13、。化、理论化的总结。 他以点、线、面为原始概念，以他以点、线、面为原始概念，以5条公设和条公设和5条公理为原始命题，给出了平面几何中的条公理为原始命题，给出了平面几何中的119个定义，个定义，465条命题及其证明，构成了历史上条命题及其证明，构成了历史上第一个数学公理体系。第一个数学公理体系。下一页例：平面几何（欧氏几何）的例：平面几何（欧氏几何）的公理化概括公理化概括原始概念：原始概念：n点、线、面点、线、面原始命题（公设）：原始命题（公设）：n公设公设1：两点之间可作一条直线；：两点之间可作一条直线；n公设公设2：一条有限直线可不断延长；：一条有限直线可不断延长；n公设公设3：以任意中心和

14、直径可以画圆；：以任意中心和直径可以画圆；n公设公设4：凡直角都彼此相等；：凡直角都彼此相等；n公设公设5：在平面上，过给定直线之外的一点，存在且仅：在平面上，过给定直线之外的一点，存在且仅存在一条平行线，即所谓的存在一条平行线，即所谓的“平行公设（公理）平行公设（公理）下一页例：平面几何（欧氏几何）的例：平面几何（欧氏几何）的公理化概括公理化概括原始命题（公理）：原始命题（公理）：u公理公理1：等于同量的量彼此相等：等于同量的量彼此相等u公理公理2：等量加等量，和相等：等量加等量，和相等u公理公理3：等量减等量，差相等：等量减等量，差相等u公理公理4：彼此重合的图形全等：彼此重合的图形全等u

15、公理公理5：整体大于部分：整体大于部分返 回例：平面几何（欧氏几何）的例：平面几何（欧氏几何）的公理化概括公理化概括公理化方法在计算学科中的应用公理化方法在计算学科中的应用 公理化方法主要用于计算学科理论形态方公理化方法主要用于计算学科理论形态方面的研究。面的研究。 在计算学科各分支领域，均采用了公理化在计算学科各分支领域，均采用了公理化方法，如方法，如: 形式语义学形式语义学 关系数据库理论关系数据库理论 计算认知领域计算认知领域 形式化系统形式化系统任何按照形式化思想建立的具有任何按照形式化思想建立的具有“符号符号化化”和和“公理化公理化”特征的抽象系统都可特征的抽象系统都可以称为形式化系

16、统。以称为形式化系统。下一页形式化系统形式化系统 一个形式化系统一般由下面几个部分组成：一个形式化系统一般由下面几个部分组成：1. 初始符号：初始符号不具有任何意义。初始符号：初始符号不具有任何意义。2. 形式规则：形式规则规定一种程序，借以判定哪些符形式规则：形式规则规定一种程序，借以判定哪些符号串是本系统中的公式，哪些不是。号串是本系统中的公式，哪些不是。3. 公理：即在本系统的公式中，确定不加推导就可以断公理：即在本系统的公式中，确定不加推导就可以断定的公式集。定的公式集。4. 变形规则：变形规则亦称演绎规则或推导规则。变形变形规则：变形规则亦称演绎规则或推导规则。变形规则规定，从已被断

17、定的公式，如何得出新的被断定规则规定，从已被断定的公式，如何得出新的被断定公式，被断定的公式又称为系统中的定理。公式，被断定的公式又称为系统中的定理。下一页在以上在以上4个组成部分中，前两个部分定个组成部分中，前两个部分定义了一个形式语言，后两个部分在该形义了一个形式语言，后两个部分在该形式语言上定义了一个演绎结构。式语言上定义了一个演绎结构。形式化系统由形式语言和定义于其上的形式化系统由形式语言和定义于其上的演绎结构组成。演绎结构组成。返 回形式化系统形式化系统从某种意义上讲，任何计算机系统软硬从某种意义上讲，任何计算机系统软硬件都是一种形式化系统，它们的结构可件都是一种形式化系统，它们的结

18、构可以用形式化方法描述。以用形式化方法描述。程序设计语言也是一种形式语言系统。程序设计语言也是一种形式语言系统。返 回形式化系统形式化系统抽象性抽象性u抽象是人们认识客观世界的基本方法，抽象是人们认识客观世界的基本方法，虽然抽象性并不是形式化系统的专利，虽然抽象性并不是形式化系统的专利，但形式化系统具有更强的抽象性。但形式化系统具有更强的抽象性。返 回形式化系统的基本特点形式化系统的基本特点符号化符号化u形式化系统的抽象性表现在它自身仅仅形式化系统的抽象性表现在它自身仅仅是一个符号系统，除了表示符号间的关是一个符号系统，除了表示符号间的关系（字符号串的变换）外，不表示任何系（字符号串的变换）外

19、，不表示任何别的意义。别的意义。返 回形式化系统的基本特点形式化系统的基本特点形式化系统的基本特点形式化系统的基本特点严格性严格性u 形式化系统中，任何初始符号和推形式化系统中，任何初始符号和推导过程都要进行严格的定义。导过程都要进行严格的定义。机械化机械化u 形式化系统采用的是一种纯形式的形式化系统采用的是一种纯形式的机械方法，因此它的严格性高于一机械方法，因此它的严格性高于一般的数学推导。般的数学推导。下一页形式化方法的局限性形式化方法的局限性形式化方法并不是形式化方法并不是“完美无缺完美无缺”的的“灵灵丹妙药丹妙药”。可以证明，任何一个形式化系统，如果可以证明，任何一个形式化系统，如果它

20、是无矛盾的，那么，它就具有下面两它是无矛盾的，那么，它就具有下面两个局限性。个局限性。下一页形式化方法的局限性形式化方法的局限性不完备性不完备性u1931年，哥德尔提出的关于形式化系统的年，哥德尔提出的关于形式化系统的“不完备性定理不完备性定理”，指出：如果一个形式的，指出：如果一个形式的数学理论是足够复杂的（复杂到所有的递归数学理论是足够复杂的（复杂到所有的递归函数在其中都能够表示），而且它是无矛盾函数在其中都能够表示），而且它是无矛盾的，那么在这一理论中必存在一个语句，这的，那么在这一理论中必存在一个语句，这一语句在这一理论中既不能证明，也不能否一语句在这一理论中既不能证明，也不能否证。证

21、。下一页31哥德尔不完备定理 哥德尔不完备定理是库尔特哥德尔（Kurt Gdel 19061978）于1931年证明并发表的两条定理。 第一定理第一定理： 任何一个相容的数学形式化理论中，只要它强到足以蕴涵皮亚诺算术公理，就可以在其中构造在体系中既不能证明也不能否证的命题。 第二定理第二定理： 任何相容的形式体系不能用于证明它本身的相容性。32歌德尔不完全定理对认知科学哲学的影响 哥德尔不完备定理的结论影响了数学哲学的结论影响了数学哲学以及形式化主义（使用形式符号描述原理）以及形式化主义（使用形式符号描述原理）中的一些观点。中的一些观点。 我们可以将第一定理解释为：我们可以将第一定理解释为：“

22、我们永远我们永远不能发现一个万能的公理系统，能够证明不能发现一个万能的公理系统，能够证明一切数学真理，而不能证明任何谬误。一切数学真理，而不能证明任何谬误。” 我们可以将第一定理解释为：我们可以将第一定理解释为：“如果一个如果一个（强度足以证明基本算术公理的）公理系（强度足以证明基本算术公理的）公理系统可以用来证明它自身的相容性，那么它统可以用来证明它自身的相容性，那么它就是不相容的。就是不相容的。”不可判定性不可判定性u如果对一类语句如果对一类语句C而言，存在一个算法而言，存在一个算法AL，使得对，使得对C中中的任一语句的任一语句S而言，可以利用算法而言，可以利用算法AL来判定其是否成立，来

23、判定其是否成立，则则C称为可判定的，否则，称为不可判定的。称为可判定的，否则，称为不可判定的。u著名的著名的“停机问题停机问题”就是一个不可判定性的问题。该问就是一个不可判定性的问题。该问题是指一个任给的图灵机对于一个任给的输入而言是否题是指一个任给的图灵机对于一个任给的输入而言是否停机的问题，图灵证明了这类问题是不可判定的。停机的问题，图灵证明了这类问题是不可判定的。u计算机系统是一种形式化系统，因此，计算机系统一样计算机系统是一种形式化系统，因此，计算机系统一样也具有形式化系统的局限性。也具有形式化系统的局限性。返 回形式化方法的局限性形式化方法的局限性形式化与公理化形式化与公理化 形式化

24、不一定导致公理化，公理系统也不形式化不一定导致公理化，公理系统也不一定是形式系统。一定是形式系统。 如欧氏几何公理系统就不是形式系统。如欧氏几何公理系统就不是形式系统。 形式化与公理化虽然不同，但在近代数学形式化与公理化虽然不同，但在近代数学中，形式系统大都是形式化的公理系统。中，形式系统大都是形式化的公理系统。第章绪论第章绪论1.1 形式化方法概述1.2 软件开发中的形式化方法软件开发中的形式化方法计算机软件一般指计算机系统中的计算机软件一般指计算机系统中的程序程序及及文档文档程序程序: :以计算机语言表达的软件系统以计算机语言表达的软件系统文档文档: :以人类语言以人类语言( (自然的或形

25、式化的自然的或形式化的) )表达的软件表达的软件系统系统二者互相配合共同构成了完整的软件系统二者互相配合共同构成了完整的软件系统人类的经验、抽象知识正逐步由软件予以精确地体人类的经验、抽象知识正逐步由软件予以精确地体现现什么是软件？什么是软件？万物皆数万物皆数? 通过软件，人们可以对其所认识到的任何通过软件，人们可以对其所认识到的任何一种事物进行一种事物进行“编码编码”。 以产生它的一个数字化的虚拟以产生它的一个数字化的虚拟“实例实例”。 软件本质：逻辑产品软件本质：逻辑产品 理论基础：理论基础：Universal TM（图灵机）（图灵机）von Neumann architecturePL

26、virtual machines 软件软件 是人类脑力劳动的产物是人类脑力劳动的产物是系统是系统逻辑逻辑的体现的体现 但又必须依附于一定的载体但又必须依附于一定的载体例如：纸张、软盘、硬盘、光盘等例如：纸张、软盘、硬盘、光盘等 其它物品呢？需不需要载体？其它物品呢？需不需要载体？理解软件的关键是什么？理解软件的关键是什么？软件本质：逻辑产品软件本质：逻辑产品软件作为逻辑产品的特点：软件作为逻辑产品的特点：优势：优势：易于变化，适应性强易于变化，适应性强复制成本低，适合规模经济复制成本低，适合规模经济劣势：劣势：不易被理解不易被理解容易出错容易出错找错、排错困难找错、排错困难软件本质：逻辑产品软

27、件本质：逻辑产品41软件开发过程软件开发过程 软件开发软件开发把现实世界的需求模型化成软件并予以实现的过程把现实世界的需求模型化成软件并予以实现的过程 软件开发的主要步骤（大致，有不同说法）：软件开发的主要步骤（大致，有不同说法）：问题和需求分析问题和需求分析设计：设计：功能设计功能设计结构设计结构设计编码（构建）编码（构建）调试调试发布、维护和升级发布、维护和升级人们在实践中提出了许多开发模型：如传统的瀑布模型，较新人们在实践中提出了许多开发模型：如传统的瀑布模型，较新近的有快速原型、迭代式开发模型等等近的有快速原型、迭代式开发模型等等-42-软件开发的历史软件开发的历史 软件开发的三个阶段

28、程序设计阶段（1946年-1956年）科学计算、机器语言及汇编语言、个体编程编程技巧、程序效率没有文档、软件一词尚未出现程序系统阶段（1956年-1968年）1956年，J.Backus Fortran语言诞生大量数据处理、小组开发“软件”一词出现：程序及其说明60年代中期，软件危机。软件工程阶段（1968年以来）1968年NATO会议，提出“软件工程”术语工程化方法、描述语言、团队开发43软件开发：实际情况软件开发：实际情况 软件开发的实际情况并不乐观。软件开发的实际情况并不乐观。 项目经常延误，预算经常超支。项目经常延误，预算经常超支。 开发的后续阶段常发现许多前期设计错误，更正的开发的后

29、续阶段常发现许多前期设计错误，更正的代价高昂。代价高昂。 发布运行的软件中常常存在着许多错误，时常崩溃发布运行的软件中常常存在着许多错误，时常崩溃 软件维护和更新工作的代价很高。软件维护和更新工作的代价很高。44软件开发：实际情况软件开发：实际情况 Therac-25 放射线治疗仪1985-87 年过量辐射过量辐射 (6 个死亡个死亡 / 截肢截肢)！Mars Pathfinder（火星探路者） 1997 年 周期性重新启动 (在火星上)！汽车导航控制系统 1986 Grady Booch 点火后加速 (撞车)！45软件开发：实际情况软件开发：实际情况 航空器控制系统功能错误功能错误 (飞机撞

30、毁飞机撞毁)！核电站控制系统 堆芯熔化 (大灾难)！?!移动电话 2000 年以后 - 死机 (烦死人)！46软件的本质问题软件的本质问题 复杂性复杂性规模：成万、成百万、甚至成千万行代码规模：成万、成百万、甚至成千万行代码系统组成部分之间异常复杂的直接与间接相互作用系统组成部分之间异常复杂的直接与间接相互作用静态结构与动态性质之间难以把握的复杂关系静态结构与动态性质之间难以把握的复杂关系 不确定性不确定性/多变性多变性需求的不断提升和变化需求的不断提升和变化异常丰富多彩的应用需求异常丰富多彩的应用需求 困境困境要求较低的开发成本和较短的开发周期要求较低的开发成本和较短的开发周期难以长期集中一

31、大批最优秀的技术人员难以长期集中一大批最优秀的技术人员E01-EDIData Warehouse(Interfaces to and from theData Warehouse are notdisplayed on this diagram)G02 - GeneralLedgerA05 - APS01 - SalesCorrectionsI01 POReceivingI03 Return toVendorI06 WarehouseManagementMainframePC/NT apps UNIX apps3rd party interfaceS06 - Credit AppP15 EES

32、 EmployeeChange NoticeOTHER APPS - PCAP - Collections/CreditTM - Credit Card DBACCTS REC APPS - PC990CORBad DebtBeneficial FeesBeneficial ReconcileJEAXFJEBFAJEBKAJEDVAJESOAJEVSAJEVSFNSFTeleCredit FeesINVENTORY CONTROL APPS - PCCode AlarmDebit ReceivingsDevo SalesDisplay InventoryIn HomeJunkoutsMerch

33、andise WithdrawalPromo CreditsRTV AccrualShrinkAP Research - Inv CntrlAP Research-Addl RptsBook to Perpetual InventoryClose Out ReportingComputer Intelligence DataCount CorrectionsCross Ref for VCB DnldsDamage Write OffDebit ReceivingsDFI Vendor DatabaseDisplay Inventory ReconcileDisplay Inventory R

34、eportingINVENTORY CONTROL APPS - PCDPI/CPIIC BatchingInventory Adj/Count CorrectInventory Control ReportsInventory LevelsInventory RollMerchandise WithdrawalOpen ReceivingsPI Count ResultsPI Time Results from InvPrice ProtectionSales Flash ReportingShrink ReportingSKU Gross MarginSKU Shrink Level De

35、tailUSMVCB DownloadsJournal Entry Tool KitScorecard - HRL02-ResourceScheduling(Campbell)P09 - P17CyborgM02 - MillenniumM03 - Millennium 3.0Banks - ACH and Pos toPayCobraB01 - StockStatusS03-PollingP14 On-line NewHire EntryCTSPlan Administrators(401K, PCS, Life,Unicare, SolomonSmith Barney)D01 Post L

36、oadBillingI04 HomeDeliveriesI02 -TransfersArthur PlanningI07 PurchaseOrderI12 EntertainmentSoftwareI05Inventory InfoE13E3 InterfaceS04 - Sales PostingV01-Price ManagementSystemI10 Cycle PhysicalInventoryI55 SKUInformationK02Customer RepairTrackingI35 Early WarningSystemB02 MerchandiseAnalysisI13- Au

37、toReplenishmentU18 - CTOInterceptI09 Cycle CountsE02-EmployeePurchaseTexlon 3.5ACHStock OptionsI17 Customer PerceivedIn-StockU16-TexlonSiteSeerC02 - CapitalProjectsF06 - FixedAssetsUS Bank ReconFileStar RepairEDICoordinatorMesa DataNEW SoundscanNPD GroupAIG Warranty GuardResumixOptikaStore BudgetRep

38、ortingP16 - Tally SheetCash Receipts/CreditS05 - HouseChargesAd ExpenseL01-PromoAnalysisV02-PriceMarketingSupportBMP - Busperformance MngtStoreScorecardI11 PriceTestingValley MediaP09Bonus/HRI15 Hand ScanAppsRoadshowPOSS08 - VertexSalesTaxA04 - CustRefund ChksEquifaxICMS CreditCellularRolloverS09 -

39、DigitalSatelliteSystemNPD,SoundScanSterling VANMailbox (Value)I18SKU RepX92-X96Host to AS400CommunicationS02 -LayawaysWashington,RGIS,Ntl Bus SystemsV04-SignSystemI14 Count CorrectionsNARMP01-EmployeeMasterfileI06 - CustomerOrderFrickCoUAR - Universal AccountReconciliationDepositoryBanksS07 - CellPh

40、onesS11 - ISPTrackingAASFringe POCash Over/ShortL60 MDFCoopSKU SelectionToolSKUPerformanceSupplierCompliance1I35 - CEIASISMisc Accounting/Finance Apps - PC/NTCOBA (Corp office Budget Assistant)PCBS(Profit Center Budget System)Merchandising BudgetAIMSMerch Mngr ApprovalBatch ForcastingAd MeasurementA

41、IMS AdminAIMSReportingAdLauncherV03- MktReactionsSpecSourceCTO2.BRebateTransferSignSystemCopyWritersWorkspaceELTPowerSuiteStoreMonitorAIS CalendarStores & MrktsDue DatesSmart PlusInsertionsOrdersBudgetAnalysis ToolPrint CostingInvoice AppAIS ReportsBroadcastFilterSmart PlusLauncherGeneralMaintenance

42、Printer POPrinterMaintenanceVendorMaintenanceVendor SetupConnect 3Connect 3ReportsConnect 3PDF TransfeSpec SourceSKU TrackingS20-SalesPollingProdigyPSPIn-HomeRepairWarrantyBillingSystemProcess Servers(Imaging)Prepared by Michelle MillsAn example of a real architecture in an industry软件的复杂性软件的复杂性软件的不确

43、定性软件的不确定性 Heisenberg不确定性：由于软件的开发和使用不确定性：由于软件的开发和使用，造成了由软件、使用者及其环境所构成的系统发生造成了由软件、使用者及其环境所构成的系统发生了变化，这样的变化是难以预测的，由此产生的不了变化，这样的变化是难以预测的，由此产生的不确定性确定性 Gdel不确定性：对一个软件，由于不确定性：对一个软件，由于使用者及其环使用者及其环境所构成的系统的描述的境所构成的系统的描述的不完备不完备所造成的不确定所造成的不确定性性应对方法应对方法管理管理 工作规范 管理和组织 过程控制 培训 人际交流 规律及本规律及本质质 抽象和封装 良好的描述形式 软件开发模型

44、 过程模型 手段和过手段和过程程 编程语言 中间件 开发工具 软件：设计和制造软件：设计和制造传统的认识是软件没有制造过程，只有设计过程传统的认识是软件没有制造过程，只有设计过程按照传统说法，软件的实现阶段也被称作按照传统说法，软件的实现阶段也被称作“程序程序设计设计”在传统的软件开发过程中，前期各个阶段的工作在传统的软件开发过程中，前期各个阶段的工作成果都是自然语言描述的成果都是自然语言描述的“非形式化非形式化”的文档，的文档，只有最后开发阶段的成果才是只有最后开发阶段的成果才是“形式化形式化”的程序的程序代码代码非形式的前期工作成果（文档）只能由人以非形非形式的前期工作成果（文档）只能由人

45、以非形式的方式阅读、理解和讨论，无法进行严格的分式的方式阅读、理解和讨论，无法进行严格的分析的推理析的推理软件：设计和制造软件：设计和制造从原则上说，程序代码都是从原则上说，程序代码都是“形式化形式化”的，有的，有“严格严格”定义的语法和语义。定义的语法和语义。程序的所有静态和动态性质都蕴藏在程序正文中，程序的所有静态和动态性质都蕴藏在程序正文中，其特点是：其特点是：程序除包含了软件的功能逻辑外，还包含了许多程序除包含了软件的功能逻辑外，还包含了许多有关具体语言、实现模型的细节，使对程序逻辑有关具体语言、实现模型的细节，使对程序逻辑详细分析变得非常困难。详细分析变得非常困难。各种实现细节大大增

46、加了程序的复杂度，从而大各种实现细节大大增加了程序的复杂度，从而大大提高了分析和推理的成本（通常不是规模的线大提高了分析和推理的成本（通常不是规模的线性函数，而是指数的）。性函数，而是指数的）。软件：设计和制造软件：设计和制造由非形式化的软件前期成果由非形式化的软件前期成果(文档文档)到后期的复杂到后期的复杂烦琐的程序代码，这一跨越的距离太大，相互之烦琐的程序代码，这一跨越的距离太大，相互之间的关系难以把握，无法验证对错。间的关系难以把握，无法验证对错。由于，软件的严格的形式化描述出现在后期，形由于，软件的严格的形式化描述出现在后期，形式太复杂，与前期成果的距离太远，导致对程序式太复杂，与前期

47、成果的距离太远，导致对程序代码的分析和推理障碍重重，并且不完整。代码的分析和推理障碍重重，并且不完整。测试不可能完全，发现问题的能力很有限，不能测试不可能完全，发现问题的能力很有限，不能成为评判标准。成为评判标准。53软件：设计和制造软件：设计和制造 可以把软件的前期工作看成设计，把最后的编程看作可以把软件的前期工作看成设计，把最后的编程看作制造制造 为了提高软件质量，必须加强软件的设计过程，需要：为了提高软件质量，必须加强软件的设计过程，需要：更可控的设计和制造过程更可控的设计和制造过程为设计本身提供更好的基础支持（理论和技术、工具）为设计本身提供更好的基础支持（理论和技术、工具）在设计过程

48、的早期，能够严格地分析前期制品的内在性质，尽早发现在设计过程的早期，能够严格地分析前期制品的内在性质，尽早发现并更正设计中隐藏的错误和缺陷并更正设计中隐藏的错误和缺陷清晰而无歧义的制品描述形式，在不同方面和不同细节程度的设计之清晰而无歧义的制品描述形式，在不同方面和不同细节程度的设计之间建立严格定义的、可以严格检查的关系间建立严格定义的、可以严格检查的关系从设计到制造的严格而清晰的转换，定义清楚什么是从设计到制造的严格而清晰的转换，定义清楚什么是正确的实现正确的实现，并，并能正确实施实际的制造活动能正确实施实际的制造活动 在软件设计阶段引进严格的形式化描述，就可以对早期成果在软件设计阶段引进严

49、格的形式化描述，就可以对早期成果进行分析和推理，为实现（制造）打下更好的基础。进行分析和推理，为实现（制造）打下更好的基础。形式化方法的引入形式化方法的引入从以上分析不难看出，在软件设计实现的各阶段从以上分析不难看出，在软件设计实现的各阶段(特别是早期特别是早期)引进严格的形式化描述，对软件开引进严格的形式化描述，对软件开发的早期成果进行分析和推理，将可以为后续开发的早期成果进行分析和推理，将可以为后续开发打下更好的基础。发打下更好的基础。在设计过程中采用严格的数学或逻辑方法分析前在设计过程中采用严格的数学或逻辑方法分析前期制品的内在性质，将可以尽早发现并更正设计期制品的内在性质，将可以尽早发

50、现并更正设计中隐藏的错误和缺陷。中隐藏的错误和缺陷。采用清晰而无歧义的描述形式，在设计和实现之采用清晰而无歧义的描述形式，在设计和实现之间建立严格定义的关系（即什么是正确的实现），间建立严格定义的关系（即什么是正确的实现），以便实现软件开发过程的自动化。以便实现软件开发过程的自动化。朴素软件设计朴素软件设计 基于自然语言的思考、设计和描述 语义含糊，可能有歧义，依赖于使用者的理解半形式化方法半形式化方法 通过相对规范的形式和语义进行定义和描述 语义较清晰，可以用工具进行部分检查和分析形式化方法形式化方法 基于严格定义的数学概念和语言 语义清晰，无歧义。 可以采用自动化工具进行检查和分析朴素方法