软件规格技术说明-复习资料

软件规格技术说明 第 1 章 1 什么是形式方法 形式方法是基于坚实的数学基础来描述和开发系统软件的方法 用严格的数学符号和 数学法则对软件系统的结构与行为进行有效的综合 分析和推理 它为系统的说明 开发 和验证提供了一个规范框架 2 软件形式方法有什么优点 1 形式规格说明是精确的 2 由误解引起的错误减少 3 形式规格说明利于系统实现 4 能够对形式规格说明进行正确性证明 3 什么是 Z 语言 Z 语言是基于一阶谓词逻辑一阶谓词逻辑和集合论集合论的形式规格说明语言 4 软件规格说明有哪两种抽象 过程抽象过程抽象和数据抽象数据抽象 过程抽象描述的是软件系统要实现的功能 而不是如何实现其功能的具体步骤 数据 抽象就是在规格说明中使用集合 关系 映射 序列 包等抽象的数学结构 而不必担心 这些结构最终是如何实现的 5 程序设计语言用于描述什么 程序设计语言可克服自然语言的缺陷 人们可用它来描述规格说明描述规格说明 程序可以被看成 是一种计算机可执行的规格说明 程序描述的是 怎么做 而不是做什么 因此 程序设计 语言不适合用来描述抽象程度较高的规格说明 第 2 章 1 什么是命题 命题是具有确定真假意义的陈述句 什么是命题公式 命题逻辑中的命题公式 是如下定义的一个有穷符号串 1 原子是命题公式 2 若 P Q 是公式 则 P P Q P Q P Q P Q 都是命题公式 3 命题公式仅通过有限次使用 1 2 获得 4 为了减少使用圆括号的数量 约定最外层的圆括号可以省略 什么是命题演算 命题逻辑等值演算 根据已知的等值式推演出与原命题公式等值的新的命题公式的过 程称为等值演算 2 什么是真值表 对于一个公式 G 将 G 在其所有解释下所取真值列成一个表 称为 G 的真值表 3 什么是命题公式的解释 有多少个 设 G 是命题公式 A1 An是出现在 G 中的所有命题变元 对 A1 An的一组 真值赋值称为 G 的一个解释 记作 I 共有 2n个 4 什么是谓词 带有参数的命题成为谓词 什么是谓词公式 谓词逻辑中的谓词公式 简称公式 可以递归地定义如下 1 原子是公式 2 如果 P Q 是公式 则 P P Q P Q P Q P Q 是公式 3 如果 P 是公式 x 是 P 中的变量 则 xP xP 是公式 4 公式仅通过有限次使用 1 2 3 获得 什么是谓词演算 利用等值式和定律进行谓词等值演算 5 什么是证明 由给定的前提 在推理过程的每一步 给出证明证据 最后得出所要的结论 什么是定理 定理是经过受逻辑限制的证明为真的陈述 6 请叙述谓词逻辑中的一点规则 one point rule P24 若已有一个含存在量词的命题公式 其中对量词给定了一个确定值 则可以消去量词 用已知值来替换所出现的量词变量 7 命题公式的证明见例 2 1 2 3 P21 8 谓词公式的证明见例 2 4 2 6 P25 9 幂集 设 A 是一个集合 由 A 的所有子集所组成的集合 称为集合 A 的幂集 记作 PA 如果有穷集合 A 的元素个数为 n 则其幂集的元素个数为 2n 10 序偶和笛卡尔积 m n 由两个对象 x 和 y 按一定次序排列而成的序偶 记作 x y 对于自然数 n n 个对象 a1 a2 an 按一定次序排列成的一个 n 元组 记作 a1 a2 an 设 A B 是任意两个集合 若序偶的第一元素是 A 的一个元素 第二元素是 B 的一个 元素 则所有这样的序偶集合 称为 集合 A B 的笛卡尔积 记作 A B 即 A B x y x A 且 y B 第 3 章 1 Z 的基本类型有哪些 基本类型 整数类型 Z N N1 复合类型 幂集类型 笛卡尔积类型 序列 包 模式类型 2 给定类型 整数类型 幂集类型 笛卡尔积类型 枚举类型 给定类型 基本类型有时被称为给定集合或给定类型 是由一对方括号括起来的名所 组成的基本类型定义引入 整数类型 Z 整数类型是 Z 的内定义基本类型 对任意类型使用类型构造符 可构 造出其他的类型 幂集类型 使用一个规格说明中的任意类型和幂集构造符 P 就可以产生该类型的幂 集类型 笛卡尔积类型 对于若干个集合 它们都已有类型 则它们的笛卡尔积就是一个新的 类型 笛卡尔积类型 3 集合和类型是什么关系 一方面 每一个类型是一个集合 若引入了一个基本类型或者使用 P 构造了一个类型 则可以把这个类型看成是一个集合 还可以引用它的元素 并可使用有关的集合操作 另一方面 当某个元素是多个集合的元素时 他只能属于一个类型 类型是一种特定的类的集合 它被看成是一个 最大集合 因为它代表了一个元素 可以属于的最大的可能的集合 4 对象声明 一个声明可以是 x T 的形式 其中 T 是一个类型 或是 y S 的形式 其中 S 是某一个 类型的子集 对象声明的缩写方法允许使用已经引入的集合的定义来写声明 对于 y S 这种形式的声明 必须强调两点 通过检查 S 的定义可知它的元素必须具 有的类型 从而确定 y 的类型 限制了 y 必须满足 S 所定义的性质 5 扩充表示法 Declaration 声明 Constraint 约束 Predicate 谓词 Decls Constr Pred 对所有的 Decls 如果 Constr 被满足 则 Pred 一定被满足 Decls Constr Pred 存在 Decls 它满足 Constr 而且它也满足 Pred Decls Pred ExPr 它表示了所有这样的值的集合 这些值是由 Decls 中满足限制 Pred 的变量以 ExPr 项的形式确定的 在 Z 中 使用操作符 可得到集合中的元素个数 3 2 中的例 3 6 3 8 P37 6 公理描述 整除 P50 图 4 2 公理定义引入了一个或多个全程变量和关于它们的谓词 这些谓词给出了进一步的信 息 7 通用式定义 包括 的通用式定义 有关的习题 3 9 3 14 3 15 3 18 iden iden 声明部分 谓词部分 第 4 章 1 关系 笛卡尔积和子集 在 Z 中 关系是一个序偶的集合 X 和 Y 的一个关系 R 是笛卡尔积 X Y 的子集 也 就是说 R X Y 故称关系是序偶的集合 2 源集和目标集 定义域和值域 在定义二元关系的时候 需要声明该关系所关联的两个元素所属的集合 这两个集合 分别被称为源集和目标集 关系的定义域是关系源集的一个子集 该子集中的任一元素至少与目标集中的一个元 素有给定的关系 关系的值域是关系目标集的一个子集 对于该子集中的任意元素 在源集中都有元素 与其有给定的关系 3 关系运算 特别是复合 逆 定义域限定 减 值域限定 减 映像 关系复合 恒等关系 id X 闭包xxXx 关系的逆 R xyRyxYyXx 定义域限定 RyxSxYyXxRS 值域限定 RyxTyYyXxTR 定义域限定减 RyxSxYyXxRS 值域限定减 RyxTyYyXxTR 映像 根据源 U 找目标 RyxUxYyUR 4 函数 部分函数 全函数 入射函数 满射函数 对这样一个关系 若任一元素关联到值域中唯一的一个元素 则该关系就是函数 部分函数 没有规定定义域是整个源集 对任何集合 X 和 Y X 到 Y 的部分函数是唯 一地映射定义域中的元素到值域中元素的所有关系 部分函数一般就称为函数 zyRzxRyxYzyXxYXRYX 全函数 定义域是整个源集 全函数是部分函数的子集 XfYXfYX dom 入射函数 在函数的定义域中不会有两个元素映射到值域中的同一元素 也称一对一 函数 入射函数也分为部分入射函数和全入射函数 左边加上箭尾符号 满射函数 函数的值域是整个目标集 满射函数分为部分满射函数和全满射函数 双箭头符号 5 二元关系和一个自变量的函数有什么区别 函数式一种特殊的关系 一个关系可以关联其定义域的任意多个元素到其值域中的任 意多个元素 关系是一个多对多的映射 若源集中的任一元素最多关联到目标集中的一个 元素 则该关系就是函数 6 函数叠加操作 函数叠加 设 f 和 g 都是类型为 X Y 的函数 这里 X 是源集 Y 是目标集 则 该操作从 f 中删除了所有这样的序偶 其第一元素属于 ggfgdomgf 的定义域 然后将函数 g 中的新的序偶添加进去 7 表示法 表示法 由声明加上谓词再跟上一个项的结构组成 其一般形式为 decls pred term 该表达式以 decls pred 为自变量 将它们映射到由 term 所定义的值 8 书中的例题和习题 4 4 4 6 4 17 4 33 4 34 4 36 第 5 章 1 模式的用途 模式的一个重要功能就是描述系统的抽象数据类型的状态 2 状态模式 和初始状态模式 状态模式 描述目标软件系统某一部分数据类型的结构特征的模式 称为状态模式 状态模式定义了目标软件系统某一部分的状态空间及其约束特性 系统中该部分的状态存 在于状态空间之中 S 由前状态模式 S 和后状态模式 S 组合得到 S S S 可以在任何不引起改变 S 状态操作的规格说明中使用 S No Change 初始状态模式 InitS S 谓词 初始化变量为空 3 模式包含 模式包含是指一个模式将另一个模式的名包含在其声明中 模式 4 模式运算 包括连接词连接 复合等 P85 命题联结词连接模式 S T S T S T S T S 模式复合 模式 A 定义为模式 B 和模式 C 的复合 如果模式 B 引起变量 S1 改变为 S2 而模式 C 引起变量 S2 改变为 S3 则模式 A 就会产生变量 S1 到 S3 的改变 模式复合 要使用换名和隐蔽两个操作 5 操作模式 前置条件模式 前置条件模式和计算过程 求模式的前置条件 对一个描述了某操作的模式 其前置条件就是这样一个精确的操 作 在该条件下 给定的操作数可应用的 前置条件运算符记作 Pre 它只能应用于描 述操作的模式 前置条件模式 通过求模式的前置条件运算所求得的结果 一个操作模式 S 的前置条件的计算过程 对给定的模式 从它的声明部分中删除输出从它的声明部分中删除输出 变量和后状态变量变量和后状态变量 并在谓词部分将它们用存在量词进行约束 S 输出变量 类型 S 的谓词部分 记为 PreS 6 熟悉 电话号码数据库 的例子和 班级管理 的例子 第 6 章 1 什么是序列 序列与通常的集合有什么区别 在 Z 中 可以用序列来模拟有序的数据对象集合 在一个序列中 一个元素的出现次序是有意义的 而且每个元素可以出现多次 在集 合中 元素的出现次序是无意义的 且每个元素只可以出现一次 2 序列的连接 逆置 包括通用式 序列连接 把一个序列放在另一个序列的后面而将它们连接成一个新的序列 序列逆置 将一个序列的所有元素取逆序所构成 rev 3 Head tail front 和 last 操作 包括通用式 书 6 1 4 head 取序列的第一元素 tail 删除第一元素 取剩下的序列 front 删除最后一个元素 取剩下的序列 last 取序列的最后一个元素 4 什么是包 包与通常的集合有什么区别 在一个包中 同一个对象的多重出现时有意义的 出现的次序是无关紧要的 5 包的表示 用双线方括号括起的包的成员的方法来表示一个包 6 包的操作函数的通用式定义 计数函数 count 告诉人们一个对象在一个包中出现的次数 包括大函数 为包中每一个元素的出现次数乘上一个倍数 元素关系 in 判断对象 x 是否为包 L 的成员 子包关系 方 判断一个包是否为另一个包的子包 包并 包中每一个对象出现的次数是它在两包中出现次数之和 包差 包中每一个对象出现的次数是它在两包中出现次数之差 差为负数则取零 项函数 items 对给定的序列 S 返回 S 的元素的包 模式的例子 1 PhoneDB 引入 P48 模式 PhoneDB P51 模式 AddEntry P76 后状态模式 PhoneDB P77 包含 PhoneDB 和 PhoneDB 的 AddEntry P78 PhoneDB 重写的 AddEntry P78 模式 RemoveEntry P79 PhoneDB P80 InitPhoneDB P81 使用命题连接词的规格说明 P82 83 模式复合 P87 88 2 Class 引入 P42 后状态模式 Class P77 操作模式 Enrollok P79 录取一个学生 Class P80 AlreadyEnrolle