基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。

柯西中值定理的证明及其应用探索

为促进高职学生深入理解柯西中值定理的内容及应用,探索了两种证明柯西中值定理的方法,并阐释了三个中值定理之间的关系.介绍了柯西中值定理在等式证明、不等式证明、函数单调性判断及极限计算中的应用,并进一步应用柯西中值定理证明了洛必达法则、积分中值定理及泰勒定理.对柯西中值定理的证明、内涵及其在解题中的应用进行探索,为微分中值定理的学习和应用提供参考.

基于Isabelle/HOL的文件系统形式化设计与验证

对于构建可信操作系统而言,文件系统设计和实现的正确性至关重要,即使是已经得到广泛运用的文件系统仍然有漏洞被检测出来。采用形式化方法对文件系统的设计和实现的正确性进行严格的验证是公认的可行方法。当前文件系统的形式化验证工作大多基于宏内核操作系统,而忽视了微内核操作系统架构下文件系统的验证。为此,提出一种微内核架构下采用内联数据机制的文件系统的形式化设计和验证方法。以高阶逻辑(HOL)和自动机模型为基础,将文件系统中的工作对象和系统资源抽象为系统对象来构建文件系统的工作状态,形式化地描述文件系统的相关系统调用的功能语义,将系统调用提供服务的过程抽象为系统工作状态发生跃迁的过程,并给出文件系统功能正确性和安全属性的断言。以实现的安全可信微内核操作系统(VSOS)中的安全可信文件系统(VSFS)为例,在设计阶段构建VSFS的有限状态机模型,并在Isabelle/HOL中抽象描述VSFS的可移植操作系统接口(POSIX)系统调用,分析和归纳出VSFS文件系统正确性断言,使用定理证明的方式来验证VSFS的正确性。实验结果表明,该方法在Isabella/HOL中完成VSFS有限状态机模型细粒度的形式化验证,满足预期的安全需求规范。

定理证明辅助工具Isabelle剖析与应用

Isabelle是一个通用的定理证明器,应用领域广泛。介绍Isabelle逻辑系统的功能和构成,分析了Isabelle的规格说明语言、验证系统的特点,并给出了用Isabelle逻辑系统来构造Z规格说明的定理证明的方法。

约束求解与定理证明专题前言

随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性.与测试不同,形式化方法可以完全排除某些类型的错误.约束求解和定理证明是形式化方法中的两大关键技术.在约束求解方面,SAT和SMT求解器已经在学术界和工业界得到了广泛应用,比如SAT求解器用于EDA领域的等价性验证,SMT求解器用于程序验证和白盒模糊测试等.交互式定理证明通过人和计算机之间的交互完成证明,能够验证非常复杂的系统和性质,例如编译器和操作系统的正确性验证.约束求解与定理证明专题关注约束求解和定理证明的理论、技术、工具与应用,包括在EDA、符号执行、模型检测、程序分析与验证、系统安全等领域的应用.

多项式插值余项定理的一个自然证明

通过对插值多项式函数性质进行分析,多项式插值余项的基本形式得到诱导,再从该基本形式出发,获得了多项式插值余项定理的新证明.整个证明过程无需借助辅助函数的构造,因而显得较为自然.这种自然证明的方式也可用于Hermite切触型插值多项式余项的证明.

综述中学勾股定理的证明方法

为了使中学生能高效解答勾股定理的题目,教师可以通过赵爽弦图证明、等面积、欧几里得证明和反证法等证明方法,使中学生更好地理解和掌握勾股定理的概念与本质。在日常的教学中,教师不断帮助学生理解勾股定理的证明,可以使学生更快和更熟练地运用勾股定理解决实际问题。

用搭积木的方法证明费马大定理没有正整数解

本文用搭积木的方法证明an+bn=cn,当n≧3时没有正整数解。

美国和英国早期教科书中的圆幂定理

选取1829—1948年间出版的80种美国和英国早期的几何教科书,探究其中关于圆幂定理的内容.研究发现教科书中推导相交弦定理、割线定理和切割线定理的各种方法,以及圆幂定理在数学内部和数学外部的应用,期望相关观点和素材能为圆幂定理的教学提供有益的参考.

基于Coq的RVWMO加载值公理形式化描述与推论证明

RISC-V内存一致性模型(RVWMO)规定了RISC-V多核系统的访存序约束,是RISC-V软硬件设计者共同遵守的重要规范,旨在为硬件设计提供灵活性的同时保证软件的易开发性。RISC-V指令集规范使用全局访存序、保留程序序以及三条公理(加载值公理、原子公理与进度保证公理)描述RVWMO。通过运用RVWMO的规则,可对多线程程序的访存序合法性进行判定,进而指导芯片设计、验证与软件开发。其中,加载值公理是最为复杂和难以运用的规则之一,是多个典型案例合法性判定的重要基础。然而,规范对于该公理的描述及案例讲解主要基于自然语言,缺乏清晰严格的形式化描述和推理过程,不利于读者理解和运用该公理。本文基于交互式定理辅助证明工具Coq,给出了RVWMO加载值公理的形式化描述以及相关引理、定理和推论的证明,对于理解运用RVWMO加载值公理和判定访存序的合法性具有重要意义。

展方法、品文化,让经典熠熠生辉——以《勾股定理》第一课时教学为例

1“勾股定理”探索的路径分析1.1路径比较《勾股定理》在人教版、苏教版、北师大版教材中均单列为一章,在章头图中或用2002年国际数学家大会会标图——赵爽弦图、或用与“外星人”联系的信号图形直观地揭示出勾股定理本质内涵与文化价值.在上述教材第一课时中基本上以“设置情境、操作测量、思考猜想、归纳证明”等环节呈现出“勾股定理”探索的路径,精彩纷呈.

算法的形式化推导与基于Isabelle的自动化验证

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.

运用定理证明器ACL2验证机器人操作系统ROS节点间通信

作为一种开源的机器人操作系统,ROS在家用或服务性机器人上也得到广泛应用,保证其设计的正确性相当重要.本文通过定理证明的方法对ROS的节点间通信进行形式化建模与属性验证.对通信层的节点间连接建立和消息传递过程进行抽象建模,模型融合网络拓扑、主题匹配和路由机制等部分,定义函数对其进行描述,提取路由函数的存在性、可达性及正确性等3个关键属性,运用定理证明工具ACL2对ROS节点间通信的功能正确性进行自动验证,证明消息从源节点出发并选择有效的传输路径到达目的节点.这种满足属性要求的参数化模型具有一般性和易扩展性,并能保证ROS节点间通信的终止属性和功能正确性,可为ROS通信层设计的正确性验证工作提供一个有效的方法参考.

运用定理证明的形式化方法验证SpaceWire编码电路

我国空间太阳望远镜(SST)项目采用了SpaceWire作为传输总线,目前针对SpaceWire总线的验证主要采用测试和模拟等传统的方法,这类验证方法是不完备的.本文旨在对SST项目中SpaceWire总线的DS编码电路是否如实地实现标准中的规范要求进行验证,运用定理证明的形式化方法,在HOL4工具上对该电路的设计实现与规范要求的一致性进行验证,克服了传统验证方法的局限性.

几何定理可读证明的自动生成

用计算机能生成几何定理的易为人们理解的证明吗？这个几十年来进展很小的难题，自１９９２年以来有了突破性进展．对于一大类欧氏几何命题──构造性几何命题，已有了相当有效的算法．基于此算法所编制的程序，已证明了５００多条非平凡的几何命题．对其中大多数命题，机器自动生成的证明是简明而易于理解的．本文是对这一领域近三年来取得的进展的综述．包括了在非欧几何可读证明方面的最新成果．

一种新的基于扩展规则的定理证明算法

基于扩展规则的定理证明方法是一种与归结方法互补的新的定理证明方法.首先通过对扩展规则的深入研究,给出了扩展规则的一个重要性质,设计并实现了该性质的判定算法.此外,从理论上分析及证明了该判定算法的时间和空间复杂性.基于此,提出了一种新的基于扩展规则的定理证明算法NER,将判定子句集可满足性问题转化为一系列文字集合的包含问题,而非计数问题.实验结果表明,算法NER的执行效率较原有扩展规则算法IER和基于归结的有向归结算法DR有明显提高,有些问题可以提高两个数量级.

机械化定理证明研究综述

随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.

多项式等式型几何定理的可读证明

目前的智能几何软件都使用基于搜索法的定理证明器作为推理引擎,其主要缺点是不能可读地证明涉及到几何量代数运算的几何定理,这极大地限制了智能几何软件的实际应用.对一类结论为几何量多项式等式的几何定理,文中提出了一种能给出可读证明的启发式搜索算法.该算法通过引入多项式的变形操作算子——标准项代换,把证明结论为多项式等式g=0的几何定理转化为寻找从g到0的标准项代换序列的搜索问题.采用Lisp语言实现了该算法,并做了30个结论为几何量等式的几何定理的推理实验.实验结果表明算法具有较高的推理效率.

文件比较算法fcomp在Isabelle/HOL中的验证

基于机器定理证明的形式验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.文件比较算法(file comparison algorithm)是一类成员众多,应用极为广泛,跨越生物信息学、情报检索、网络安全等多个应用领域的基础算法.在交互式定理证明器Isabelle/HOL中对Miller和Myers在1985年提出的基于行的文件比较算法fcomp做了形式化,改正了算法关于边界变量迭代的一个小错误,证明了改正后算法的可终止性和正确性;对算法时间复杂性做了完全形式化的分析,印证了算法的非形式化分析结论,为今后更多文件比较算法的形式验证提供了可供借鉴的经验.

一阶谓词演算定理机器证明的余式方法

本文将一阶谓词演算的定理证明转化为代数簇的计算，从而获得了代数化的Ｈｅｒｂｒａｎｄ过程．又通过一阶多项式间的求余运算，给出了余式方法并证明了它的完备性．同时，我们证明了归结原理是余式方法的一种特例．