軟件開(kāi)發(fā)的形式化工程方法

前言

本書(shū)以簡(jiǎn)潔明了的語(yǔ)言介紹了軟件開(kāi)發(fā)技術(shù)的最新成果——形式化工程方法，并在精確而簡(jiǎn)單的概念描述和必要的數(shù)學(xué)定義基礎(chǔ)之上，以大量淺顯易懂的案例系統(tǒng)地闡述了一個(gè)具體的系統(tǒng)建模和功能描述語(yǔ)言SOFL(Structured Object-Oriented Formal Language)以及在此語(yǔ)言基礎(chǔ)之上建立起來(lái)的并具有代表性的形式化工程方法，稱(chēng)為SOFL方法。。大家都知道，大型軟件產(chǎn)品的開(kāi)發(fā)是一個(gè)一般需要多數(shù)開(kāi)發(fā)人員參加的復(fù)雜過(guò)程。它的主要環(huán)節(jié)有三個(gè)：理解、創(chuàng)造和確認(rèn)。為了給用戶(hù)提供滿(mǎn)意而正確的軟件產(chǎn)品，開(kāi)發(fā)者首先必須正確和全面地理解用戶(hù)的要求，包括功能要求。必要的數(shù)據(jù)資源。對(duì)功能與數(shù)據(jù)資源或系統(tǒng)行為的限制。在此基礎(chǔ)之上，開(kāi)發(fā)者必須通過(guò)系統(tǒng)的設(shè)計(jì)，構(gòu)建軟件系統(tǒng)的體系結(jié)構(gòu)。數(shù)據(jù)結(jié)構(gòu)和有效的算法，并以一定的編程語(yǔ)言實(shí)現(xiàn)其代碼。這一系列的創(chuàng)造過(guò)程是不可能完全自動(dòng)實(shí)現(xiàn)的，它必須依靠軟件開(kāi)發(fā)者來(lái)完成。然而，開(kāi)發(fā)者是不能保證不出錯(cuò)的。實(shí)際上，大型軟件系統(tǒng)的開(kāi)發(fā)過(guò)程中一般都要出現(xiàn)大量的人為錯(cuò)誤，經(jīng)常造成軟件產(chǎn)品的生產(chǎn)費(fèi)用增大，不能按時(shí)交貨，或不能保證質(zhì)量。為此，完成的軟件產(chǎn)品的質(zhì)量必須得到嚴(yán)密的確認(rèn)以后其產(chǎn)品才能送交用戶(hù)使用。保證軟件質(zhì)量的一個(gè)很重要的要素就是軟件開(kāi)發(fā)方法。開(kāi)發(fā)方法是不是實(shí)用有效，一般取決于它是否具備三個(gè)要素：簡(jiǎn)單。可視化和精確。也就是說(shuō)，該方法必須用起來(lái)簡(jiǎn)單，其表現(xiàn)形式要有效地發(fā)揮圖形語(yǔ)言的可視化效果，同時(shí)所表達(dá)的內(nèi)容必須精確以確保其意思能被準(zhǔn)確理解。傳統(tǒng)的軟件開(kāi)發(fā)方法，像結(jié)構(gòu)化和面向?qū)ο蟮拈_(kāi)發(fā)方法，基本上都用自然語(yǔ)言或語(yǔ)義不明的圖形語(yǔ)言來(lái)描述用戶(hù)的需求和系統(tǒng)設(shè)計(jì)文檔。由于自然語(yǔ)言表達(dá)結(jié)構(gòu)和所用術(shù)語(yǔ)的意思不清楚所造成的二義性，使得軟件文檔經(jīng)常被誤解或被隨意解釋以造成大量嚴(yán)重的設(shè)計(jì)或?qū)崿F(xiàn)上的錯(cuò)誤。這種局面也嚴(yán)重地影響了切實(shí)有效的支撐工具的開(kāi)發(fā)和建立。.。 上世紀(jì)七十年代以來(lái)，以Hoare邏輯和Dijkstra的最弱前置謂詞演算為基礎(chǔ)發(fā)展而來(lái)的形式化開(kāi)發(fā)方法為嚴(yán)密地開(kāi)發(fā)軟件系統(tǒng)提供了理論基礎(chǔ)和技術(shù)，為解決上述問(wèn)題邁出了重要的一步。這些技術(shù)包括形式化規(guī)范說(shuō)明書(shū)寫(xiě)作語(yǔ)言，逐步求精的開(kāi)發(fā)方法，以及程序正確性證明技術(shù)。但遺憾的是，這些形式化技術(shù)只重視規(guī)范說(shuō)明書(shū)的精確性和軟件開(kāi)發(fā)的嚴(yán)密性，而未能在簡(jiǎn)單可行和有效的可視化方面取得可喜的進(jìn)展。恰恰相反，大型軟件系統(tǒng)的形式化規(guī)范說(shuō)明書(shū)往往復(fù)雜難懂，修改花費(fèi)時(shí)間，出錯(cuò)的可能性很大。加之，逐步求精的開(kāi)發(fā)方法和正確性證明技術(shù)都對(duì)開(kāi)發(fā)人員的抽象和邏輯演算能力要求很高，使得這種技術(shù)很難被一般企業(yè)的軟件開(kāi)發(fā)者所接受。如何才能使嚴(yán)密性很高的形式化開(kāi)發(fā)方法融合到傳統(tǒng)的軟件工程過(guò)程和技術(shù)中以提高和促進(jìn)它們的嚴(yán)密性。有效性以及可控制性從而最終達(dá)到提高軟件生產(chǎn)效率和軟件質(zhì)量的目的就成為一個(gè)意義重大的研究課題。形式化工程方法和SOFL方法就是在這種情況下從上世紀(jì)八十年代末逐漸形成并發(fā)展而來(lái)的。其目的就是建立起能把形式化開(kāi)發(fā)方法有效地結(jié)合到傳統(tǒng)的軟件開(kāi)發(fā)過(guò)程和方法中的技術(shù)，使得形式化方法能夠更加簡(jiǎn)單地被一般軟件開(kāi)發(fā)者使用，發(fā)揮其高嚴(yán)密性的特長(zhǎng)以促進(jìn)傳統(tǒng)軟件開(kāi)發(fā)技術(shù)的有效性和系統(tǒng)性，并使軟件開(kāi)發(fā)過(guò)程能得到更加有效的工具支撐。為建立有效的系統(tǒng)模型和確切的需求規(guī)范說(shuō)明書(shū)，SOFL方法提供了具有簡(jiǎn)單?？梢暬途_特點(diǎn)的形式化規(guī)范說(shuō)明書(shū)語(yǔ)言和行之有效的建立形式化規(guī)范說(shuō)明書(shū)的三步法。為有效地查出需求規(guī)范說(shuō)明書(shū)中的錯(cuò)誤，SOFL提供了嚴(yán)密的復(fù)審(review)和說(shuō)明書(shū)測(cè)試技術(shù)。為有效地利用結(jié)構(gòu)化和面向?qū)ο笤O(shè)計(jì)方法的各自?xún)?yōu)勢(shì)，SOFL提供了把結(jié)構(gòu)化和面向?qū)ο蟮脑O(shè)計(jì)方法有機(jī)結(jié)合的技術(shù)，使得結(jié)構(gòu)化方法在需求分析和抽象設(shè)計(jì)方面發(fā)揮其優(yōu)點(diǎn)以方便開(kāi)發(fā)者和用戶(hù)之間的交流和合作，而使面向?qū)ο蠓椒ㄔ谠敿?xì)設(shè)計(jì)和編碼方面發(fā)揮其特長(zhǎng)以增強(qiáng)所開(kāi)發(fā)系統(tǒng)的可維護(hù)性和重用性。它也提供了把結(jié)構(gòu)化設(shè)計(jì)轉(zhuǎn)化成面向?qū)ο蟮某绦虼a的方法和技術(shù)。為有效地發(fā)現(xiàn)程序中的錯(cuò)誤，SOFL提供了基于形式化規(guī)范說(shuō)明書(shū)的嚴(yán)密檢查(inspection)和嚴(yán)密測(cè)試技術(shù)。雖然這最后兩種查錯(cuò)技術(shù)沒(méi)有包括在本書(shū)之內(nèi)，但它們已形成SOFL方法的不可分割的部分?？偠灾琒OFL是集結(jié)構(gòu)化。面向?qū)ο蠛托问交椒ㄓ谝簧?，并具有?jiǎn)單?？梢暬途_的特點(diǎn)的形式化工程方法。它已被工業(yè)界和多數(shù)軟件工程人員所使用，其效果正在引起更多軟件工程師和研究者的興趣和關(guān)注。本書(shū)的內(nèi)容反映了作者在為提高軟件開(kāi)發(fā)質(zhì)量以及開(kāi)創(chuàng)嚴(yán)密有效和實(shí)用可行的形式化工程方法這個(gè)新技術(shù)領(lǐng)域近20年來(lái)的研究成果，并為進(jìn)一步徹底的解決軟件危機(jī)這個(gè)一直在困擾軟件工程的重大難題，提出和闡述了“智能軟件工程環(huán)境”這個(gè)未來(lái)軟件工程的發(fā)展方向。作為本書(shū)的作者，在2008年第29屆奧運(yùn)會(huì)在北京召開(kāi)之際，能將此書(shū)與國(guó)內(nèi)讀者見(jiàn)面，我感到由衷的欣慰，也很感謝清華大學(xué)出版社的極大熱情和努力，幫助我實(shí)現(xiàn)了多年來(lái)想把形式化工程方法SOFL介紹給國(guó)內(nèi)軟件工程界的大學(xué)生。研究生。研究者以及工程技術(shù)人員的夙愿。我衷心希望讀者能通過(guò)學(xué)習(xí)本書(shū)的內(nèi)容享受到形式化工程方法的新思想，掌握其應(yīng)用的系統(tǒng)技術(shù)，并提高開(kāi)發(fā)高質(zhì)量軟件產(chǎn)品的技巧和能力，為自己的學(xué)習(xí)。就業(yè)。研究以及工作創(chuàng)造新的生機(jī)。

內(nèi)容概要

本書(shū)首次開(kāi)創(chuàng)了一個(gè)新技術(shù)，即形式化工程方法，把傳統(tǒng)的形式化方法和軟件工程有機(jī)結(jié)合起來(lái)。它提供了一個(gè)嚴(yán)密、系統(tǒng)、有效的軟件開(kāi)發(fā)方法，其實(shí)用性超過(guò)了目前所有形式化方法。這正好可以滿(mǎn)足學(xué)術(shù)界、軟件工程類(lèi)學(xué)生對(duì)學(xué)習(xí)形式化工程方法和SOFL的迫切需求。　　本書(shū)通俗易懂，實(shí)例豐富，可滿(mǎn)足讀者即學(xué)即用的需要。書(shū)中對(duì)軟件開(kāi)發(fā)中的形式化工程方法進(jìn)行了介紹和討論，內(nèi)容涵蓋SE 2004中關(guān)于“軟件的形式化方法”的知識(shí)點(diǎn)，主要包括：有限狀態(tài)機(jī)、Statechart、Petri網(wǎng)、通信順序進(jìn)程、通信系統(tǒng)演算、一階邏輯、程序正確性證明、時(shí)態(tài)邏輯、模型檢驗(yàn)、2、VDM和Larch等。本書(shū)可作為計(jì)算機(jī)、軟件工程等專(zhuān)業(yè)高年級(jí)本科生或研究生的教學(xué)用書(shū)，也可供相關(guān)領(lǐng)域的研究人員和工程技術(shù)人員參考。

作者簡(jiǎn)介

Shaoying Liu 教授，著名計(jì)算機(jī)專(zhuān)家，日本法政大學(xué)教授，上海交通大學(xué)和上海大學(xué)客座教授。早年在西安交通大學(xué)獲得學(xué)士和碩士學(xué)位，后在英國(guó)曼徹斯特大學(xué)獲得博士學(xué)位?，F(xiàn)為IEEE計(jì)算機(jī)學(xué)會(huì)復(fù)雜性技術(shù)委員會(huì)副主席，IEEE計(jì)算機(jī)學(xué)會(huì)、ACM、日本軟件科學(xué)與技術(shù)學(xué)會(huì)成員。多年來(lái)

書(shū)籍目錄

1 Introduction　1.1  Software Life Cycle　1.2  The Problem　1.3  Formal Methods　　1.3.1  What Are Formal Methods　  1.3.2  Some Commonly Used Formal Methods　  1.3.3  Challenges to Formal Methods　1.4  Formal Engineering Methods　1.5  What Is SOFL　1.6  A Little History of SOFL　1.7  Comparison with Related Work　1.8  Exercises2 Propositional Logic　2.1  Propositions　2.2  Operators　2.3  Conjunction　2.4  Disjunction　2.5  Negation　2.6  Implication　2.7  Equivalence　2.8  Tautology, Contradiction, and Contingency　2.9  Normal Forms　2.10 Sequent　2.11 Proof　　2.11.1 Inference Rules　　2.11.2 Rules for Conjunction　  2.11.3 Rules for Disjunction　  2.11.4 Rules for Negation　  2.11.5 Rules for Implication　  2.11.6 Rules for Equivalence　  2.11.7 Properties of Propositional Expressions　2.12 Exercises3 Predicate Logic　3.1  Predicates　3.2  Quantifiers　　3.2.1  The Universal Quantifier　　3.2.2  The Existential Quantifier　  3.2.3  Quantified Expressions with Multiple Bound Variables　  3.2.4  Multiple Quantifiers　  3.2.5  de Morgan's Laws　3.3  Substitution　3.4  Proof in Predicate Logic　  3.4.1  Introduction and Elimination of Existential Quantifiers　  3.4.2  Introduction and Elimination of Universal Quantifiers  3.5  Validity and Satisfaction  3.6  Treatment of Partial Predicates  3.7 Formal Specification with Predicates  3.8  Exercises4 The Module  4.1  Module for Abstraction  4.2  Condition Data Flow Diagrams  4.3  Processes  4.4  Data Flows  4.5  Data Stores  4.6  Convention for Names  4.7  Conditional Structures  4.8  Merging and Separating Structures  4.9  Diverging Structures  4.10 Renaming Structure  4.11 Connecting Structures  4.12 Important Issues on CDFDs　　4.12.1 Starting Processes　  4.12.2 Starting Nodes　  4.12.3 Terminating Processes　  4.12.4 Terminating Nodes　  4.12.5 Enabling and Executing a CDFD　  4.12.6 Restriction on Parallel Processes　  4.12.7 Disconnected CDFDs　  4.12.8 External Processes  4.13 Associating CDFD with a Module  4.14 How to Write Comments  4.15 A Module for the ATM　4.16 Compound Expressions　  4.16.1 The if-then-else Expression　  4.16.2 The let Expression　  4.16.3 The case Expression　  4.16.4 Reference to Pre and Postconditions　4.17 Function Definitions　  4.17.1 Explicit and Implicit Specifications　  4.17.2 Recursive Functions　4.18 Exercises5 Hierarchical CDFDs and Modules　5.1  Process Decomposition　5.2  Handling Stores in Decomposition　5.3  Input and Output Data Flows　5.4  The Correctness of Decomposition　5.5  Scope　5.6  Exercises6 Explicit Specifications　6.1  The Structure of an Explicit Specification　6.2  Assignment Statement　6.3  Sequential Statements  6.4  Conditional Statements  6.5  Multiple Choice Statements  6.6  The Block Statement  6.7  The While Statement  6.8  Method Invocation  6.9  Input and Output Statements  6.10 Example  6.11 Exercises7  Basic Data Types  7.1  The Numeric Types  7.2  The Character Type  7.3  The Enumeration Types  7.4  The Boolean Type  7.5  An Example  7.6  Exercises8  The Set Types  8.1  What Is a Set　8.2  Set Type Declaration　8.3 Constructors and Operators on Sets　  8.3.1  Constructors　  8.3.2  Operators　8.4  Specification with Set Types　8.5  Exercises9 The Sequence and String Types　9.1  What Is a Sequence　9.2  Sequence Type Declarations　9.3  Constructors and Operators on Sequences　 9.3.1  Constructors　 9.3.2  Operators　9.4  Specifications Using Sequences　 9.4.1  Input and Output Module　 9.4.2  Membership Management System  9.5  Exercises10 The Composite and Product Types　10.1 Composite Types　　10.1.1 Constructing a Composite Type　　10.1.2 Fields Inheritance　　10.1.3 Constructor　　10.1.4 Operators　　10.1.5 Comparison　10.2 Product Types　10.3 An Example of Specification  10.4 Exercises11 The Map Types　11.1 What Is a Map　11.2 The Type Constructor　11.3 Operators　　11.3.1 Constructors　　11.3.2 Operators  11.4 Specification Using a Map  11.5 Exercises12 The Union Types　12.1 Union Type Declaration　12.2 A Special Union Type　12.3 Is Function　12.4 A Specification with a Union Type　12.5 Exercises13 Classes　13.1 Classes and Objects　　13.1.1 Class Definition　　13.1.2 Objects　　13.1.3 Identity of Objects　13.2 Reference and Access Control　13.3 The Reference of a Current Object　13.4 Inheritance　　13.4.1 What Is Inheritance　　13.4.2 Superclasses and Subclasses　　13.4.3 Constructor　　13.4.4 Method Overloading　　13.4.5 Method Overriding　　13.4.6 Garbage Collection　13.5 Polymorphism　13.6 Generic Classes　13.7 An Example of Class Hierarchy　13.8 Example of Using Objects in Modules　13.9 Exercises14 The Software Development Process　14.1 Software Process Using SOFL　14.2 Requirements Analysis　  14.2.1 The Informal Specification　  14.2.2 The Semi-formal Specification　14.3 Abstract Design　14.4 Evolution　14.5 Detailed Design　  14.5.1 Transformation from Implicit to Explicit Specifications　  14.5.2 Transformation from Structured to Object-Oriented　Specifications　14.6 Program　14.7 Validation and Verification　14.8 Adapting the Process to Specific Applications　14.9 Exercises15 Approaches to Constructing Specifications　15.1 The Top-Down Approach　  15.1.1 The CDFD-Module-First Strategy　  15.1.2 The CDFD-Hierarchy-First Strategy　  15.1.3 The Modules and Classes　15.2 The Middle-out Approach　15.3 Comparison of the Approaches　15.4 Exercises16 A Case Study - Modeling an ATM　16.1 Informal User Requirements Specification　16.2 Semi-formal Functional Specification　16.3 Formal Abstract Design Specification　16.4 Formal Detailed Design Specification　16.5 Summary　16.6 Exercises17 Rigorous Review　17.1 The Principle of Rigorous Review　17.2 Properties　　17.2.1 Internal Consistency of a Process　  17.2.2 Invariant-Conformance Consistency　  17.2.3 Satisfiability　  17.2.4 Internal Consistency of CDFD  17.3 Review Task Tree　  17.3.1 Review Task Tree Notation　  17.3.2 Minimal Cut Sets　  17.3.3 Review Evaluation  17.4 Property Review　  17.4.1 Review of Consistency Between Process and Invariant　  17.4.2 Process Consistency Review　  17.4.3 Review of Process Satisfiability　  17.4.4 Review of Internal Consistency of CDFD  17.5 Constructive and Critical Review  17.6 Important Points  17.7 Exercises18 Specification Testing  18.1 The Process of Testing  18.2 Unit Testing　  18.2.1 Process Testing　  18.2.2 Invariant Testing  18.3 Criteria for Test Case Generation  18.4 Integration Testing　  18.4.1 Testing Sequential Constructs　  18.4.2 Testing Conditional Constructs　  18.4.3 Testing Decompositions  18.5 Exercises 19 Transformation from Designs to Programs  19.1 Transformation of Data Types  19.2 Transformation of Modules and Classes  19.3 Transformation of Processes　  19.3.1 Transformation of Single-Port Processes　  19.3.2 Transformation of Multiple-Port Processes　19.4 Transformation of CDFD　19.5 Exercises20 Intelligent Software Engineering Environment　20.1 Software Engineering Environment　20.2 Intelligent Software Engineering Environment　20.3 Ways to Build an ISEE　  20.3.1 Domain-Driven Approach　  20.3.2 Method-Driven Approach　  20.3.3 Combination of Both　20.4 ISEE and Formalization　20.5 ISEE for SOFL    20.5.1 Support for Requirements Analysis　  20.5.2 Support for Abstract Design　  20.5.3 Support for Refinement　  20.5.4 Support for Verification and Validation　  20.5.5 Support for Transformation　  20.5.6 Support for Program Testing　  20.5.7 Support for System Modification　  20.5.8 Support for Process Management　20.6 Exercises References　　A  Syntax of SOFL　　A.1 Specifications　　A.2 Modules　  A.3 Processes　　A.4 Functions　  A.5 Classes　  A.6 Types　  A.7 Expressions　  A.8 Ordinary Expressions　　  A.8.1 Compound Expressions　 　 A.8.2 Unary Expressions　 　 A.8.3 Binary Expressions　 　 A.8.4 Apply Expressions　 　 A.8.5 Basic Expressions　 　 A.8.6 Constants　 　 A.8.7 Simple Variables　 　 A.8.8 Special Keywords　　  A.8.9 Set Expressions　 　 A.8.10 Sequence Expressions　 　 A.8.11 Map Expressions　 　 A.8.12 Composite Expressions　 　 A.8.13 Product Expressions    A.9 Predicate Expressions　　  A.9.1 Boolean Variables　　  A.9.2 Relational Expressions　　  A.9.3 Conjunction　　  A.9.4 Disjunction　　  A.9.5 Implication　　  A.9.6 Equivalence　　  A.9.7 Negation　　  A.9.8 Quantified Expressions　　A.10 Identifiers　　　A. 11 Character　　　A. 12 CommentsIndex

章節(jié)摘錄

插圖：

媒體關(guān)注與評(píng)論

Such books are to be whole-heartedly welcomed because they are written with an acute understanding of the issues for designers of useful software. 　　--Cliff B. JonesUniversity of Newcastle upon TyneProbably the best coverage of any formal treatment I have seen. 　　--Peter Lindsay　　University of Queensland

編輯推薦

《國(guó)外經(jīng)典教材?計(jì)算機(jī)科學(xué)與技術(shù)?軟件開(kāi)發(fā)的形式化工程方法:結(jié)構(gòu)化+面向?qū)ο?形式化》可作為計(jì)算機(jī)、軟件工程等專(zhuān)業(yè)高年級(jí)本科生或研究生的教學(xué)用書(shū)，也可供相關(guān)領(lǐng)域的研究人員和工程技術(shù)人員參考。

圖書(shū)封面

圖書(shū)標(biāo)簽Tags

無(wú)

評(píng)論、評(píng)分、閱讀與下載

---

    軟件開(kāi)發(fā)的形式化工程方法 PDF格式下載

---