第9章--形式化方法.pptVIP

基本概念 根据形式化的程度，可以把软件工程方法划分成非形式化、半形式化和形式化三类。使用自然语言描述需求规格说明，是典型的非形式化方法。使用数据流图或实体—关系图等图形符号建立模型，是典型的半形式化方法。 用于开发计算机系统的形式化方法，是描述系统性质的基于数学的技术。 软件开发中的数学 数学最有用的性质之一是，它能够简洁、准确地描述物理现象、对象或动作的结果，因此是理想的建模工具。 在软件开发过程中使用数学的另一个优点是，可以在软件工程活动之间平滑地过渡。不仅功能规格说明，而且系统设计也可以用数学表达，当然，程序代码也是一种数学符号(虽然是一种相当繁琐、冗长的数学符号)。 数学作为软件开发工具的最后一个优点是，它提供了高层确认的手段。可以使用数学方法证明，设计符合规格说明，程序代码正确地反映了设计结果。 应该建立详尽的文档。建议使用自然语言注释来配合形式化的规格说明，以帮助读者理解系统。 不应该放弃质量标准。在系统开发过程中必须一如既往地实施其他SQA活动。 不应该盲目依赖形式化方法，这种方法并不能保证系统绝对正确。 应该测试、测试再测试。由于形式化方法不能保证系统绝对正确，因此，软件测试的重要性并没有降低。 应该重用。即使使用了形式化方法，软件重用仍然是降低软件成本和提高软件质量的唯一合理的方法。 数学预备知识 为了有效地应用形式化方法，软件工程师必须具有与集合和序列相关的数学符号知识，以及谓词演算中的逻辑符号方面的知识。 集合与构造性规格说明 集合是对象或元素的聚集，被用于形式化方法的基础。集合中包含的元素是唯一的(即，不允许重复)。具有少量元素的集合用花括号括起来，元素间用逗号分开。例如，集合 ｛C＋＋，Smalltalk，Ada，COBOL，Java｝ 包含五种程序设计语言的名字。 应用数学符号描述形式化规格说明 为了说明数学表示法在软件构件的形式化规格说明中的使用，我们前面提出的块处理器的例子。回顾一下，计算机操作系统中的一个重要构件维护用户创建的文件。块处理器维护一个未用块池，并同时保持对当前被使用块的跟踪。当块从被删除文件释放时，它们通常被加入到等待进入未用块池的块队列中。这一点如图2 所示。 形式规格说明语言 形式规格说明语言通常由三个主要的成分构成： (1)语法，定义用于表示规格说明的特定表示方法； (2)语义，帮助定义用于描述系统的“对象的全域(universe of objects)” ； (3)一组关系，定义确定哪个对象真正满足规格说明的规则。 Z规格说明语言 Z（正确读音为“zed”）是在过去二十年里发展起来的规格说明语言，已在形式化方法领域中广泛使用。 使用Z语言需要具备集合论、函数、数理逻辑等方面的知识。 Z语法及语义 Z规格说明由一组格（schema，盒子式的结构）组成，用于说明变量及这些变量之间的关系。一个schema 实质上类似于程序设计语言构件的形式化规格说明。 一个schema描述系统存取及修改的存储数据。在Z语言中被称为“状态”。Schema能够标识系统内用于改变状态及关系的操作。 使用Z举例 我们使用Z 规格说明语言对本章前面介绍的块处理器的例子建模。下面schema 的例子描述了块处理器的状态和数据不变式： 有穷状态机 利用有穷状态机可以准确地描述一个系统，因此是表达规格说明的一种形式化方法。 下面通过一个简单例子介绍有穷状态机的基本概念。 一个保险箱上装了一个复合锁，锁有三个位置，分别标记为1、2、3，转盘可向左（L）或向右（R）转动。这样，在任何时刻转盘都有6种可能的运动，即1L、1R、2L、2R、3L、3R。保险箱的组合密码是1L、3R、2L，转盘的任何其他运动都将引起报警。 从上面这个简单例子可以看出，一个有穷状态机包括下述5个部分：状态集J、输入集K、由当前状态和当前输入确定下一个状态(次态)的转换函数T、初始态S和终态集F。 有穷状态机的概念在计算机系统种应用非常广泛。 例如，每个菜单驱动的用户界面都是一个有穷状态机的实现。一个菜单的显示和一个状态相对应，键盘输入或用鼠标选择一个图标是使系统进入其他状态的一个事件。状态的每个转换都具有下面的形式： 当前状态〔菜单〕+事件〔所选择的项〕＝下个状态 为了对一个系统进行规格说明，通常都需要对有穷状态机做一个很有用的扩展，即在前述的5元组中加入第6个组件——谓词集P，即把有穷状态机扩展为一个6元组，其中每个谓词都是系统全局状态Y的函数。转换函数T现在是一个从(J-F)×K×P到J的函数。现在的转换规则形式如下： 当前状态〔菜单〕+事件〔所选择的项〕+谓词=下个状态 有穷状态机方法采用了一种简单的格式来描述规格说明： 当前状态+事件+谓词=下个状态