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