开放逻辑与软件测试形式化技术

1、开放逻辑与软件测试形式化技术开放逻辑与软件测试形式化技术 张伟，张伟， 东北大学信息科学与工程学院东北大学信息科学与工程学院 主要内容主要内容 背景知识背景知识 开放逻辑开放逻辑 软件测试定理软件测试定理 一、一、背景知识背景知识 1、人工智能人工智能 什么是人工智能（AI的定义）：让计算机去完成需要“智能”才能完成的任务。 人工智能的两大学派：符号主义和连接主义： 连接主义认为思维是大量互连的神经元的集体活动所造成的结果； 符号主义则认为人类认知的基本元素是符号,认知过程就是符号表示上的一 种运算。 符号主义取得了辉煌的成果符号主义取得了辉煌的成果 Newell和Simon等人的心理学小组编

2、制出了一个称为逻辑理论机的数学定理 证明程序，证明了Russell和Whitehead的“数学原理”中的部分定理，并发 现了原书中的几个证明错误。后来的GSP能求解许多问题。计算机下棋程序 能够战胜国际象棋大师。最引人注目的是专家系统。 专家系统：一个软件系统，其解决某一领域的问题时，能够达到该领域专家 的水平。 如美国斯坦福大学研制的MYCIN系统，是用于细菌感染疾病和脑膜炎，然 后就如何用抗菌素治疗向内科医生提出医疗方案，它虽然是最早的专家系统， 无论从系统的原理、结构以及性能看都是相当成功的。水平稳定，知识永存。 斯坦福大学人工智能研究中心(SRI)的地质勘探专家咨询系统PROSPECT

3、OR, 可根据岩石标本及其它勘探数据，对可能的矿藏进行探测。曾发现过有开采 价值的锂矿。 以上事实表明，不管是什么领域，只要能够通过某种知识获取的手段，把人 类专家的某个专门领域的知识“转移”到计算机中去，依靠它的推理程序， 计算机就有可能作出接近专家水平的工作。 从理论上看，符号系统实际上是公理系统。何为公理系统？ 2.公理系统 欧氏几何的创始人是公元前三世纪的古希腊 伟大数学家欧几里德。在他以前，古希腊人 已经积累了大量的几何知识，并开始用逻辑 推理的方法去证明一些几何命题的结论。欧 几里德在前人的基础上，天才般地按照逻辑 系统把几何命题整理起来，构建了欧氏几何 系统，建成了一座巍峨的几何

4、大厦，完成了 数学史上的光辉著作几何原本（5+5）： 1、从若干不证自明的公理出发，利用纯逻 辑推理的方法，证明出所有定理的演绎系统 即为公理系统。 2、通过有限把握无限； 3、第一个公理系统； 4、影响人类文明至今(例如,命题公式集的定义)。 3、数理逻辑 公理系统的方法延展到逻辑学的领域，就形成了数理逻辑。 数理逻辑定义：用数学的方法研究逻辑问题。 很多推理并不依赖所论证的具体内容。如： 假如下雨地就会湿。今天下雨了，故今天地湿。 人都有一死。苏格拉底是人，所以苏格拉底也会死。 抽象化后，A B，A B 。 形式化的逻辑认为，可以用巧妙的方法把推理过程纯化， 从而不必思考推理中涉及的内容，

5、并达到数学那样的精确 性。 莱布尼兹（Leibniz）的理想： 把这些思维形式的规则用符号和数学的方式表达出来，并以数学的方式 推进它，导致了数理逻辑这门科学的诞生与发展。 把推理规则变成演算规则，莱布尼兹首先创立“逻辑演算”，并且进一 步设想，可以设法造出能进行这种演算的机器，即所谓逻辑机。莱布尼 兹曾幻想过，一个那样的黄金时代即将来临：两个哲学家发生哲学分歧 时，用不着辩论，只要把笔拿在手里，在计算工具面前坐下来，两个人 面对面笑嘻嘻地说：“让我们来计算一下吧！”谁对谁错，看计算的结 果就知道了。 由此可见，在莱布尼兹看来，“思维”不过是一种复杂的“计算”而已。 什么是“计算”？ 通用计算

6、机存在性定理被证明 计算理论在1937年取得了重大的突破。英国学者图林(A.M.Turing）发 表了论可计算的数及其对判定问题的应用。他严格地用数学方法定 义了什么是“计算”（能左移、右移、读、写的磁带机），即著名的 “图灵机”。还证明了，存在一个图灵机，它能执行任何计算过程， （只要给它所要求计算过程的程序）通用计算机是存在的。这在理 论上排除了巴贝奇的继承者们去构造通用计算机的疑虑，同时也为如何 构造提供了理论指导。（今天计算机界没有Nobel奖，但有Turing奖）。 就计算能力而言，今天的所有计算机与TM等价。 1900年数学大会，Hilbert提出了伟大的设想：建立通用逻辑公理系统

7、， 可以囊括所有数学定理。同时提出23个问题。该设想最终在1931年被 Godel的不完备定理所否定。但是稍小一些的一阶逻辑系统含盖范围已 相当强大。 后来证明，一阶逻辑推理系统（计算能力）等价于Turing机。（TM例） 一阶逻辑中的自然推理系统一阶逻辑中的自然推理系统G： 自然推理系统推导公式的例子自然推理系统推导公式的例子 著名的计算机软件大师 Dijkstra （埃德斯加狄克斯特拉）曾有一段自述, 足以说明数 理逻辑对于计算机科学是何等的重要。 （可见，实现人工智能的逻辑准备相当充分。但是，关键的问题： “什么是智能？”却一直没有突破。我们只有著名的图灵实验。） 二、二、开放逻辑开放逻

8、辑 2、OPEN过程模式 开放逻辑提出开放逻辑提出OPEN过程模式，其基本工作流程如下：过程模式，其基本工作流程如下： 3、版本和版本序列 六、事实反驳与修正演算 1、新猜想和新公理 2、事实反驳与极大缩减、事实反驳与极大缩减 当一个形式理论受到事实反驳时，人们需要对该形式理论进行修正， 而修正后所得到的结果称为极大缩减。 3、R演算演算 如果是一个形式理论，并且 A 可证，那么关于 形式反驳A的极大缩减是与A协调的的极大子集合。本节 讨论如何求解所有的极大缩减。事实上，也可以像自然推 理系统那样，设计出一组符号演算的规则，使得对给定的 和A，可以使用这些规则推导出所有的极大缩减。这就是 R-

9、演算系统。 4、R演算的例子演算的例子 5、R演算的可靠性、完全性演算的可靠性、完全性 Reiter的基于模型的诊断推理理论 程序修正是软件开发过程中一个相当耗费时间的过程。它包括 通过测试和模型检查对程序错误的定位和纠正。近年来，自动 纠错技术（Automatic debugging)已经发展为软件工程领域的一 个研究热点24。 基于模型的诊断技术是一种被广泛关注的程序纠错的人工智能 手段。Reiter在1987年提出了著名的诊断推理理论基础。在他的 诊断推理理论中，先将软件系统表示为逻辑语句集合，而软件 错误诊断问题被表示为对公式集合一致性测试问题。 七、软件测试和程序修正七、软件测试和程

10、序修正 ( program debugging ) 的形式化的形式化 Reiter的基于模型的诊断推理理论 Reiter首先用一阶逻辑表示软件系统和系统的组件。然后给出当 所有组件都运行正常情况下该系统的行为描述。当得到一组该 系统实际运行的观测数据（observation ), 就将其与理论期望的 行为描述数据相比较，如果出现冲突（即，逻辑不一致冲突（即，逻辑不一致 （inconsistent），则称遇到了一个诊断问题（找到一个 BUG）。程序修正就是要寻找出该系统的哪些组件行为不正常， 才导致了这种冲突（和不一致）。 这涉及到逻辑语言、系统模型描述、行为描述和系统错误的形 式定义。 A s

11、ystem to be diagnosed is given by a triple (SD, COMP,OBS) where SD, the system description, is a set of logical sentences; COMP, the system components, is a finite set of constants; and OBS, an observation, is a finite set of logical sentences. There is a special predicate AB(c) which says that comp

12、onent c is abnormal。 Definition A diagnosis for (SD, COMP,OBS) is a minimal set COMP s.t. the following is consistent: SDOBSAB(c) | c AB(c) | c COMP . 于是，程序诊断问题被转化为一个逻辑公式的一致性判定问题。 EXAMPLE 全加器系统的电路全加器系统的电路: 全加器系统的全加器系统的SD语句集语句集: 该全加器的一次该全加器的一次OBS(发现错误发现错误): 通过求取定义中满足一致性要求的通过求取定义中满足一致性要求的找出原因找出原因(BUG)

13、: 纠错纠错: 1 1 1 0 0 0 1 反推反推 出错部件出错部件 判定性问题：判断一个公式集合的一致性是不可计算的。所以 Reiter提出，加上实际应用的限制（如，仅讨论线性电路的等价 性问题）来回避一般的一阶逻辑公式集合的一致性判断问题。 关于如何寻找到所有诊断（ diagnosis），一个直接的办法是 采用生成-测试方法，系统的生成COMP（COMPONENT）的所 有子集，然后测试以下公式的一致性： SDOBS AB(c) | c AB(c) | c COMP . 后来，Reiter又提出了改进效率的方法。 * 测试基本定理 开放逻辑十分适合于解决软件测试与纠错问题： 开放逻辑自然的表达了软件系统版本的变迁； 开放逻辑不需要找出COMP的每个子集合来一一测试其一致性， 而是直接找出导致矛盾（冲突）出现的逻辑前提组件，而且其 寻找过程是通过逻辑演算来完成的； 开放逻辑可以接受新的事实（组件）作为其公理（即，接受新 的组件做为系统的一个部分而重新展开推理）。 R演算可以找出最大一致集合 因而可以发现不一致，并且 修正程序规约 R演算可以找出最大一致集合： 当遇到系统的期望行为与实际测试行为数据冲突的时候，开放 逻辑运用其R演算来寻找回避这个冲突的SD+OBS COMP 最 大一致集合（等于找到了O