软件工程-第十章-形式化方法.ppt

软件工程Software Engineering 第十章 形式化方法 形式化方法提供了规约环境的基础，它使得所生成的分析模型比用传统的或面向对象的方法生成的模型更完整、一致和无二义性。集合论和逻辑符号的描述设施使得我们可以创建清晰的关于事实的陈述。 支配形式化方法的基本概念是：数据不变式、状态、离散数学、序列相关联的符号体系、形式化规约语言。 10.1 形式化方法 形式化方法的定义 定义10—1：用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术。这样的形式化方法提供了一个框架，人们可以在框架中以系统的方式刻划、开发和验证系统。 形式化方法主要思想 利用形式化规格说明语言定义用户需求，并采用数学推演的方法证明需求定义的性质，例如一致性、实时系统的活性和公平性等。对于复杂的应用问题，尽管无法验证整个需求定义的完全性，但仍有可能为避免某些要点的疏漏而建立数学断言，然后予以形式证明或反驳。 形式化方法是克服需求分析阶段不精确性、不一致性和不完全性的有效途径。 10.1.1 形式化方法概念 例10--1：符号表(如右图)：它由一组没有重复的项构成。程序被用于维护一个符号表，在许多不同类型的应用中使用此符号表。 如果对于上表有一个陈述：包括不多于Max2D的用户名，那么就为表设定了一个限制，这就称为数据不变式的条件的一个构成成分。数据不变式是一个条件，它在包含一组数据的系统的执行过程中总保持为真。 上面讨论的符号表的数据不变式有两个构成成分： (1)表中包含的名字数不超过MaxIds。 (2)在表中没有重复的名字。 状态的概念 在形式化方法的语言环境中，状态是系统访问和修改的存储数据。在上述符号表程序的例子中，状态是符号表。 操作的概念 这是在系统中发生的读或写状态数据的动作。 10.1.2 数学知识 1. 集合和构造性规约 所谓集合，乃是有某些可以相互区分的如何对象，如数、变量、函数、字母、数字、图、语言、程序、事件等，或者没有任何对象，汇集在一起所组成的整体。 例10--2：一个包含4个元素的自然数集合： ｛1，3，5，7｝ 例10--3：包含五种程序设计语言的名字的集合： ｛C ，C＋＋， Pascal， Basic， FORTRAN ｝ 例10--4：下面的数的聚集不是集合，因为它包含了重复的元素2： ｛33，2，99，11，22，88，2｝ 在集合中，元素出现的顺序是不重要的。我们将集合中元素的数量称为集合的基数(cardinality)，并用操作符#返回集合的基数。 例10--5：表达式说明用于已知集合的基数操作符，其结果指出集合中项的数量： ＃｛A， B， C， D｝＝ 4 如果要定义一个集合，可以通过枚举出集合的元素来定。也可以是创建一个构造性集合规约，这种方式是用布尔表达式来刻划集合成员的一般形式。 例10--6：下面是一个构造性规约的例子： ｛n：N｜n＜ 5·n｝ 这个规约中有三个部分： ①：基调n：N； ②：谓词n＜5； ③：项n 。 基调刻划在形成集合时考虑的值的范围，谓词定义集合如何被构造，项则给出集合中项的一般形式。 2. 集合运算符 用命题法定义两个集合的运算。 定义10--2 设A，B为任意两个集合。令 A∪B={x│ x∈ A或x ∈B} A∩B={x│ x ∈A和 x∈B} A－B={x│ x ∈A且x B } A B=（A∪B）－（A∩B） 集合的运算可以用文氏图如图直观地表示。图中的阴影部分表示运算的结果。 3．笛卡尔乘积 4. 逻辑运算符 ?4. 序列 10.1.3 应用数学符号描述形式规约 例10--18：块处理器 在操作系统中一个更重要的部分是维护由用户创建的文件的子系统，块处理器是文件子系统中的一部分。文件存储中的文件由存储设备上的存储块构成，在计算机的操作中，文件被创建和删除，需要存储块的获取和释放。为了处理这些，文件子系统维持一个未用块池，并将保持对当前使用块的跟踪。当块从被删除文件释放时，它们通常被加入到等待进入未用块池的块队列中。如图所示. ?对这个子系统而言，状态是自由块的集合、已用块的集合、以及返回块的队列，数据不变式用自然语言表达如下： 1.没有块同时被标记为未用和已用。 2.所有在队列中的块集合将是当前已用块集合的子集。 3.没有队列元素包含相同的块号。 4.已用块和未用块的集合将是组成文件的块的总集。 5.在未用块集合中没有重复的块号。 6.在