Vol.21 No.1 蔡家楣等：软件开发过程的开发图描述 ·85· 文法的匹配函数并得到它的正确性证明，这一过 的名字.这是允许的，因为单元GRAMMAR和 程大致由下面几个开发步组成 GRAMMARI等价. (I)从已有单元MATCH导出新单元 由上面也可看出构成和演化的不同在于：演 GRAM MATCH,它基于已有单元GRAMMAR 化要求我们去研究某个（些）单元的开发历史，而 和REG2GRAM.MATCH和GRAM MATCH之 构成只提供整个系统在某个开发步上的一种定 间的关系应为等价关系，但这一点尚有待证 格效果.也可以看出，演化并不完全是独立 明.因此在图4的证明框中填人了1个问号，以表 的.GRAMMAR的演化是为了去证明因MATCH 明在此有1个须填人的证明需求. 演化而引人的语义关系，因此，我们常常为了实 现一个主要步而去完成一系列的次要步.当然也 Scan Scan 可以建立一种机制把若干次要步组合到一个主 要步中去 Match Match Gram Match 4开发图的完善 Reg2_Gram Reg2_Gram 在实际使用时，开发图的结点和边上还应标 RegExp RegExp Grammar 明属性，这些属性有两类： Grammar ()组织属性.对于单元来说是关于作者、产 生日期、非形式文件等，而对于开发步来说是指 Library Library 定的变换和非形式文件等. 图4Gram-Match (2)语义属性，对单元来说是一致性、初始性、 充分完备性、公理库等，对开发步来说是指关系， (2)为了证明上一步的正确性，就要在单元 如等价、行为等价、提纯等. GRAMMAR中加人I条定理，这样就产生了 例如，在LEX开发中用到这样一些语义属 GRAMMAR的I个新版本，叫GRAMMAR1.这 性.引人正则表达式的单元REGEXP带有属 个新版本是等价于老版本的，它的证明也在这一 性“initial”(初始性)：它很简单地引入了自由产生 步中完成.（见图5左边） 的表示正则表达式的构件， (3)GRAMMAR新版本的引进并不能自动解 而在单元REG2 AM GRAMMAR之间的边 决新版本的连接问题，这就需要外加一个开发 则是refer-.to涉及关系，有属性“persistent'”(一 步，该步的任务是把单元GRAM MATCH及其 致)，即不允许从正则表达式到文法转换的规范 他单元与GRAMMAR的新版本相连.填写第一 去改变文法的语义.在GRAMMAR和GRAM- 步所引人的等价关系说明框，删去GRAMMAR MAR1之间的导出关系边上则应标明属 的老版本（见图5右边）.而GRAMMAR新版本 性“equivalent”(等价). 由于老版本的删去而重新编号，现在编为老版本 Scan Scan Match Gram-Match 等价 Match Gram Match 证明 Reg2-Gram Reg2 Gram RegExp Grammar RegExp 等价 证明 Library Grammar Library Grammar 图5引入定理再联接蔡家嵋等 软件开 发过 程 的开 发 图描述 文法 的 匹 配 函 数 并得 到 它 的 正 确 性 证 明 这 一 过 程 大致 由下 面 几个 开 发步组 成 从 已 有 单 元 导 出 新 单 元 ， 它 基 于 已 有 单元 和 和 之 间 的 关 系 应 为 等 价 关 系 ， 但 这 一 点 尚 有 待 证 明 因此在 图 的证 明框 中填人 了 个 问 号 ， 以 表 明在此有 个须填人 的证 明需 求 扮 · 硫 之 称幼 的 名 字 这 是 允 许 的 ， 因 为 单 元 和 等价 由上 面 也 可 看 出构 成 和 演 化 的 不 同在 于 演 化 要 求 我 们 去研 究 某 个 些 单元 的 开 发 历 史 ， 而 构 成 只 提 供 整 个 系 统 在 某 个 开 发 步 上 的 一 种 定 格 效 果 也 可 以 看 出 ， 演 化 并 不 完 全 是 独 立 的 的演化是 为 了去 证 明 因 演 化 而 引 入 的语义 关 系 ， 因 此 ， 我 们 常 常 为 了 实 现 一个 主要步而 去完成 一 系列 的次要 步 当然 也 可 以 建 立 一 种 机 制 把 若 干 次 要 步 组 合 到 一 个 主 要 步 中去 为 了证 明上 一 步 的正 确性 ， 就 要 在 单 元 中 加 人 条 定 理 ， 这 样 就 产 生 了 的 个 新 版 本 ， 叫 这 个新 版本是 等价于 老版本的 ， 它 的证 明也 在 这 一 步 中完成 见 图 左边 新版本 的引进并不 能 自动解 决 新 版 本 的连 接 问题 ， 这 就 需 要 外 加 一 个 开 发 步 ， 该 步 的 任务 是 把 单元 及 其 他 单元 与 的新 版 本 相 连 填 写 第 一 步所 引人 的等价 关 系说 明框 ， 删 去 的 老 版 本 见 图 右边 而 新 版 本 由于 老 版本 的删去而 重新 编 号 ， 现 在编 为老 版 本 开发 图的完善 在 实 际使 用 时 ， 开 发 图的结 点 和边 上 还 应标 明属性 ， 这些 属性 有 两类 组 织 属 性 对于 单元来 说是 关 于 作 者 、 产 生 日期 、 非 形 式 文 件 等 ， 而 对于 开 发 步 来 说是 指 定 的变 换 和 非形式 文件 等 语义 属性 对单元来说是 一致性 、 初 始性 、 充 分 完 备性 、 公 理 库等 ， 对 开 发 步 来 说是 指 关 系 ， 如等价 、 行 为等价 、 提 纯等 例 如 ， 在 开 发 中用 到 这 样 一 些 语 义 属 性 引 人 正 则 表 达 式 的 单 元 带 有 属 性 “ ” 初 始性 它很 简单地 引人 了 自由产生 的表示 正 则 表达式 的构件 而 在 单元 之 间 的 边 则 是 免 一 涉 及 关 系 ， 有 属 性 “ ” 一 致 ， 即 不 允 许 从 正 则 表 达 式 到 文 法 转 换 的 规 范 去 改 变 文 法 的 语 义 在 和 之 间 的 导 出 关 系 边 上 则 应 标 明 属 性 “ ” 等价 一 们口们 · 证 明 飞 卜 证 明 之 们。 图 引入定理再联接