第 卷 第 期 匕 石 灿 夕 · 人 工 智 能及 识 别 技 术 · 计 算 机 工 程 年 月 文 章编 号 一。一。刁 月 一 刊 定理证 明 辅 助 工 具 廖 宇 , 杨 大军 南京 大学计 算机科 学与技术 系 , 南京 文献标 识码 中图 分 类 号 剖析 是斯 坦福研 究机 构 开 发 的 强 大 的 规 约 、 验证 系统 , 它 的 适 用 领 域广 泛 在概要介绍 的 构 成 、 功 能 后 , 着重 分析 了 的 规 摘 要 约语 言 、 验证 系统 的 特 点 , 以 及使得 关键词 规 约语 言 定理证 明 器 形 式化 方 法 灵 活 、 强 大 的设 计 决 策和 内在机制 , 一 , 只 只 一 一 , , , · ’ , , 洋 是原 型 验证 系统 的 目 的 是把它作为一个重量级验证 系统 所需 的相 关技术 , 的 缩 写 , 斯 坦 福 研究机构 在过去 年 中开发 了一 系列验证 系 统 , 开 发 的轻量级原 型 , 以 探索实现 这 一名 字正是 由此 而 来 我们 在设计并发 面 向对 象广谱规约 语 时 , 拟 对 该 语 言 的 核 心 部 分 进行 验证 , 因 言 一 此 , 对 作 了较为深入的剖析 为在计算机科 学中严格 、 高效地应 用 形 式化方 法提 供 自动化的机器 支持 , 它 易于安装 、 使用 和 维护 , 足一个 良 好 的集成环境 该 系统主要 包括规约语言和定理证明 器 两 部 分 , 并且还 集成 了解释器 、 类 型检查器及预 定义的规 约库和 各种 方便的 浏 览 、 编 辑工 具【‘ 提供的规约语言基于 高 阶逻拜 , 具有丰富的类型 系统 , 是一般适用 的语言 , 表达能 力很强 , 大多数数学概念 、 计算概念均可用 该语言 自然直接 地表示 出来 的 定理证 明器 以 交互 方 式 工作 , 同时又 具 备 高度的 自动化 水准 它 的命令的 能 力很强 , 琐屑 的证明 细 节为证 明 器 的 内部推理机制掩盖 , 使得用 户仅在 关健决策点 上控制证明 过程 为在计 算机科学中应 用 形 式化方法提供机 器 支持 , 然 而 形 式化方法可 以 以 不 同 的 方式 、 风格 、 不 同程度 的严 格 性 , 应 用 于 不 同 的 目 标 例 如 , 最早 的形 式化方 法用 于对程 序作正 确 性证明 即驻行正 一段 以 实现级的程序设计语言 书写 的程序 满足 已知为 正确 的详 细规约 并 不适合这种程 序 正 确 性验证 工作 , 它 的设计 目 标是辅助 形 式化方 法在计算机 系统开发的早期 阶段的应 用 。 欲应 用 形 式化方 法 , 首先要有 一 个对所研究对 象 硬件 系统 、 软件 系统 、 算法等 的准确 的形 式化描述 , 即一个正确 的 形 式化规约 然 而 , 要获得 正 确 的形 式化规约 , 仅引入形 式化方 法是不 够的 , 提供如 下 机制 用 以 保证规 约 的 正 确 性 在规约语 言 中引入 丰 富的类 型 系统 通过严格的 类 型检查来及早发现规约 中的错 一个规 约 相 当 于一套公理 系统 , 提 出一 系列 关 于 误 此公理 系统 的定理 , 如果规约 是正确 的 , 那 么 这些 定理应 该 的 定理证 明 器构造这些 定 理的证明 来验 成立 , 通过应 用 一 一 证规约 的正确 性 。 这样 , 的规约 。 的规 约 语 言 可 用 于构 造充分可信 为 ’正 确 ’ 一 当前 自动验证 系统分为典型 的 两类 一类拥有极其有效 的 自动定理证明机制 , 然 而 其规约 语言的表达能力却十分有 定理证 明 器仅仅使用 简单的 无 限 , 例 如 强 大的 类型 的构造一阶逻辑作为其规约语 言 的基础 另一类恰恰相 反 , 拥有表达能 力丰富的规约语言却缺少有效的定理证明 器 提供推理 的机器 支持 , 例 如 支持灵 活 的 和 的 ’证 明 助 手 , 的演绎推理机制相 当贫乏 因此在语 言的表达能力与 机 器 的辅助推理 能力之间存在一个权衡 , 采取一条中间 道 路 , 它 既有强有 力 的机器推理 支持 , 规约语 言 又有足够丰 富的表达手段 下 面分别 阐述 增强语言表达能 力的几个 机制 语 言塞 于苟阶逻弃 尽管现有各式各样的逻辉可供选 择 简单命题逻挥 、 谓词 逻辑 、 模态时态逻辑及集合理论和 高阶逻挥等 , 然 而 对通用规约语言 , 仅有高阶逻样和 集合理 论能够提供需要的表达能 力 集合理论天生是无 类型 的 , 而 类 型机制 是发现规约 中错误的重要手段 , 高阶逻样既支持灵 活 的类 型 系统 , 又允许高效的类型检查 , 有助 于构建简明 、 清晰的规约 , 因此 选择 了高阶逻辑 羊 富时美型 系扰 强 类型 机制对 维持 高阶逻辉的一致 性是必要的 , 并且类型检查也是发现规约 中许多铃误 、 保证 规约语 义正确 的 简单有效方法 语法正确 性检查 由 系统的解 释器完成 拥 有丰富的类 型 系统 , 诸如 数值类型 、 枚举类型及元组类型 、 记录类 型 、 函数类型 和这些构造类型 的依赖 形 式 谓词 子 类型 是其 中最具特 色的一种类型 , 它允 许在 已有类型 上 附加 限制条件 例 如 已有类型 , 满足限制 条件 是谓 词 的 的子类 型 可定义 为 石 作 者 简介 序 宇 , 男 , 研究生 , 主研方 向为 井发面 向对 象语言及 形 式化方法 收稿 日期 一 一 

使用谓词 子类 型可 以 清晰地表达 出 函数的定义域和值 域 , 进 而 构造 出 简明 准确 的规约 多数传 统逻辑使用 全 函数 , 而 在规约 过程 中经常要用 到 部分 函数 , 如除法运算在除数为零时是无定义的 因此在近 来的逻挥 中 , 如 使 用 的逻挥 , 允许使用 部分 函数 但 部分 函数的存在使得相应 的支撑演绎推理 系统即定理证明 器 十 分复杂 , 其推理 效率也 大大降低 为解决这一 矛盾 , 扩 充 了类型 系统 , 引入 了谓词 子类型 , 从而 在仅有全 函数 的 逻辑框 架 内提供部分 函数的功 能 例如通常意义 下 的部分 函 数 除 法 运 算在 引入 谓 词 子 类 型 伙 后 , 除 法 运 算可 定 义 为 如 下 全 函 数 砷 , 刃丈 持夏刀 时撰淤 化设施 理论是 语言 的基本模块 设施 , 一个 规约 由且仅 由一组理论构成 理论 的基本 结 构 知下 理论名 理论参数表 类 型说明 变 童说明 常童说明 函数定 义 递 归函数定 义 公式说明 注 义务部分不是理论的 书面 组成部分 , 它是在类型检查 、 开 假设部分 会理部分 义务部分 定理部分 发证 明 的过程 中由 系统 自动生成的 一个理论可 以 带参数 , 例 如 一个 队列理论可 以 把最大 队列 长度作为参数 , 一个有序二叉树理论 中 , 树的每个结 点 的类型 和排序关 系也可 以 以 参数形 式存在 这样 , 一个理论 成为一块模板 , 在应 用理论时可以根据实际 需要对参数赋 予 具体的值 , 从而得到相应 的理论实例 由此可见 , 带参数 的 理论与类属类型是扭其相似的 , 因此也具有其最大的优点 书写理论时拥有更大的灵活性 , 所得到的理论具有更大的可 复用性 但为 了准确 地表达规 约 , 在许多场合有必要对理论 参数加 以 限制 , 提供 了假设部分来表达这种要求 , 例 如 有序二叉树理论 中的排序 关 系参数可以 被限定为 全序 关 系 例子 下 面 以 最为 典型 的堆找为 例 , 来具体 阐释 规约语言的上述特点 砷 ‘ , 扮 ‘ ‘ , 一 一 一 一 , , , , , 如上所示 , 堆栈被定义为一个理论 , 它构成 了对堆找的 一个完整的规约 为 了使定义的堆找具有一般性 、 易于被 复 用 , 这里并没有对堆找的元素的类 型作具体 限制 , 因此上 述 理论带有类型 参数 , 这样元素为整数的堆找 、 为 实数 的 堆 类型 的常量 找甚至为 队列 的堆找等等 , 均可 以 通过对上 面 同一个理论加 以 实例化得到 接着定义 了 类型 的 变 量 及 是一个谓词 子类 是 语 言 中保 留 型 , 它 相 当 于 扛 字 , 它仅指 明所 定义的是类型 , 但没有对该类型 的性质作任 何规定 , 这也体现 出 语 言 的类 型 系统是十 分丰 富的 类 型 , 、 叩和 是堆找上 的 种 最基本的操作 , 因为 的 规约语言是基于 高阶逻辑 的 , 因此可 以 用 函数来定义 , 并通 过 条公理对这 种操作 的基本性质作 出 约 束 最后 的定 理 叩加 是为 了验证 上述规 约 的正确 性 而提 出的 , 因为根 据堆栈的先进后 出原 则 , 如果上 面 的理论定 义是正确 的 , 这 条定理显然应该 可以 证明 为真 的 定理 证 明 器 的 定理证 明 器 采取 目 标制 导 的 工作方 式 , 一个证 明 的构造从待证定理开始 , 递进地应 用 证明 器提供的命令进 行推理 , 不 断生成新 的子 目标 , 如此反复直至所有子 目标均 显 然为真 这与 的 工作 方 式是十 分类似的 , 证明过程 便是构造一裸倒 笠的证明树 , 根是待证定理 , 每个结 点用 逻 … 表示 , 因为 它 清 抖构 件 晰地封装 了一 个证 明 分 支 的 所有相 关信 息 下 面 分别论述 , 人 , 凡 卜 , , 定理证 明器的 几个特 色 莎犬 定活时价价类 定理证 明器 的命令可分为基 本命令 、 自定义规则 和证 明 策略 类 基本命令相应 于核 心 逻样的推理规则 , 用 户是无法 更改的 , 但 的基本命令要 比 高阶逻辑本身提供的推理规则 的功 能更加 强 大 , 从 而可 更 方便地构造证明 , 也使获得的证明 更加健壮 , 使证明过程可 以 被 高效地重新运行 并且基本命令是十分灵活 的 , 它可 以 以 多种 方 式应 用 于 不 同环境 , 可以 带参数 以 修改其行为 自定 义规 则 和证 明 策略 用 于把频繁使用 的证 明模式抽 象、 表达 出来 如果说基本命令类似 于 一般程序设计语言 中 的基本语 句 , 自定义规则和证 明策略则 相 当于过程或 函数 , 每条 自定义规则 或证 明策略是应 用 系统提供 的一 个简单语 言 把多条基本命令组织起来构成 的 , 更加 强 大 的版本还可 以 包 括决策过程 自定义规则 和证 明策略的 区别在于二者对结 果 的表达不 同 , 自定义规则 直接把一个 目标化 为零个或 多个子 目标 , 而证明策略则 生成一裸树 , 树根是 目标 , 树叶是等待 用 户进一步证明 的子 目标 , 中继结 点是 由 系统生成并 自动分 解的 中间 目标 相对于基本命令 , 自定义规则 、 证 明策略的粒度更大 、 功 能更强 , 也使证明 更易于构造 、 用 户使用 更方便 更重要 的是它们 提供 了扩展 命令集的手段 , 因此针对一个特定 领域 , 用 户可定 义合 适的证明策略 、 自定义规则 , 从 而使该 领域 内问题的求解变得 简单 、 高效 高戎时决衷过表 引入决策过程是卫 定理证明器 的 又一特 色 , 它提 高了证明 器的 自动化水准 即使是琦民简单 、 显 然 的事实 , 要构造其形 式化证明也是相 当 困难的 , 而典型 的用 户根本就不 关 心 这些显然成立 的 细 节 , 因此 , 决 策过程 被设计 为 帮助用 户 自动证 明这些子 目标 使用 决策过程处理 相 等和线性 不 等是最具 重要 意 义 、 贯 穿整个 系统 的 部 分 这些 决 策过程应 用 一致 闭 包处理相等推理 , 在 自然数 、 实数域上执行线 性算术推理 , 如处理 形 式 的 表达式 为使决 策过程更灵活 , 在上述基本功 能之上还作 了 一 一 

简单的扩展 , 使其可 以 处理涉及非线性成分的表达式 , 如 一 一 使 用 决 策过程可 以 简化 表 达 式 、 数据类型表达式 、 函数定 义和条件 重写规则 的条件 , 从 而使用 户仅需在关健点上对证明过程 实施控制 , 而 不 必 陷入 琐屑 的证明 细节之中 , 并使得证明 的表达更加 简捷 、 紧凑 夕畜度丈互 与 夕动化 时定理证 穷 器 当前存在的 定理证 明 器有两个极端 , 一类是每一 小步证明均由用 户控制 的低级 的证明检查 器 , 例 如 , 这一类 证 明 器相 当于 简单地 把 纸 面上 的证 明掇到 了机器上 , 机器本身并没有提供多少推理 能 力来辅助 用 户工作 另 一类是完全 自动化 的定理证 明 器 , , 用 户将 定理 交给机 器 , 在 没有 用 户 的任何 干 预 如 下 , 完全依靠机 器 自身的推理 能 力给 出证明 结 果 概略 地 想 , 似乎完全 自动化 的证 明器是最理想的 , 然 而 不容忽视其 致命的缺 陷 它 的应 用 范 围很 窄 , 只 能够证 明一些 简单的 定 理 , 即与证 明 器相应 的规约 语言 的表 达 能力 十 分有 限 对 支持的一般适用 的规约语 言 , 完全 自动化的证 明 器或 者 根本无 法证明稍 复杂 的定理 , 或者 即便可 以 , 其证明也相 当 复杂 , 所耗时 间之长会使证 明本身失去意 义 因此 的 定 理证明 器介于上述两 个极端之 间 , 高层 的证 明过程 由用 户 直 接控制 , 而 底层 的证 明 由机 器 自动 处 理 人与机 器各有 所 长 , 人的 智能 比机 器 高 , 而 机器搜 于 琐屑 的 重 复性 工作 , 的证明 器正是吸纳 了二者的优点 另一方 面 , 完全 自动 化 的证明 器只 给 出证 明结 果一 一定理可证 、 不可证 , 如可证 为真还是为假 , 而 不 关 心证明本身 , 但 的应用 目标 决 定 了证 明过程要 比证 明 结 果 更为重要 , 清晰 、 易读 的证 明 是 孜孜以 求的 正如软件开发有生命周期一样 , 证 明 的构造 同样也存在 如 下 周期 证明 的开发 、 调试 、 展示 、 维护 由上 面 的讨论 的定理证 明 器在证明 开发周期的各个阶段辅 助 高 可见 , 效地构造可读性 良好 的证 明 , 以 方便用 于与其他人交流及将 来的进一步验证 就证 明开发阶段 而 言 , 证明器提供一 组强 大的命令进行命题推理 、 算术推理等 , 基本命今又可 以 组合构 成证明策略和 自定义规则 为使证明 易于调试 , 证明 器 允许取 消 已做 的证 明 步骤 , 还可 以 在证明过粗 中修改规 约 在 的辅助 下 , 证明 器可 以 较清晰 的形 式将证 明展示给用 户 , 但证明 的可读性仍很差 为支持 证 明 的维护 , 证 明 器允许证明或部分证 明重新编辉 、 运行 、 结束 语 的应 用 范 围很广 , 可以 对计算机领域中几乎所有对 象进行规 约 与验证 如 它 可应 用 于 软件 一 的 多 数算法 、 硬件 一抽 象流水线 处理器 , 也可对 实时铁路道叉控 制 器 、 混成差错模型 的分布式协议的正确 性作规约与验证 尽管 足辅助 开发 易读 的规约 、 辅助 定理证明的有效 工具 , 仍有许多方面 有待进一 步完善 如通过引入结构子类 型 、 归纳 定义 、 定理 间 的精化 映射等 , 可进一步增强规约语 言 的表达能 力 可定义更多的 高级的证明策略 , 使系统的用 户界面 更友好 , 证明 器 的效率更高 还可从 已往 的证明 中提 取 出健壮 、 易复用 的证明框架 , 以 方便后 续证明 的构造‘ , , 参考文献 一 , , , 一 , , , , , , , 认 一 , 丫甘 , , , , 一 上接 第 页 故 降树一从顶 到底 下 表示 最终影响 到损 伤 原 因整个 工 程 项 目 的各层损 伤 树 的 图 抢修方 法 对每一损伤 模式 的可 行 的抢修方 法优先 级 , 按详细 的操作过程与 所需 资源 , 以 及完成 时 限进行排序 列表 。 结论 成功 实施 项 目 的 两 个 最 重要 的方 向足有效的数据 管理 和完善的产品最终影响 , 损伤模式 、 损伤 原 因的分析 , 包括 要求的数据库以 及不 断建造并完善知识库的接 口 参考文献 而 , , 即 , , , 一 , 恤 · 一 甘茂治 论战场损 伤评枯与修复分析 方 法 军械工程 学院 学报 , , 李建平 , 石 全 , 甘茂治 武器装备战场损 伤 评枯 与修复 军械工程 学 院 , 一 图 修改工作跟踪 修 改工作 对 用 于 这些 具有最 高风险优 先 码 的损伤原 因的修改工作进行列表显 示 进行这些修改工作 确保对 的投资获得最大的改进 凡 。 跟踪 提供报告来跟踪修 改工作的 实施 , 包括反债者预 定 日期和完成百分 比 情况 如 图 修改工作跟 殊 所示 一 一