形式化说明技术

形式化说明技术是软件工程常用的说明方法
形式化说明技术是软件工程中常用的说明方法，它基于数理逻辑、集合论和形式语言等数学基础，通过形式化的符号和规则描述软件系统的行为和性质，从而对软件进行精确、严谨和可检验的描述。

形式化说明技术包括以下几个方面：
1.数学符号：形式化说明技术使用代数符号、逻辑符号和其他数学符号对软件进行建模和描述。

这些符号具有严格的定义和规则，可以消除不同认知和语言带来的歧义和难以理解的问题。

2.形式规范：形式化说明技术还提供了一系列形式规范用于描述软件系统的行为和性质，如状态机、Petri网、Z规范等。

这些规范提供了一种形式化的表达方式，可以清晰地描述系统的结构和行为。

3.模型检验：形式化说明技术可以使用模型检验工具来对建模和规范进行验证。

这些工具可以从数学上证明软件是否满足其规范，从而帮助开发者发现软件中潜在的错误和缺陷，并提供相应的改进方案。

4.可重复性：形式化说明技术提供了一种可重复的方法，可以对软件进行精确且可检验的描述。

这些描述可以被其他人复用和修改，使软件的开发和维护变得更加高效和便捷。

总之，形式化说明技术是一种高度精细、严密和可靠的软件描述方法，广泛应用于软件工程领域，有助于提高软件质量和可靠性。

第一章一、什么是软件危机？它有哪些典型表现？为什么会出现软件危机？软件危机是指在计算机软件开发、使用与维护过程中遇到的一系列严重问题和难题。

它包括两方面：如何开发软件，已满足对软件日益增长的需求；如何维护数量不断增长的已有软件。

软件危机的典型表现：(1) 对软件开发成本和进度的估计常常很不准确。

常常出现实际成本比估算成本高出一个数量级、实际进度比计划进度拖延几个月甚至几年的现象。

而为了赶进度和节约成本所采取的一些权宜之计又往往损害了软件产品的质量。

这些都降低了开发商的信誉，引起用户不满。

(2) 用户对已完成的软件不满意的现象时有发生。

(3) 软件产品的质量往往是靠不住的。

(4) 软件常常是不可维护的。

(5) 软件通常没有适当的文档资料。

文档资料不全或不合格，必将给软件开发和维护工作带来许多难以想象的困难和难以解决的问题。

(6) 软件成本、软件维护费在计算机系统总成本中所占比例逐年上升。

(7) 开发生产率提高的速度远跟不上计算机应用普及的需求。

软件危机出现的原因：(1) 来自软件自身的特点：是逻辑部件，缺乏可见性；规模庞大、复杂，修改、维护困难。

(2) 软件开发与维护的方法不当：忽视需求分析；认为软件开发等于程序编写；轻视软件维护。

(3) 供求矛盾将是一个永恒的主题：面对日益增长的软件需求，人们显得力不从心。

二、假设自己是一家软件公司的总工程师，当把图1.1给手下的软件工程师们观看，告诉他们及时发现并改正错误的重要性时，有人不同意这个观点，认为要求在错误进入软件之前就清楚它们是不现实的，并举例说：“如果一个故障是编码错误造成的，那么，一个人怎么能在设计阶段清除它呢？”应该怎么反驳他？答：在软件开发的不同阶段进行修改付出的代价是很不相同的，在早期引入变动，涉及的面较少，因而代价也比较低；在开发的中期，软件配置的许多成分已经完成，引入一个变动要对所有已完成的配置成分都做相应的修改，不仅工作量大，而且逻辑上也更复杂，因此付出的代价剧增；在软件“已经完成”是在引入变动，当然付出的代价更高。

用z语言描述的最简单的形式化规格说明最简单的形式化规格说明是通过使用Z语言来定义和描述系统的行为和特性。

Z语言是一种形式化规范语言，它用于描述软件系统、硬件系统或任何其他系统的规范。

Z语言使用数学符号和形式化的术语，以一种精确而准确的方式来定义系统的规范。

它可以描述系统的状态、操作、约束和性质，并提供一种清晰和可验证的方法来确定系统是否满足规范。

例如，假设我们要描述一个简单的计算器系统。

我们可以使用Z语言来说明该系统的规范。

以下是一个简单的示例：基本规范：- 系统具有一个输入口和一个输出口。

- 输入口接收用户输入的数字和操作符。

- 输出口显示计算结果。

状态规范：- 系统具有一个变量x，表示当前的结果。

- 系统具有一个变量input，表示用户的输入。

操作规范：- 用户输入的每个数字将更新变量x的值。

- 用户输入的操作符将触发相应的操作，如加法、减法、乘法或除法。

约束规范：- 变量x的值必须在合理的范围内，否则应显示错误。

- 用户输入的操作符必须是有效的操作符之一，否则应显示错误。

性质规范：- 当用户输入正确的数字和操作符时，系统应按预期进行计算，并正确显示结果。

- 当用户输入无效的数字或操作符时，系统应显示错误信息，以指示输入错误。

通过使用Z语言，我们能够明确地定义系统的规范，包括输入、状态、操作和性质。

这种形式化的规范能够帮助开发人员、测试人员和项目相关人员共享和理解系统的期望行为，从而提高系统的可靠性和正确性。

需要注意的是，以上只是一个简化的示例，实际的形式化规格说明可能会更加复杂和详细。

但使用Z语言作为规范语言可以帮助我们准确地描述系统的要求和行为，以便开发出高质量的软件系统。

第一章一、什么是软件危机？它有哪些典型表现？为什么会出现软件危机？软件危机是指在计算机软件开发、使用与维护过程中遇到的一系列严重问题和难题。

它包括两方面：如何开发软件，已满足对软件日益增长的需求；如何维护数量不断增长的已有软件。

软件危机的典型表现：(1) 对软件开发成本和进度的估计常常很不准确。

常常出现实际成本比估算成本高出一个数量级、实际进度比计划进度拖延几个月甚至几年的现象。

而为了赶进度和节约成本所采取的一些权宜之计又往往损害了软件产品的质量。

这些都降低了开发商的信誉，引起用户不满。

(2) 用户对已完成的软件不满意的现象时有发生。

(3) 软件产品的质量往往是靠不住的。

(4) 软件常常是不可维护的。

(5) 软件通常没有适当的文档资料。

文档资料不全或不合格，必将给软件开发和维护工作带来许多难以想象的困难和难以解决的问题。

(6) 软件成本、软件维护费在计算机系统总成本中所占比例逐年上升。

(7) 开发生产率提高的速度远跟不上计算机应用普及的需求。

软件危机出现的原因：(1) 来自软件自身的特点：是逻辑部件，缺乏可见性；规模庞大、复杂，修改、维护困难。

(2) 软件开发与维护的方法不当：忽视需求分析；认为软件开发等于程序编写；轻视软件维护。

(3) 供求矛盾将是一个永恒的主题：面对日益增长的软件需求，人们显得力不从心。

二、假设自己是一家软件公司的总工程师，当把图1.1给手下的软件工程师们观看，告诉他们及时发现并改正错误的重要性时，有人不同意这个观点，认为要求在错误进入软件之前就清楚它们是不现实的，并举例说：“如果一个故障是编码错误造成的，那么，一个人怎么能在设计阶段清除它呢？”应该怎么反驳他？答：在软件开发的不同阶段进行修改付出的代价是很不相同的，在早期引入变动，涉及的面较少，因而代价也比较低；在开发的中期，软件配置的许多成分已经完成，引入一个变动要对所有已完成的配置成分都做相应的修改，不仅工作量大，而且逻辑上也更复杂，因此付出的代价剧增；在软件“已经完成”是在引入变动，当然付出的代价更高。

软件工程形式化说明技术在当今数字化时代，软件工程的重要性日益凸显。

为了确保软件的质量、可靠性和可维护性，各种技术和方法不断涌现，其中形式化说明技术是一个关键的领域。

那么，什么是软件工程形式化说明技术呢？简单来说，它是一种用于精确描述软件系统的需求、设计和行为的技术手段。

与我们日常中较为随意和模糊的描述不同，形式化说明技术采用严格的数学和逻辑符号，以一种无歧义、精确且可验证的方式来表达软件的各种特性。

想象一下，我们要建造一座高楼大厦。

在开始施工之前，建筑师会绘制详细的蓝图，标注出每一个尺寸、每一种材料、每一个结构的细节。

软件工程中的形式化说明就类似于这样的蓝图，但它更加精确和严格。

形式化说明技术的一个重要优点是能够减少软件系统中的不确定性和模糊性。

在传统的软件开发过程中，需求和设计往往通过自然语言来描述，这可能导致不同的人对同一份文档有不同的理解。

而形式化说明则消除了这种模糊性，因为它的定义是精确且无二义的。

比如说，一个关于用户登录功能的需求描述，如果用自然语言可能会说：“用户输入用户名和密码，如果用户名和密码正确，就允许登录。

”但这可能会引起一些疑问，比如：用户名和密码的正确匹配规则是什么？是否区分大小写？是否有次数限制？而通过形式化说明，可以明确地定义这些细节，避免误解和错误。

形式化说明技术还可以帮助我们在软件开发的早期阶段发现错误。

由于其精确性，我们可以使用数学方法对形式化的描述进行推理和验证。

这就像是在数学考试中检查答案一样，如果我们的描述存在逻辑上的不一致或错误，通过这种验证就能够及早发现，从而避免在后期开发中付出高昂的代价来修复。

在实际应用中，有多种形式化说明技术可供选择。

例如，状态机模型可以用来描述系统在不同状态之间的转换和行为；时序逻辑可以用于表达时间相关的性质；还有形式化的语法和语义定义等。

以状态机模型为例，它将系统定义为一系列有限的状态，以及在不同条件下从一个状态转换到另一个状态的规则。

04章形式化说明技术形式化说明技术（Formal Specification Techniques）是一种系统性、精确地描述和定义软件系统执行行为、功能和性质的技术方法。

它通过使用数学语言和形式规约的方法，将软件系统的设计和实现过程从自然语言的模糊性和歧义性中解放出来，从而改善了软件开发和维护的效率和质量。

形式化说明技术的核心思想是将软件系统描述为一个数学模型，通过形式化的推理和证明，确保系统满足设计要求并具备所需的性质。

形式化说明技术不仅能够精确地描述系统的行为和功能，还可以检查系统的正确性、一致性、完备性、可靠性和安全性等方面的属性，提前发现和解决潜在的问题。

形式化说明技术的应用范围广泛，包括需求分析、系统设计、编码验证、软件测试、系统仿真和代码生成等方面。

下面将介绍几种常见的形式化说明技术。

1. 判定性有穷状态自动机（Deterministic Finite State Automaton，DFSA）：DFSA 是一种常用的形式化说明技术，用于描述系统的状态和状态转移。

它可以形式化地描述系统的行为，通过状态转移图来表示系统的状态变化，从而帮助开发人员更好地理解和设计系统。

2. 时序逻辑（Temporal Logic）：时序逻辑是一种扩展的命题逻辑，用于描述系统的时序性质。

通过形式化的规约、语义和推理，可以验证系统是否满足时序性质，如安全性、活性、不变性等。

时序逻辑广泛应用于软硬件系统的验证和验证。

3. Petri 网（Petri Nets）：Petri 网是一种用于建模和分析并发系统的图形化形式化说明技术。

Petri 网通过描述系统的状态、变迁和资源，揭示系统的并发行为和资源竞争情况，从而帮助开发人员理解和设计并发系统。

4. Z 规范（Z Specification）：Z 规范是一种基于集合论和一阶谓词逻辑的形式化说明技术，用于描述系统的状态、操作和约束等。

Z 规范通过形式化地定义系统的状态集合、操作集合和约束条件，帮助开发人员更好地理解和设计系统。

软件工程课后习题答案习题1 略。

习题2 略。

习题3 略。

习题42．在什么情况下应该使用形式化说明技术？使用形式化说明技术时应遵守哪些准则？人们在理解用自然语言描述的规格说明时，容易产生二义性。

为了克服非形式化方法的缺点，人们把数学引入软件开发工程，创造了基于数学的形式化说明技术。

应用形式化方法的准则：（1）应该选用释放的表示方法；（2）应该形式化，但不要过分形式化；（3）应该估算成本；（4）应该有形式化方法顾问随时提供咨询；（5）不应该放弃传统的开发方法；（6）应该建立详尽的文档；（7）不应该放弃质量标准；（8）不应该盲目依赖形式化方法；（9）应该测试、测试再测试；（10）应该重用。

4．用有穷状态机说明自动化图书馆流通系统习题5 略。

习题6 略。

习题7 略。

习题8 略。

习题91．什么是面向对象方法学？它有哪些优点？面向对象方法学，是尽可能模拟人类习惯的思维方式，使开发软件的方法和过程尽可能接近人类认识世界解决问题的方法和过程，从而使得实现解法的解空间（也称为求解域）与描述问题的问题空间（也称为问题域）在结构上尽可能一致。

优点：1.与人类习惯的思维方法一致；2.稳定性好；3.可重用性好；4.较易开发大型软件产品；5.可维护性好10．建立订货系统的用例模型。

分析如下：从对这个订货系统的需求可以知道，仓库管理员通过放在仓库中的终端把零件入库/出库市事务报告给订货系统，系统接受到事务信息之后应该处理事务；采购员需要使用订货系统提供的产生报表功能，以获取订货报表。

综上所述，用例如下：习题101．用面向对象方法分析研究本书习题2第2题中描述的储蓄系统，试建立它的对象模型、动态模型和功能模型。

对象模型参考：以上还需将关联关系说明补全。

动态模型参考：（1）脚本正常情况脚本：●储户有存款要求，填写存款单，包含储户个人信息，存款金额和存款类型；●业务员查收存款，审核存款与存款单存款金额吻合；●存款单生效；●储户有取款要求，填写取款单，包含个人账号、密码（待定）和存款金额；●业务员审核存款，验证储户身份，确定储户存款金额 > = 取款金额；●审核通过，取款单生效；●系统打印利息清单，业务员把本金和利息返回储户。

第4章形式化说明技术1．举例对比形式化方法和欠形式化方法的优缺点。

答：（1）欠形式化方法的缺点①矛盾矛盾是指一组相互冲突的陈述。

②二义性二义性是指读者可以用不同方式理解的陈述。

③含糊性例如，人们可能经常在文档中看到类似下面这样的需求：“系统界面应该是对用户友好的。

”实际上，这样笼统的陈述并没有给出任何有用的信息。

④不完整性。

如果在规格说明书中对一个命令的功能没有更多的描述，那么，这个命令的细节是严重不完整的。

⑤抽象层次混乱。

抽象层次混乱是指在非常抽象的陈述中混进了一些关于细节的低层次陈述。

这样的规格说明书使得读者很难了解系统的整体功能结构。

（2）形式化方法的优点①能够简洁准确地描述物理现象、对象或动作的结果。

在理想情况下，分析员可以写出系统的数学规格说明，它准确到几乎没有二义性，而且可以用数学方法来验证，以发现存在的矛盾和不完整性，在这样的规格说明中完全没有含糊性。

②可以在不同的软件工程活动之间平滑地过渡。

③提供了高层确认的手段。

可以使用数学方法证明，设计符合规格说明，程序代码正确地实现了设计结果。

2．在什么情况下应该使用形式化说明技术？使用形式化说明技术时应遵守哪些准则？答：（1）人们在理解用自然语言描述的规格说明时，容易产生二义性。

为了克服非形式化方法的缺点，人们把数学引入软件工程。

创造了基于数学的形式化说明技术。

（2）应用形式化方法的准则：①应该选用适当的表示方法。

②应该形式化，但不要过分形式化。

③应该估算成本。

④应该有形式化方法顾问随时提供咨询。

⑤不应该放弃传统的开发方法。

⑥应该建立详尽的文档。

⑦不应该放弃质量标准。

⑧不应该盲目依赖形式化方法。

⑨应该测试、测试再测试。

⑩应该重用。

3．一个浮点二进制数的构成是：一个可选的符号（+或-），后跟一个或多个二进制位，再跟上一个字符E，再加上另一个可选符号（+或-）及一个或多个二进制位。

例如，下列的字符串都是浮点二进制数：110101E-101-100111E11101+1E0更形式化地，浮点二进制数定义如下：其中：符号∷=表示定义为；符号[...]表示可选项；符号a|b表示“a或b。