软件开发过程的开发图描述

D0I:10.13374/i.issn1001-053x.1999.01.024 第21卷第1期 北京科技大学学报 VoL21 No.1 1999年2月 Journal of University of Science and Technlogy Beijing Feb.1999 软件开发过程的开发图描述 蔡家楣) 杜国维2) 1)浙江工业大学信息工程学院，杭州3100042)北京科技大学材料物理系，北京100083 摘要提出一种开发图工具用来将程序开发过程形式化，描述开发中涉及的各种与不同方式相 关的单元集，从而解决对开发过程的分析修改和管理问题.并用UMX下的LEX作为例子说明了 这种工具的使用. 关键词程序开发过程；形式化：开发图；LEX 分类号TP311.1 软件的形式开发必须解决2个方面的问 1.1定义1构成 题：一是产品，也就是规范或程序.二是开发过 如果某个单元A的描述中引用单元B,就说 程.前者的描术一般用代数说明语言如Spec A涉及B(A refer to B),一张包含涉及关系的子 trum,Obscure;或函数式语言如ML,Opal;或面向 开发图叫构成(configuration). 对象的语言TROLL,C+等；甚至也可以用传统 图1是2个构成的例子.在多数用语言写的 语言如Pascal等来写.而后者即开发过程则较难 规范中涉及关系是严格层次化的.如在ML中，上 解决，这实际上是指一种途径的形式化问题，是 述涉及关系实际上就是1个结构(stucture).中所 一个软件系统通过这种途径从初始规范到最终 包含的子结构.但也有循环相关的情况， 实现逐步得以解决的过程.用一种统一的表示 来描述这种开发过程，可以有利于分析和传达开 发思想，而这就必须为这一过程的形式化提供一 种建立基于规范或编程语言的各种概念的集成 方式，并达到通用灵活、形式严密、管理简单3个 方面的要求，我们在课题中使用了一种称为开发 图的工具，它能很好地满足这些要求. 1开发图 在一个开发环境中所涉及的所有语言都提 图1构成的例子 供了将大型软件系统模块化的手段，我们把这样 1个模块化的实体叫作单元.在软件开发处理过 1.2定义2演化 程中，要做的工作就是产生、变换和修改这些单 如果1个单元是通过1个外开发步从某个已 元，并建立1个单元集，在这个单元集当中的单元 有单元得到的，称该新单元是由已有单元导出 彼此以不同方式相关，开发图表示的就是这样1 的.由导出关系来联结的单元集叫作演化 个单元集. (evolution).如图2.演化反映了1个软件开发过 在开发图中它以单元为结点，而以单元间的 程的片断，通常这种演化是1个开发序列，也可以 关系为边.其中水平边（箭头）表示改变数据结构 是1棵树.2个开发单元也可以通过上述2种情况 的开发步，而其他箭头则表示1个规范（或程序） 而相关，即既有涉及关系又有导出关系.比如从1 的模块化结构，可给出如下定义， 个给定的单元A导出了B,而B又与A相关. 1998-3-03收稿察家楣男，52岁，副牧授 下面用1个具体的例子说明用开发图描述的 *国家~863”高科技项目 开发过程，所用的例子是unix工具LEX中的词法

第 卷 年 第 期 月 北 京 科 技 大 学 学 报 软件开发过程 的开发图描述 蔡家梢 ’ 浙江工 业大学信息工 程学 院 ， 杭州 杜 国维 北京科技大学材料物理系 ， 北京 摘 要 提 出一种开发图工具用来将程序开发过程形式化 ， 描述开发 中涉及 的各种 与不 同方式相 关 的单元集 ， 从而解决对开发过程 的分析修改和 管理 问题 并用 下 的 作为例子说明 了 这种工具的使用 关健词 程序开发过程 形式化 开发 图 分类号 · 软 件 的 形 式 开 发 必 须 解 决 个 方 面 的 问 题 一 是 产 品 ， 也 就 是 规 范 或 程 序 二 是 开 发 过 程 前 者 的 描 术 一 般 用 代 数 说 明 语 言 如 咖 ， ‘ 或 函 数式语言如 ， 或面 向 对象 的语 言 ， 料 等 甚 至 也 可 以 用 传 统 语 言 如 等来写 而 后 者 即开 发 过 程 则 较 难 解 决 ， 这 实 际 上 是 指 一 种 途 径 的形 式 化 问题 ， 是 一 个 软 件 系 统 通 过 这 种 途 径 从 初 始 规范 到 最 终 实 现 逐 步 得 以 解 决 的过 程 川 用 一 种 统 一 的表 示 来描 述 这 种 开 发 过 程 ， 可 以 有 利 于 分 析 和传 达 开 发 思 想 ， 而 这 就 必 须 为 这 一 过 程 的形 式化提 供 一 种 建 立 基 于 规 范 或 编 程 语 言 的各 种 概 念 的集 成 方 式 ， 并 达 到 通 用 灵 活 、 形 式 严 密 、 管理 简单 个 方 面 的要 求 我们 在 课题 中使用 了一 种 称 为 开 发 图的工具 ， 它能很好地满足这些要求 定 义 构成 如果某 个 单元 的描 述 中引 用 单元 ， 就说 涉 及 ， 一 张包 含 涉 及 关系 的子 开发 图叫构成 图 是 个 构成 的例 子 在 多 数 用 语 言写 的 规范 中涉 及 关 系是 严格层 次化 的 如在 中 ， 上 述 涉及 关 系 实 际 上 就 是 个 结 构 盯 中所 包含 的子结构 但 也有循 环相 关 的情 况 开发 图 在 一 个 开 发 环 境 中所 涉 及 的所 有 语 言 都 提 供 了将大 型 软件 系 统模 块 化 的手段 ， 我们把 这 样 个模 块 化 的实体 叫作 单元 在 软件 开 发 处 理 过 程 中 ， 要 做 的工 作 就 是 产 生 、 变 换 和 修 改 这 些 单 元 ， 并建立 个单元集 ， 在这 个单元集 当中的单元 彼此 以 不 同方 式 相 关 开 发 图表 示 的就 是 这 样 个单元集 在 开 发 图 中它 以单元 为结 点 ， 而 以 单 元 间 的 关 系 为边 其 中水平 边 箭 头 表 示 改 变 数 据 结 构 的 开 发 步 ， 而 其 他 箭 头 则 表 示 个规范 或程 序 的模 块 化 结构 ， 可 给 出如下定义 一 一 收稿 蔡家相 男 ， 岁 ， 副教授 国家 “ ” 高科技项 目 图 构成的例子 定 义 演化 如果 个单元是 通 过 个外 开 发步从某 个 已 有 单 元 得 到 的 ， 称 该 新 单 元 是 由 已 有 单 元 导 出 的 由 导 出 关 系 来 联 结 的 单 元 集 叫 作 演 化 如 图 演 化反 映 了 个软 件 开 发 过 程 的片 断 ， 通 常这种 演化是 个开 发序列 ， 也 可 以 是 棵树 个 开发 单元 也 可 以通 过 上 述 种情 况 而 相 关 ， 即既 有涉 及 关 系又 有 导 出关系 比如从 个 给定 的单元 导出 了 ， 而 又 与 相 关 下 面 用 个具体的例子说 明用 开发 图描述 的 开 发过 程 ， 所 用 的例子是 工具 中的词法 DOI ：10．13374／j ．issn1001－053x．1999．01．024

·84· 北京科技大学学报 1999年第1期 扫描器部分， 一输人串重组方式为：其首部为输人序列中 的1个正则表达式的最长前缀所匹配. 开发的基本思想是把基于正则表达式的函 数SCAN的初始需求规范转换成基于语法的规 范，然后在文法层面上完成某种优化，最后推出1 个十分接近于通常的有限自动机实现的SCAN 版本.为了这一目的，要开发1个将文法及文法上 图2演化的例子 的操作建立模型的自包含库，以便于今后的对象 重用. 2用开发图表示的LEX开发过程 图3即是用开发图表示的这一开发过程，图 中的结点表示了代数说明语言所写的单元，而边 该扫描器的功能是当作用于1个输人字符串 则表示了单元之间的关系.为简单起见，我们把 和1个表示可能记号的正则表达式序列时返回1 标准库和文法库放在一个Library库中. 个记号序列和余下的输人串.每个记号必须是输 等价 实现 人串中尚未分析部分的1个“最长前缀”匹配，而 Scan Gram-Scan Gram_Scan I 如果有几个正则表达式都与同样长的串相匹配， 证明 证明 则选择它们中最前面的那1个四. Match 等价 Gram_match 这一开发过程的开始是用某种代数说明语 言来写出LEX的需求规范，其顶层函数是 证明 SCAN,下面是用SPECTRUM写的单元SCAN的 证明 Reg2_Gram 一部分： 实现 Reg2_Gram ，一、 实现「 scan:String X Seq Segexp-Seq Regexp x String RegExp Grammar Grammar I axioms Vs,s String:rs,ts:Seq Regexp in 证明 scan(s,rs)=(ts,s )= Library s is postfix of sA 图3LEX开发过程 (Vr:Regexp,rEts=>rErsA (ts=e=>s=s'Λ 3开发过程分析 Vs :String;r:RegexprErsAs => ((s r)is_prefix_match_of s) 观察图3可以看出它分为若干垂直和水平 A 层：左边的垂直层表示的是初始需求规范，单元 (ts≠e=>]sl,s2:String.s=sl.s2∧ SCAN定义了主函数scan,它基于单元MATCH Scan(s2,rs)=(rest ts,s )A 而MATCH定义了同正则表达式的匹配； (s1,first ts)is_longest_prefix_match_of(s,rs) MATCH又基于单元REGEXP.中间的垂直层则 )片 表示了开发的中间步，以文法为基础的扫描和匹 配.而右边的垂直层则表示了程序实现. endaxioms; 水平箭头是由推导步所产生的，它们所表达 该规范中的axioms部分叙述了这样几点： 的关系有等价(equvalent)、提纯(refinement)、实 一S是输人串的后部； 现(implementation)等.伴随这些推导步产生了一 一正则表达式的输出序列s的每一成员都 些验证需求，而由相应的验证活动所产生的证明 在输入序列s之中； (proof)则被标示在边上供以后参考.比如，在开发 一如果该字符串中没有非空前缀同s中的 过程中必须证明正则表达式上的匹配是等价于 一个正则表达式相匹配，则正则表达式的输出序 正规文法上的匹配的.这一证明就被标在从 列为空； MATCH到GRAM-MATCH的边上· LEX开发过程的任务之一是推出1种基于

北 京 科 技 大 学 学 报 年 第 期 扫描 器部分 ’ 图 演化的例子 用 开发 图表示 的 开发过程 该 扫描器 的功 能是 当作用于 个输人 字符 串 和 个 表示 可 能 记号 的 正 则表 达式序 列 时返 回 个 记 号 序列 和 余下 的 输人 串 每个 记 号 必须是 输 人 串中 尚未 分 析部 分 的 个 “ 最 长前 缀 ” 匹 配 ， 而 如 果 有 几个 正则 表 达式 都 与 同样 长 的 串相 匹 配 ， 则选 择它们中最前面 的那 个 这 一 开 发 过 程 的 开 始 是 用某 种 代 数 说 明语 言 来 写 出 的 需 求 规 范 ， 其 顶 层 函 数 是 ， 下 面是 用 写 的单元 的 一部分 一 甲 ， ， ， ， 夕 八 ， ‘ 〔 八 ’ 八 军 ‘ 八 羊 ， 少 羊 ， 八 ， ， ， ， 该规范 中的 部 分叙 述 了这样 几点 一’ 是 输人 串的后 部 一正 则 表 达 式 的 输 出序 列 的 每 一 成 员 都 在输人 序列 之 中 一如 果 该 字 符 串中没 有 非 空 前 缀 同 中 的 一个 正 则 表 达 式相 匹 配 ， 则 正 则 表 达 式 的输 出序 列 为空 一输人 串重 组 方 式 为 其首部 为输人 序列 中 的 个正则表达式的最 长前缀所 匹 配 开 发 的基 本 思 想 是 把 基 于 正 则 表 达 式 的 函 数 的 初 始 需 求规 范转换 成基 于 语 法 的规 范 ， 然后 在 文法 层 面上完成某种 优化 ， 最后 推 出 个 十 分 接 近 于 通 常 的 有 限 自动 机 实 现 的 版本 为了这一 目的 ， 要 开发 个将文法 及 文法上 的操 作建 立模 型 的 自包含 库 ， 以便 于 今 后 的对象 重 用 图 即是 用 开 发 图表示 的这 一 开 发 过 程 ， 图 中的结 点表示 了代数说 明语 言 所 写 的单元 ， 而 边 则 表 示 了单元 之 间 的 关 系 为 简 单起 见 ， 我 们 把 标 准库和 文法库放在 一个 库 中 等价 实现 证 明一 等价 竺窄 几匕 比 糕碧孚缨 证 明 上 一 ，一 一 八 一 、 证 明 实现 一 们。 实现 证明 图 开发过程 开发过程分析 观 察 图 可 以 看 出它 分 为 若 干 垂 直 和 水 平 层 左 边 的 垂 直 层 表 示 的 是 初 始 需 求 规 范 ， 单 元 定 义 了 主 函 数 ， 它 基 于 单 元 而 定 义 了 同 正 则 表 达 式 的 匹 配 又 基 于 单元 中 间 的 垂 直层 则 表示 了开 发 的 中间步 ， 以 文法 为基 础 的扫描和 匹 配 而右边 的垂 直层则表示 了程序 实现 水平箭 头是 由推 导步所 产 生 的 ， 它 们 所 表 达 的 关 系 有 等 价 、 提 纯 、 实 现 等 伴 随这 些 推 导步 产 生 了 一 些 验 证需 求 ， 而 由相 应 的验 证 活 动所 产 生 的证 明 则被标示 在边 上供 以 后 参考 比如 ， 在 开 发 过 程 中必 须 证 明 正 则 表 达 式 上 的 匹 配 是 等 价 于 正 规 文 法 上 的 匹 配 的 这 一 证 明 就 被 标 在 从 到 一 的边 上 开 发 过 程 的 任 务 之 一 是 推 出 种 基 于

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引入定理再联接

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

·86* 北京科技大学学报 1999年第1期 依附于开发图结点或边的属性必须加以证 过可视化编程工具对它们进行处理等，就有可能 明，对语义属性来说这种证明是一种形式证明， 实现把规范说明开发与提纯证明集成于一个 而对非形式属性来说应是一种非形式的论证.如 ICASE环境之中，无疑是很有意义的.在我们的 在LEX例中，为了证明GRAMMAR和GRAMM- 课题里已经用这种方法结合代数说明语言及 AR1等价，必须形式地证明下面的特性应是由该 ECC扩展构造逻辑进行了上述工作，证明是有效 规范导出的一条定理： 可行的. Vg1,g2:grammar in L(gl,Ig2)=L(gl)UL(g2). 参考文献 意为：由文法并集产生的语言是2个语言的并集， 关于证明的管理有多种方法，如可以把它们 I Broy M.Methodische Grundlagen der Programmierung, 看作是与规范、实现、模块类似的单元，或者看作 Informatik and Mathematik.NY:Springer Press,1990. 是一种特定的属性，甚至看成是开发过程本身. 355~365 不同的管理各有优缺点，可以视不同情况而定. 2 Axel Dold,Martin Strecker.Program Development 开发图在应用中还有一些问题可以讨论，比 with Specification Operators-illustrated by Aspecifica- tion of the LEX Scanner.Ulm:Uniiversity Ulm Press, 如如何把边重新连接，如何删去边和结点，以及 1993.203~208 如何把独立的子开发图组合成更大的开发图等. 3 Abdelwaheb Ayari.Stefan Friedrich,Ramses A,Heck- 5结束语 ler,Jacques Loecks.Das Fallbeispiel LEX.Saar- brueken:University Saarbrueken Press,1992.65~70 在大型软件形式开发过程中，运用开发图工 4 Matthias Weber.A Meta-Calculus for Formal System 具可以把开发过程及其中的单元关系形象直观 Development.Oldenbourg:Oldenbourg Press,1991. 地表示出来，既便于分析修改也便于管理.如通 110~120 Development Graph to Describe Development Process of Sortware Cai Jiamei,Du Guowei2) 1)Institute of Information,Zhejiang University of Technology.Hangxhou 310014.China 2)Department of Materials Physics,UST Beijing,Beijing 100083.China ABSTRACT A development graph tool to formalize a development process of program is proposed. It describes a collection of units that are related to each other in various way.This tool provides a possibility to solve analysis,modify management of a ddevelopment process,The use of this tool is showed with a example LWX of UNIX. DEY WORDS development process of program;formalization;development graph;LWX

北 京 科 技 大 学 学 报 年 第 期 依附 于 开 发 图结 点 或边 的 属 性 必 须 加 以 证 明 ， 对语义 属 性 来 说 这 种 证 明是 一 种 形 式 证 明 ， 而 对非形 式 属 性 来说应 是 一 种 非 形 式 的论 证 如 在 例 中 ， 为 了证 明 和 一 等价 ， 必须 形 式 地 证 明下 面 的特性 应是 由该 规范 导 出的一条定理 ， ， 意为 由文 法并集 产 生 的语 言是 个语言 的并集 关于 证 明 的管 理 有 多 种 方 法 ， 如 可 以 把 它们 看作是 与规范 、 实 现 、 模 块 类 似 的 单元 ， 或 者看 作 是 一 种 特 定 的 属 性 ， 甚 至 看 成 是 开 发 过 程 本 身 不 同的管理 各有优缺 点 ， 可 以 视不 同情况而定 开 发 图在 应 用 中还 有 一 些 问题 可 以讨论 ， 比 如 如 何 把 边 重 新 连 接 ， 如 何 删 去 边 和 结 点 ， 以 及 如何 把独立 的子 开 发 图组合成更 大 的开 发 图等 过 可视 化编程 工具 对它 们进行处理 等 ， 就有 可 能 实 现 把 规 范 说 明 开 发 与 提 纯 证 明 集 成 于 一 个 环 境 之 中 ， 无 疑 是 很 有 意 义 的 在 我 们 的 课 题 里 已 经 用 这 种 方 法 结 合 代 数 说 明 语 言 及 扩展构造 逻辑进行 了上 述 工作 ， 证 明是有效 可行 的 参 考 文 献 结束语 在 大 型 软件形 式 开 发 过 程 中 ， 运 用 开 发 图工 具 可 以 把 开 发 过 程 及 其 中 的 单元 关 系 形 象 直 观 地 表 示 出来 ， 既 便 于 分 析 修 改 也 便 于 管理 如 通 ， 议 水 ， ， 一 ， ， ， ， ， 工 ， 一 一 ， ， ， 勺 ， ， ， ， · ， ， 说