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