软件规格说明技术-6.ppt

上海大学计算机学院 items 具有下列定律： dom(items s) = ran s items〈a1, ? , an〉= ? a1, ? , an ? items(s ? t) = items s ? items t items s = items t ? (?f: dom s ? dom t? s=f ; t) 6.2.2 一个排序的规格说明 现介绍一个简单的序列与包的应用例子：将一个序列按非递减序排序。 要求对给定的类型为 X 的对象序列 in?，操作的输出结果为一个所有元素以递增序出现的序列 out! 对于一个类型 X 的元素定义了一个全序，那么我们可以对 X 的元素进行排序。 X 上的一个全序关系是指： ?x: X ? x≤x (自反) ?x, y: X ? x≤y ?y≤x ? x = y (反对称) ?x, y, z: X ? x≤y ? y≤z ? x≤z (传递) 此外，≤还应该具有性质： ?x, y: X ? x≤y ? y≤x 这里，≤ 并不表示小于等于，仅表示了一种次序。自然数集合上的 ? (小于等于)关系是全序的一个例子。 集合X上的所有全序的集合 totord[X] 的形式定义: [X] totord： ?(X ? X) ?F: X ? X ? F ? totord ? (?x: X ? x ? x ? F ) ? (?x, y:X?{x ? y, y ? x} ? F ? x = y) ? (?x, y, z: X?{x ? y, y ? z}?F? x ? z?F) ? (?x, y: X?x ? y ? F ? y ? x? F) ) 为了能用 Z 来说明排序的操作，先定义一个类型为 (X ? X) ? ?(seq X) 的通用式函数 nondecreasing，它以一个全序作为自变量，产生全序下的所有非递减序的序列的集合。 [X] nondecreasing：(X ? X) ? ?(seq X) ?F: X ? X; ?: seq X ? ? ? nondecreasing F ? (?i, j:dom ? | ij ? ? i ? ?j ? F) nondecreasing F 是一个非递减序序列的集合当且仅当 F 是一个全序。现可给出排序的规格说明Sort[X]。 Sort[X] in?, out!：seq X F?：X?X F? ? totord[X] out! ? nondecreasing F? items (out!) = items (in?) 因为，在同一个集合上可以定义许多不同的全序，所以必须输入关系 F?。 排序的输出是非递减序的，故输出序列与输入序列所含的元素项以及出现的次数是相同的。这是由谓词 items (out!) = items (in?) 来表示的。 这个排序的规格说明使用了一个通用式模式，类似于一个带有形式参数的子程序。 6.2.3 一个自动售货机的规格说明 状态引入 现在介绍一个稍微大一点的使用包类型以及包的操作函数的规格说明。 这是一个关于自动售货机的例子。 需要有一个能由售货机卖出的所有商品的集合Good，因此 Good 是一个给定集合。在任何时候，由售货机卖出的商品是 Good 的子集。 售货机的状态说明为模式 VendingMachine。 VendingMachine coin：? ? cost：Good ? ? stock：bag Good float：bag ? dom stock ? dom cost ? dom float ? coin [Good] 在模式中，集合 coin 是所有可接受的英镑硬币的集合。每一个硬币以便士值标记。 函数 cost 返回的是以便士表示的该商品的价格。例如， cost(wispa)=17, cost(crisp)=19, cost(kitkat)=19 包stock记录了当前在售货机中每一种商品的数目。例如： stock={wispa ? 3, crisps ? 11, kitkat ? 1} 包float记录了当前机器中每一