谓词逻辑在程序正确性证明中的应用

年第 期 高等函授学报 自然科学版 计算机知识 谓词逻辑在程序正确性证明中的应用 黄 万 徽 华 中师范大学计算机科学系 现代计算机 中的程 序规模越来越大 , 复 一个精确描述 。 这个精确的描述 由初始断言 杂程度越来越 高 , 如何保证程序 的正确性也 及结束断言刻划 。 其 中初始断言刻划 了提供 就越来越重要 。 一般认为程序的正确性可通 此程序的初始条件 , 即在程序执行前 , 一些程 过程序调试而获得保证 , 其实不 然 。 调试可 序变元应满足的特性与关系 。 如果不提供特 以发现程序的错误 , 但不能保证程序正确 , 因 殊的初始条件 , 则此断 言为永 真 , 记 为 为在调试时只能选取有限次初值进行有限次 结束断言刻划了要求程序所完成 的功能 。 初 的试验 , 而无 法保证程序动态执行 时所有可 始断言与结束断言一起刻划了对整个程序的 能出现情况的正确性 。 正确性的要求 。 如果一个程序开始时满足初 为 了 解 决 此 类 问 题 快递公司问题件快递公司问题件货款处理关于圆的周长面积重点题型关于解方程组的题及答案关于南海问题 , 年 始断言的要求 , 执行结束后满足结束 断言的 在论文 要求 , 则我们称此程序是正 确 的 。 否则 则称 中首先提 出用数学方法去解决 。 的方 为不正确的 。 法是归纳断言法 , 其基本要点是将编制程序 但有的时候 , 一个程序很长 , 为证明其正 的要求用断言的形式 表 关于同志近三年现实表现材料材料类招标技术评分表图表与交易pdf视力表打印pdf用图表说话 pdf 示 。 所谓断言实际上 确仅用一个初始断言和结束断言是很不方便 就是谓词 。 通常在程序开始时设置一个初始 的 。 因此有必要将整个程序分成若干个程序 断言 —一些初始条 件 , 在程序结束设 置结 段 , 而在每个程序段 的前 、 后 各设 置断 言 称 束断言 —执行到某一段程序时的要求 。 如 为该程序的初始断言与结束断言 , 往往前一 果程序由初始 断言 开 始执行后 , 每到一 个断 个程序段的结束断言可 以是后一个程序段的 言处均能被满足 , 且一直到结束断言为止 , 这 初始断言 。 这样一 来 , 一个程序除 了设 置初 时就说此程序是正确的 。 始断言与结束断言外 , 在程序 中的若干个地 断言及其在程序正确性中的作用 方还可 以设置一些 中间断言 。 两个 中间断言 任何程序都有变元 。 变元在程序执行的 间的部分程序构成 了一个程序段 。 关于程序 不 同阶段 中都应满足一定的特性和关系 。 因 段的正确性可 以这样描述 当程序段执行前 而可 以用谓词将其特性 与关系刻划 出来 , 而 满足它的初始 断言 , 执行完毕后满足其结束 这种谓词就叫断言或 叫程序断言 。 如 断言 , 则我们称此程序段是正确的 。 ,’十 ’’ 设 人 , 人 是断言 , 是一程序段 , 则符号 “ ” 人 人 “ ’’ 表示程序 在执行前满足 氏 , 而执行后满足 ,’为非负整数 ” 人。 故我们说 , 一个 程 序 对 于初 始 断言 等均为断言 。 和结束断言 是正确的 , 当且仅 当 。 为了证 明一程序的正确性 , 首先 , 必须对 当 是 由大量程序语句所组成时 , 符号 该程序所完成的功能以及提供的初始条件作 入 人可用 收稿 日期 一 一 , 年第 期 高等函授学报 自然科学版 人 人 表示更为恰 当 。 例 程序段 是正确的 , 它等价于 , 例 十 人 是正确的 , 它等价于 , 程序正确性证明的推理 规则 编码规则下载淘宝规则下载天猫规则下载麻将竞赛规则pdf麻将竞赛规则pdf 为了证 明程 序正 确性 , 首先需要 刻划程 序语言中的每个可执行语言对程序变元的影 响 。 其次 , 考虑如何将这些影 响组合起来使 它成为整个程序对程序变元的影 响 。 我们用 推理规则去刻划这些现象 。 这种推理规则仅 在程序语言 中是正确 的 , 而并不象命题逻辑 的推理规则那样 逻辑永 真 , 对任何领域都是 正确的 。 这种 推理规则共有 条 , 其基本形 式为 卜 或 , 卜 也可 以表示为 粤 一 ’ 平一巨口 巨习, , , 一 。 一结束 结束 图 平 一 ‘ ‘ 巨习 山 ’ ‘ “ ‘ ’ ‘ 一 ’ ‘ 一 ’ 结束 图 如果图 是正确的 , 则 图 是正确的 。 也可 以将合成规则表示如下 如果 戊 以及 人 昆 凡 都正确 , 则 民 凡 凡 吼 , , 下哥 二兴 一 兀一 议 找 正确 。 例 如果程序 现将各条分别说 明如下 合成规则 将一个程序分成若干个程序段 , 只要证 明各段是正确 的 , 则 由这些程序段组合而成 的程序是正确 的 。 设有程序段 乳 和 昆 , 而 , 昆 表示 由程 序段组合的程序 , 它先执行 夙 再执行 凡 , 则 戊 此时有 , 昆 这个推理规则就叫合成规则 。 合成规则可用 信息流程图形式表示如下 是正确的 且程序 凡 凡 也是正确的 , 则我们由合成规则可知 凡 也是正确的 。 合成规则是一个很有用 的规则 , 它告诉 年第 期 高等函授学报 自然科学版 我们如果要证 明 的正 确性 , 那 么 , 只 要将程序部分分 成 若 干段 昆 , 昆 , ⋯ , , 然 后分 别 设 计 出 一 些 中 间 断 言 , , ⋯ , 一 , 则 只要 证 明 , , ⋯ , 一 的 正确性 , 再 反 复应 用合成规则 即可推得 的正确性 。 推论规则 设 为正确 , 则断言 为另一个较 强 的断言 代替后 , 仍为真 , 而断言 为另一个较弱 的断 言 ’代替后 ’仍为 真 。 上述思想用下面推论规则形式表示 设断言 , , , ’以及程序 , 则有 这个规则刻划 了控制语句 “ ’’ , 表示 只有 当条件 成立时 , 才去执行 设 , 为 断言 , 吕为程 序段 , 为 条 件 , 则有 八 这叫做 ⋯ 规则 , 其 中 一 是一个命题 , 不管程序如何 , 它必须为真 。 这 个规则可用信息流程图的形式表示如下 如果下 图是正确 的 , 并且我们还 能证 明 为真 。 甲甲一四一’ 以及 , ’ 八 这个推理规则就叫推论规则 。 例 设有程序段 人 二 是正确的 , 同时有 二 是正确 的 。 那么 由推论规则可得出 凡 是正确的 。 程序语言中的一些控制语句如果用推理 规则形式表示 , 常见的三种基本形式是 条件 条件 以及 条件 这三个语句 中 , 条件也 是一个关 于 程 序 变元的断 言 , 但 它不 是 程 序 断 言 , 一 般用 来表示 , , 和 几 可 以是单一 的语句 , 也可 以包括 ⋯ 对 中的语句序列 。 ⋯ 规则 则下 图所示 的程序也是正确的 。 开开始始 结结束束 也可 以将 二 规则表示如下 如果 人 是正确 , 且 , 一 为真 , 则 戊 是正确的 。 例 为了证明 年第 期 高等函授学报 自然科学版 的正确性 , 由 二 规则 只需证明 ‘ 的正确性 , 以及证明命题 , 为真 。 首先 , 我们证明 八 的正 确性 。 可 以看 到 被指派为 , 而 的 值不变 , 所 以有 ’ ‘ 八 而 ’ 一凡 是真的 , 因此 由推论规则可得 ’ 妻 的正确性 。 其次 , 我们有 一 而又有 由 的定义 又有 妻 由 一 故有 ‘ 由 一 因此证明了 ⋯ ⋯ 规则 这个规则 刻划 了控制语 句 凡 , 它表示 当条件 成立时执行 , 否则 执行 昆 。 设 和 为断言 , 为程序段 , 为条 件 , 则有 〕 几 这个 推 理 规 则 叫 二 ⋯ 规 则 。 它可 以用信息流程图的形式表示如下 如果 图 正确的 , 则图 是正确的 。 甲 一 甲 二 巨口 巨到‘ 一 结束 结束 图 甲 ’ 一 ‘ 卿结束 图 也可 以将 二 一 的规则表示如下 如果 凡 是正确的 , 且 ‘ 凡 人 是正确的 , 则 昆 人 是正确的 。 例 证明 一 戊 一 八 是正确的 , 只要证明下 面的两者的正确性 ‘ 一 ’ 一 》 和 飞 一 年第 期 高等函授学报 自然科学版 迭代规则 这个规 则 刻 划 了 控 制 语 句 , 它表示 只有 当条件 不成立 时程序 才执行 下条语句 , 否则程序执行 , 并且每次执行 后重新判断条件 , 直到条件不成立为止 。 刻划 语 句 的 推 理 规 则 叫 迭 代 规 划 。 在迭作规则 中需要有一 个 断言 , 在该语 句 执行前 为真 , 执行后仍 为真 。 这个断言 叫循环不变关系 , 一般是 比较难于设置的 。 设 为循环不变关系 , 为条件 , 为程 序段 , 则有 这就叫迭代规则 , 它可用信息流程 图的形式 表示如下 八 八门 粤月一 乡面囱 ⋯⋯ 假 结束 图 图 如果图 是正确的 , 则图 是正确的 。 也可表为如下形式 如果 凡 是正确的 , 则 八 〕 是正确的 。 例 求 , 其中 。 可 以反复用加法 以实现乘法 。 让 的值 一开始为 , 然后每次 于 处加一 个 , 一 共 加 次 , 最后结束 。 下面给出这个过程 · , 》 》 戊 址 氏 这个过程 已用断言作 了注释 , 是初始 断言 , 与 是结束断言 。 现在证 明上述程序的 正确性 。 人 是 确的 , 亦即 是正确的 , 因 为 赋值 语 句 置 为 不 影 响 的值 。 人 凡 是正确的 , 亦 即 妻 正确性 的 , 理 由同上 。 , 凡 是正确 的 , 可用合 成规则及 和 得到 。 , 人 是正确 的 , 因为 由 初等 算术 成 性 质 容 易 推 得 凡 人 是 正 确 的 , 再用推论规则即可得 。 人 毛 人 是 正确的 , 因而可看 出 人 八 凡 是正确 的 , 所 以 只需证明 凡 用 中间断言 凡 , 先证明 人 是正确的 , 这是 因为 值为语句 十 所 改变 , 设未改变之前的 值为 ’ , 则此时 凡 年第 期 高等 函授学报 自然科学版 是 ‘ 八 当执行赋值语 句后 , 的值 为 ’ 十 , 此 时 由 ‘ 与 ’ 可得 , 由此得 出 凡 戊 类似可得 人 十 札 再 由合成规则得 》 是正确 的 。 用迭代公式 即 可得 。 岛 是 正 确 的 , 故 人 八 一人 是正确的 , 再 由 用推论规则即可得 。 由 , 用合成规则可得整个程序是 正确的 。 从这个例子可看 出如何证明程序正 确性的全过程 。 它有下列步骤 ①设置程序的初始断言和结束断言 。 ②将程序分成若 干段 , 每段 有初始和结 束断言 , 而往往上一段 的结束断言是下 一段 的初始断言 。 ③证明每一程序段对于它的初始和结束 断言是正确的 。 ④得出整个程序对它的初始和结束断言 的正确性 。 程序正确性证明中的公理 除推理规则外 , 在程序正 确性证 明中还 需要一些公理 , 这些公理仅在验证程序正确 性时是永真 的 。 它们一 共有两条 , 一 条 叫赋 值公理 , 另一条 叫赋值预备公理 , 都描述 了执 行一个赋值语句的结果 。 设一个程序有变元 , , ⋯ , 。 , 则赋值语句有如下形式 。 , 交 , ⋯ , 其中 。 , , ⋯ , 是 一 含 有 变 元 , , ⋯ , 。 的表 达 式 。 如有 程序 断 言 、 , , ⋯ , , 再执行赋值语句 叫前先结构形式 , 则在赋值语句后面的断言成立 日 , , ⋯ , 为 一 , 十 , ⋯ , 、 。 , 为 , ⋯ , ,一 , , 、 , ⋯ , 它表 明存在某些 的值使断言 , 交 , ⋯ , 。一 , , , ⋯ , 为真 , 而此时如用这个 值代人 。 中的 。, 并 和其它变元 、 共 的当前值一起 , 其结果将 是 的 当前值 。 不 仅 如 此 , 而 且 这 是 在 , , ⋯ , 成立 的情 况 下所 成 立 的最强 的正确断言 。 它用如下的赋值公理刻划 , 勺 , ⋯ , 。 , 交 , ⋯ , 旧 , 为 , ⋯ , 为 一 , , , ⋯ , 。 , , ⋯ , 一 , , , ⋯ , 也可 以是这样 即断言 , , ⋯ , 在赋 值语句 。 , , ⋯ , 执行后 叫后 向结 构形式 , 此时下面的断言必成立 。 , , ⋯ , ‘一 , 。 , , , ⋯ , 为 , ⋯ , , 。, , ⋯ , 这是保证执行赋值语句后断言成立的最弱陈 述 , 它可用下述 的赋值预备公理刻划 , , , ⋯ , 一 , 。 , , ⋯ , , ⋯ , , 、 , ⋯ , 。 , , 为 , ⋯ , , 交 , ⋯ , 一般来说两个公理 中只要一个就够 了 。 例 设有程序段 戊 如果 是 则对 凡 的最强断言是 戊 日 ’ ’ ’ 容易证明这个语句包含 ’ 二 如果用后 向结构 , 假定断言 人 是 戊 二 则 是 人 用 十 替换 而得到 , 给出 ’ 从上面可 以看 出如何用谓词逻辑方法去证明 程序正确性问题 。 当然这种方法要具有实用 价值 , 尚待进一步改进 。