精华内容
下载资源
问答
  • 形式化
    千次阅读
    2017-06-20 16:45:37

     形式化方法的主要内容包括:
    (1)系统建模System Modeling:通过构造系统S的模型M来描述系统及其行为模式。
    (2)形式规约Formal Specification:通过定义系统S必须满足的一些属性P,如安全性、活性等来描述系统约束。
    (3)形式验证Formal Verification:证明描述系统S行为 的模型M确实满足系统的形式规约。

     并发系统的计算模型有很多,像迁移系统、自动机、petri网以及基于进程代数的CSP、CCS等。
    (1)迁移系统是一种基于状态迁移的基本计算模型,即通过系统(程序)的状态集合以及对应状态间变迁的迁移(也称操作)集合刻画系统的行为模型。
    (2)自动机是计算机科学中最基本的一类抽象计算模型。其中有穷自动机是自动机理论的基础,它是一种描述有穷状态系统的抽象数学模型,许多并发模型都是在有穷自动机的基础上建立的。
    迁移系统和自动机本质上都是交错并发模型,即系统进程间的并发执行并不是真并发,而是通过各个原子迁移以不确定的顺序交错执行来表示的,其计算行为表现为状态迁移序列。
    (3)Petri网是最早的并发计算模型,它是一种系统的既有数学分析又有图形描述的工具,既可以通过直观的图形刻画系统的结构,又可以引入数学方法对其性质进行分析,特别适合描述系统种进程间的顺序、并发、互斥、冲突及同步等关系。与
    迁移系统、有穷自动机不同,Petri网所描述的并发是真的并发,在Petri网中系统不存在统一的时钟,除因果 关系外没有其他信息可以用来判定两个事件的依赖关系。

     模型检测算法主要是通过遍历状态空间检验属性规约在系统模型中是否成立来实现。在遍历过程中,有两种描述可达状态空间的方法:一种是状态以及状态迁移关系都显式地存储在内存中,并且对属性的验证也是通过显式地遍历状态空间中的所有可达状态来完成的,称为显式模型检测;另一种是采用符号方法隐含地表示可达状态空间,称为隐式模型检测。

    概率模型检测将模型检测与概率分析方法(如马尔科夫链等)相结合,使用该方法不仅可以知道一个系统是否有可能出错,而且能得到错误发生的概率。通过对系统行为的概率分析,可以忽略发生概率非常小的错误,还可以用来评估一个系统发生错误的平均时间 。目前常见的概率模型包括离散时间马尔科夫链、连续时间马尔科夫链。相应的概率性质描述逻辑有概率计算机树逻辑及连续随机逻辑等。PRISM基于概率模型检验的工具,它支持高级建模及多种概率并发模型。

    更多相关内容
  • 形式化方法一般可分为形式化规范说明Formal Specification,和形式化验证Formal Verification。 Formal Formal Specification 形式化规范说明 Formal Verification 形式化验证 Theorem Proving 定理检测/Deductive...

    【1】 概述

    硬件和软件系统在规模和功能上的增长增加了复杂性,也 增加了潜在错误的可能性,这些错误引起了金钱、时间上的损 失,甚至会危及人们的生命。形式方法是用于软件和硬件系统 的规范,开发和验证的特定类型的基于数学的技术,是改善和 确保系统质量的重要方法。形式化方法在软件和硬件领域中 的应用进展比较显著,引起了各个领域的注意[1]。形式化验证 方法是形式化方法的一个重要的研究内容,本文主要对形式化 验证方法进行探讨。

    形式化方法一般可分为形式化规范说明Formal Specification,和形式化验证Formal Verification。

    Formal

    • Formal Specification 形式化规范说明
    • Formal Verification 形式化验证
      • Theorem Proving 定理检测(证明)/Deductive Verification 演绎检测
      • Model Checking 模型检测
      • Automated Test Case Generation 自动测试用例生成

    在这里插入图片描述

    【2】基本概念

    【2.1】形式化规范说明

    硬件和软件系统在规模和功能上的增长增加了复杂性,也 增加了潜在错误的可能性,这些错误引起了金钱、时间上的损 失,甚至会危及人们的生命。形式方法是用于软件和硬件系统 的规范,开发和验证的特定类型的基于数学的技术,是改善和 确保系统质量的重要方法。形式化方法在软件和硬件领域中 的应用进展比较显著,引起了各个领域的注意[1]。形式化验证 方法是形式化方法的一个重要的研究内容,本文主要对形式化 验证方法进行探讨。

    【2.2】形式化验证

    【2.2.1】定理证明

    定理证明:先对系统及其性质进行抽取,表示成基于某种 逻辑的命题、谓词、定理,在验证者的引导下,不断地对公理、以 证明的定理施加推理规则,产生新的定理,直到推导出表达系 统性质的公式,从而证明设计的系统满足该性质。现在定理证 明器越来越多的应用在验证硬件和软件设计的安全临界性质 的验证[3]。 定理证明高度抽象,具有强大的逻辑表达能力,可以验证 几乎所有的系统行为特性,可以处理无限的状态空间。定理证 明器可以分为三种:自动定理证明器、交互式定理证明器及证 明检验器。现在大多数定理证明器是交互式的,需要人的引 导,对验证者的要求有良好的数学经验。 主要的定理证明工具有:STeP(Stanford)、TLV、AL2(UTAus⁃ tin/CLI)、Coq、HOL(Cambridge)、Isabelle(Cambridge)、Larch、Nu⁃ prl、PVS(SRI)等。

    【2.2.2】模型检测

    模型检测是一种通过对目标系统建立一个有限的模型,并在模型发生改变时,检测希望满足的性质,例如安全性和活性在该模型中是否成立、稳定的技术。

    目前有两种主要模型检测技术:

    • 一种是时态模型检测,这 种方法中规范说明用时态逻辑公式表示,系统用有限状态转换模型表示,用模型检测器检测模型是否满足规范说明公式。
    • 另外一种是等价性检测,这种方法中规范说明用一个自动机表示,系统用一个自动机表示,然后证明两个模型是否一致。

    自动化程度较高是模型检测的优点,并且当系统不满足给 定的性质时,可以给出反例,使设计人员方便找出设计错误。 模型检测应用于硬件和协议的验证,现在在对软件设计的验证 已成为研究的热点。状态空间爆炸问题是其主要的缺点。

    主要的模型检测工具有:

    • COSPAN/FORMALCHECK(Bell)、
    • MURPHY(Stanford)、SPIN(Bell)、
    • SMV(CMU)、
    • VIS(Berkeley)等。

    目前形式化验证方法成功应用于商业、航空业、通信业和 芯片制造业,INTEL,ARM和NIVIDA等大公司已经把形式化方法应用到芯片的制造和验证[5]。

    从本质上讲,模型检测技术就是穷尽对状态空间的搜索,并通过模型的有限性来保证该搜索过程一定会终止。最初的模型检测应用在硬件和协议验证领域,十分成功,后来在软件系统的验证上也得到了广泛应用。

    Reference:

    [形式化验证方法浅析] 陈波1,李夫明2 (1.山东理工大 学 计算机科学与技术学院,山东 淄博255000; 2.山东理工大学 数学与统计学院,山东 淄博255000)**

    后续待阅读资料

    线性时序逻辑 https://www.docin.com/p-506137477.html
    模型检测 https://wenku.baidu.com/view/800eade45a8102d277a22f3a.html?fr=search
    model checking overview and buchi automata and LTL https://www.docin.com/p-1003260979.html

    展开全文
  • 软件形式化方法概述

    千次阅读 2018-11-10 10:09:55
    软件形式化方法概述

    分享一下我老师大神的人工智能教程!零基础,通俗易懂!http://blog.csdn.net/jiangjunshow

    也欢迎大家转载本篇文章。分享知识,造福人民,实现我们中华民族伟大复兴!

                   

           友情提示:本文理论性和专业性较强,如果木有接触过该领域,读起来可能会有一点点吃力,吐舌头!本文是Sunny结合多份资料综合整理而成,有点凌乱,见谅!

     

           软件形式化方法(Formal Method)在软件开发中一直都受到多方面的争议。持肯定态度的拥护者认为形式化方法会引起软件开发的革命微笑,另一些持否定态度者则怀疑甚至反对将数学引入软件开发过程中难过

           形式化开发方法的一些争议或缺陷主要体现在:

           (1) 形式化方法中所包含的数学理论,限制了大多数程序设计人员的学习和使用;

           (2) 认为采用形式化方法会延误项目开发周期、增加开发费用

           (3) 许多流行的形式化方法对于较小规模的项目是有效的,但却很难应用于一些大型系统

           (4) 形式化方法不能确保开发出完全正确的软件;

           (5) 缺乏对软件生命周期内各个阶段提供全面支持的形式化方法;

           等。

     

          从广义上讲,形式化方法是借助数学的方法来解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述、模型推理和验证的方法。就形式化建模而言,形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定,或证明该表达式具有某种性质。

     

           难过关于形式化方法:悲观者的角度难过

           形式化方法是为数学家准备的

           形式化方法仅供从事形式化研究的人使用

           从事形式化研究的人仅使用形式化方法

           形式化方法的运用将延缓软件开发进度

           形式化方法的运用将提高软件开发成本

           形式化方法仅应用于开发安全要求极高的系统

           形式化方法仅被用于无关紧要的系统,且缺少工具支持

     

           微笑关于形式化方法:乐观者的角度微笑      

           运用形式化方法将开发出完美的软件

           形式化方法可以替换传统的软件工程方法

     

          形式化方法的出发点是数学逻辑方法,其目的是开发可靠的软件产品。从软件开发来讲,形式化方法目前并非软件开发的主流。从软件发展看,早期的软件是用于数值计算,程序语言侧重于函数和算法的描述,后来数据库的应用和数据结构逐渐变得重要。现在的软件更为复杂,因此,对象、组件、接口、通讯、开放等成为非常重要的概念。从软件工程方法来讲,有一套描述这些概念的办法,比如说用图形、表格、逻辑、自然语言等,交叉使用以描述一个系统的各个方面。因此换一个角度来考虑,我们也可以以目前常用的软件开发方法为出发点,研究怎样将这些方法形式化,使软件系统的描述精确化,以减少可能的误解所带来的问题;或以目前常用的软件开发过程为出发点,研究怎样在软件开发过程中增加一些形式化方法的应用,以提高软件的可靠性。

     

           形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式化开发。形式化的描述就是用形式化的语言(具有严格的语法语义定义的语言)做描述。形式化的软件开发,就是用形式化的语言来描述软件需求和特征,并且通过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。这样的验证当然得建立在严格的语法语义的基础之上的。在实际应用中,这是不容易做到的。形式化方法研究的目的就是希望能够提供更好的理论、方法和工具,扩大形式化方法的应用范围和使用价值。

     

           形式化方法的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致、不明确或不完整,有助于增加软件开发人员对系统的理解,因此形式化方法是提高软件系统,特别是Safety-Critical系统的安全性与可靠性的重要手段。最早的形式化方法是逻辑与逻辑推理,它的目标是使推理机械化。从广义上讲,这一目标受到许多挫折,比如说逻辑系统的不完备性(incompleteness)、逻辑系统的不可判定性(undecidability)、自动推理的难处理性(intractability)。但是在一些实际应用上,逻辑方法和自动推理还是起着非常大的作用。

     

           形式化方法在软件开发中能够起到的作用是多方面的。首先是对软件需求的描述,软件需求的描述是软件开发的基础。比如说一般非形式化的描述很可能导致描述的不明确和不一致,如果描述的不明确和不一致将导致设计、编程的错误,将来的修改所要付出的代价就非常大了,如果导致的错误没有被发现,则影响程序的可靠和使用。形式化方法则要求描述的明确性,而描述的不一致性也就相对易于发现。其次是对软件设计的描述。软件设计的描述和软件需求的描述一样重要,形式化方法的优点对于软件需求的描述同样适用于软件设计的描述,另外由于有了软件需求的形式化描述,我们可以检验软件的设计是否满足软件的要求。对于编程来讲,我们可以考虑自动代码生成。对于一些简单的系统,形式化的描述有可能直接转换成可执行程序,这就简化了软件开发过程,节约了资源和减少了出错的可能性。另外,形式化方法可以用于程序的验证,以保证程序的正确性。对于测试来讲,形式化方法可用于测试用例的自动生成,这可以节约许多时间和在一定程度上保证测试用例的覆盖率。

     

     

           形式化方法原则上就是用数学与逻辑的方法描述和验证软件。从描述上讲,一方面是系统或程序的描述,另一方面是性质的描述。这些可以用一种或多种语言来描述。这些语言包括命题逻辑,一阶逻辑,高阶逻辑,代数,状态机,并发状态机,自动机,计算树逻辑,线性时序逻辑,进程代数, π-演算, μ-演算,特殊的程序语言,以及程序语言的子集等。从验证来讲,主要有两类方法,一类是以逻辑推理为基础,另一类则以穷尽搜索为基础。逻辑推理有 natural deduction, sequent calculus, resolution 以及Hoare-logic 等方法,穷尽搜索方法统称为模型检测。这类方法与系统或程序以及系统性质的表示有很大的关系,比如说符号模型检测,其基本原理是用命题逻辑公式表示状态转换关系,用不动点算法计算状态的可达性以及这些状态是否满足某些性质。

     

           形式化方法的应用在电路设计和协议设计上都取得了很大的成绩,但是对于软件来讲还有很多没有解决的问题。软件的描述要比电路和协议复杂,一个软件描述所包含的状态空间通常来讲可以是无限的,因此验证的难度很大。逻辑推理的不足之处在于推理的难度,对于稍微复杂的系统,自动化的推理就难以胜任。人为的推理有很大的缺点,除了费时费力外,比如说一个定理推不出来,并不能说明这个定理不成立,很可能是推理方法和策略应用不当。模型检测的好处在于它有全自动化的检测过程,并且如果一个性质不满足,它能给出这个性质不满足的理由,我们即可据此对我们的系统描述进行改进。模型检测的困难首先是它所能检测的是有限状态模型。这样对于一般软件来讲,需要有一个从任意状态到有限状态的建模过程,并且这样的一个模型的状态空间会面临组合爆炸的问题。

     

           形式验证一般被称为形式化验证方法,是相对于传统的验证(模拟、仿真和测试)而言的。形式化验证方法的主要思路就是使用数学的公式、定理和系统来验证一个系统的正确性等。目前的形式化验证方法可以用于验证硬件系统、软件系统和其他系统,而且形式化验证的技术目前也已经发展到不但可以验证系统的功能正确性(有没有错误),而且可以验证系统的性能指标(功耗、散热、延迟等等)。形式化验证方法主要可以分为三种:定理证明、模型检测和等价性验证。定理证明的基本原理是选定一个数学逻辑体系,并用其中的公式来描述(如软、硬件)系统和系统性质刻画,然后在一定的数学逻辑(如hol逻辑)体系中依据此体系的公理、定理、推导规则和系统描述公式,看看能不能推导出系统的性质刻画公式,如果可以的话验证成功。模型检测的原理比较简单但是非常实用,它将(如软、硬件)系统建模成有限状态系统(一般成为keripke结构),系统的性质刻画用时序逻辑公式表示(CTL,LTL等),而后在此模型上来验证性质刻画的正确性,模型检测于定理证明相比是有很大优势的,他可以全自动地验证,不需要人工干预,而定理证明则在一些关键推导路径中需要数学家控制。还有一种是等价性验证,等价性验证其实是一种半形式话的技术,同前两种验证正确性的技术不同,它验证的是设计的一致性,即不同设计阶段的设计是否功能相同,这种技术中一般采用符号的方法和增量的方法,而且由于这种方法和硬件电路紧密结合,所以电路验证的一些传统方法也大量应用于此中方法中来,比如ATPG技术等。如大家使用的Synopsys的Formality本质上就是一个等价性验证器。形式化验证是非常有用的,只是国内作这一行的人太少。大家可以看看Synopsys和Cadence两家公司,它们都是从形式化验证起家的,然后转到目前流行的将设计和验证统一在一起,即“设计验证”领域。

        

     
      

           软件形式化方法研究内容:
        形式化语言(形式化描述、形式规约):怎样描述软件系统及其行为模式;更好地刻画软件系统的性质,比如说,通讯、分布、开放、移动;各种语言的应用、比较,语言与语言之间的转换;开发相应的软件工具。

        形式化验证(形式验证):怎样验证软件系统符合给定的行为模式;更有效地验证软件系统的性质,比如说,自动化、速度快、内存需求少;各种方法的应用、比较;开发相应的软件工具。

     

        具体来说,软件形式化方法包括以下几个主要研究方向:

        (1) 基础概念:复合、抽象、重用模型、数学理论组合、数据结构及算法。需要对如何复合方法、复合规格、复合模型、复合理论、复合证明等进一步的理解;需要开发出将整体特性分解为易于验证的局部特性的有效方法;实际系统在规格和验证之前都要进行某种程度上的抽象,需要研究出评判抽象层次合理与否的方法;重用不仅可以提高开发效率,而且可以提高软件的可靠性,应当研究可重用模型和理论;许多安全关键反应式系统是数字和模拟混合的,需要连续和离散两个范畴内数学基础支撑的混杂系统理论和技术支撑;大规模、复杂软件中搜索空间是巨大的,需要研究出新的数据结构和算法。

        (2) 形式化方法与面向对象方法的结合:这已经成为软件工程领域的一个研究热点,例如:Statecharts、Petri网、Z语言、VDM等,以及与面向对象方法结合产生的Objectcharts、面向对象Petri网、Object-Z、Z++、VDM++等。这方面的研究体现在两个方面:利用面向对象结构来提高形式符号的表达能力;使用形式化方法来分析面向对象的语义或提高这些标记符号的表达对象概念的能力。形式化方法和其他传统软件开发方法相结合以达到取长补短的目的,也是值得研究的课题。

        (3) 工具开发:具有良好用户界面、易于学习和操作简单的形式化方法支撑工具,对于形式化方法的推广应用是大有裨益的。追求通用的完善的形式化方法及其支撑工具是不现实的,侧重于如下某一个或几个方面准则的特色方法和工具是未来研究的重点。这些准则包括:一旦开始使用之后尽早得到明显的效益;效益随着开发者的了解深入和熟练而增加;单一规格可以在软件开发生命周期的多个阶段取得效益;能和其他通用编程语言或方法交互使用;工具应当像编译器那样易于使用、输出,也易于阅读;概念和工具应当易于入门和学习掌握;软件特性分析有所侧重;支持渐进软件开发,允许部分规格和验证。此外,特定问题域的形式化方法及其工具研究也是非常重要的。


    【作者:刘伟   http://blog.csdn.net/lovelion

               

    给我老师的人工智能教程打call!http://blog.csdn.net/jiangjunshow

    这里写图片描述
    展开全文
  • 操作系统形式化验证实践教程(1) - 证明第一个定理 形式化方法分为三个主要部分:系统建模(System Modeling)、形式规约(Formal Specification)和形式化验证(Formal Verification)。 其中系统建模用形式化的模型来描述...

    操作系统形式化验证实践教程(1) - 证明第一个定理

    形式化方法分为三个主要部分:系统建模(System Modeling)、形式规约(Formal Specification)和形式化验证(Formal Verification)。
    其中系统建模用形式化的模型来描述系统及其行为模式。建模完成后,需要用形式规约来精确描述建模出来的需求。有了规约,如何检验是否符合规约呢?这就需要形式化验证方法。

    形式化验证方法主要分为两类:一类是以穷尽搜索为基础的模型检测,另一类是以逻辑推理为基础的演绎逻辑。相对于前者,后者既可以验证有穷的状态系统,也可以使用归纳法来处理无限状态的问题。

    演绎逻辑在早期发展很快,但是后来在大规模软件验证上成本较高,所以发展一直不快。但是,最近十几年,以seL4为代表的操作系统和CompCert为代表的编译器的正确性证明的完成,给形式化验证带来了重要的突破性进展。
    这也带来了两大流派:seL4所使用的Isabelle/HOL工具和CompCert所使用的Coq工具。
    Isabelle是基于Standard ML语言开发的,支持生成Standard ML, ocaml, Haskell和Scala语言的代码。而Coq是基于ocaml语言的。

    波澜壮阔的操作系统级的验证全景,我们后面会徐徐展开。做为一个落地的教程,我们千里之行始于足下,先从Isabelle/HOL工具的使用开始说起。

    Isabelle/HOL简介

    Isabelle/HOL可以通过下面的网址下载和安装:https://www.cl.cam.ac.uk/research/hvg/Isabelle/installation.html。支持Linux/mac/Windows平台。

    HOL是High Order Logic,即高阶逻辑的缩写。

    废话不多说,Isabelle封装在jEdit中,有完整的集成开发环境。我们安装好了之后直接打开看一眼:

    Isabelle/HOL

    有几点不跟普通编程语言的不同之处:

    • HOL的代码以theory组织在一起
    • theory之下有函数fun,值value, 有公式lemma, theorem等
    • 当我们把光标放到lemma或theorem中时,发现系统可以自动帮我们做一些推理的验证
    • HOL代码中大量使用非ASCII符号,可能给用惯了ASCII字符的程序员们带来一定的不适应,但是可读性绝对比用ASCII表示要上一个层次

    自动证明第一个定理

    同其它编程语言类似,HOL也有自己的数据类型系统。我们先从最简单的布尔类型开始。

    HOL支持bool来表示布尔类型。用True表示真值,False表示假值。
    取反为 ¬ \lnot ¬, 取交为 ∧ \land ,取并为 ∨ \lor

    下面我们写一个求布尔交的函数。
    交函数的输入为两个bool,输出也是一个bool.
    我们用"bool ⇒ bool ⇒ bool"来描述这个函数的类型。
    “⇒”的输入方法是用TeX值:<\Rightarrow>.
    HOL语句要用字符串符号""来括起来,原理我们后面再讲。
    代码逻辑上,除了输入为True和True返回True之外,其它都返回False:

    fun conj2 :: "bool ⇒ bool ⇒ bool" where
    "conj2 True True = True"|
    "conj2 _ _ = False"
    

    下面高光时刻来了,我们来用Isabelle/HOL证明我们学习之旅中的第一个定理False与另一个布尔值取conj2操作,结果一定为False。

    lemma conj_02: "conj2 False m = False"
      apply(induction m)
       apply(auto)
      done
    

    apply(induction m)和apply(auto)的作用是让HOL自动帮我们推断证明。
    把光标放到apply(auto)语句,我们从output窗口看到:

    proof (prove)
    goal (2 subgoals):
     1. conj2 False True = False
     2. conj2 False False = False
    

    如图所示:
    conj02

    趁热打铁,我们再写一个练习下:

    fun not2 :: "bool ⇒ bool" where
    "not2 True = False" |
    "not2 False = True"
    lemma not02 : "not2 x = (¬ x)"
      apply(induction x)
      apply(auto)
      done
    

    lnot

    从有限到无限

    恭喜大家,已经学会证明有限情况下的定理证明了。但是这还不够,我们还要能证明无限的情况。
    下面我们就从有限的布尔类型,前进到自然数类型nat和整数类型int.

    自然数的定义带着浓浓的数学归纳法的味道。这里用到了求后继函数Suc:自然数nat = 0 或 Suc nat。也就是说,自然数定义为0,Suc(0), Suc(Suc(0))…

    有了这个定义,我们可以重新定义一个加法了:

    fun add2 ::"nat ⇒ nat ⇒nat" where 
    "add2 0 n = n" | 
    "add2 (Suc m) n = Suc(add2 m n)"
    

    首先是0和n进行add2等于n,然后是m的后继与n进行add2操作,等于m与n进行add2操作后再求后继。

    这么说有点抽象,我们来看例子。

    第一个例子:add2 0 1,根据定义,这个就等于1。这个容易理解。
    第二个例子:add2 1 2。1是Suc 0,于是这个式子为Suc(add2 0 2),add2 0 2根据第一条定义式结果为2。
    第三个例子:add2 2 3。2是Suc 1,于是式子为Suc(add2 1 3),再递推为Suc(Suc(add2 0 3),结果为5.

    这样,通过这样一种递推关系,我们重新定义了加法。

    那么,这个我们新定义的加法,归纳出来的加法,跟真实的加法是不是一致呢?我们写个定理去进行自动证明:

    lemma add_02: "add2 m n = m+n"
      apply(induction m)
      apply(auto)
      done
    

    下面是证明的结果:

    proof (prove)
    goal (2 subgoals):
     1. add2 0 n = 0 + n
     2. ⋀m. add2 m n = m + n ⟹ add2 (Suc m) n = Suc m + n
    

    根据两个初始条件,有两个子目标需要证明:
    第一个是初始条件,add2 0 n = 0+n。
    第二个是基于后继的递推条件。

    皮亚诺公理

    上面的证明方法叫做归纳原理,也叫做皮亚诺第五公理。
    我们来从头看下这5条公理:

    1. 0是一个自然数
    2. 任何自然数n都有一个自然数Suc(n)作为它的后继
    3. 0不是任何自然数的后继
    4. 后继函数是单一的,即,如果Suc(m)=Suc(n),则m=n.
    5. 令Q为关于自然数的一个性质。如果
    • 0具有性质Q
    • 并且 如果自然数n具有性质Q,则Suc(n)也具有性质Q
    • 那么所有自然数n都有性质Q

    在此基础上,我们可以定义加法和乘法。

    • 加法:对于任何自然数n和m:
      • n + 0 = n
      • 并且 n + Suc(m) = Suc(n + m)
    • 乘法:对任何自然数n和m:
      • n * 0 = 0
      • n * Suc(m) = (n * m) + n

    乘法的定理证明如下:

    fun mul2 ::"nat ⇒ nat ⇒nat" where 
    "mul2 0 n = 0" | 
    "mul2 (Suc m) n = n * m + n"
    
    lemma add_02: "mul2 m n = m * n"
      apply(induction m)
      apply(auto)
      done
    

    求值

    在过程中,难免有些值我们希望看到输出结果,这时可以通过value语句来实现。

    例:

    value "Suc(0)"
    

    输出结果为:

    "1"
      :: "nat"
    

    1为结果的值,nat是类型。

    调用我们自己定义的函数也没有问题:

    value "add2 1 (Suc 4)"
    

    输出结果为:

    "6"
      :: "nat"
    

    恭喜你,我们已经在定理证明的世界里证明了第一个定理。
    后面的路很长,坡也有点陡,我们继续前进。

    展开全文
  • 随着平台级应用的普遍化,智能合约涉及的金额呈指数级别增长,如果其代码存在漏洞,则可能会遭到攻击,造成巨额损失,为防止类似事件发生,提出了运用形式化方法提高智能合约的安全系数的方法。 一、智能合约简介 ...
  • 什么是形式化

    千次阅读 2018-08-10 05:22:32
    形式化方法在古代就运用了,而在现代逻辑中又有了进一步的发展和完善。这种方法特别在数学、计算机科学、人工智能等领域得到广泛运用。它能精确地揭示各种逻辑规律,制定相应...
  • 形式化验证工具——prism(1-安装)

    千次阅读 2022-03-08 10:50:31
    prism是一款免费开源的形式化验证工具。是一个比较容易上手的工具。 其下载连接:PRISM - Download 官方给出使用教程,地址:PRISM - Tutorial 第1部分:使用一个简单的离散时间马尔可夫链(DTMC)示例 - 一种...
  • 形式化语言的重要性

    千次阅读 2019-02-26 23:16:59
    2.半形式化的语言(数学语言),即自然语言加特定的符号。 3.形式化的语言(逻辑语言) 半形式化语言 任何一个数学分支的语言都是在自然语言的基础上附加一些特定的符号,它们与自然语言相比更具形式化。因此,称它...
  • 关于软件形式化验证

    万次阅读 2018-05-29 09:37:01
    形式化验证是用逻辑来验证程序的可靠性,就是把一段程序用逻辑的方法证明一遍,证明它能得到预期的结果,没有bug。一般这类研究主要应用于昂贵的航天器材的操作系统、危险的医疗设备的程序之中。因为航天器材、医疗...
  • 总共包括synopsys若干讲芯片相关知识。... 芯片验证方法学近十年的发展极大的帮助到了验证工作效率和质量的提升,但是基于传统激励机制的...近几年越来越多的工程师把眼光投向了形式化验证,对比探讨两种方法学的异同。
  • 1.举例对比形式化方法和欠形式化方法的优缺点。 形式化说明: 优点:(1)简洁准确的描述物理现象,对象获动作的结果。 (2)可以在不同软件工程活动之间平滑的过度。 (3)它提供了高层确认的手段。 缺点:大多形式化的...
  • 文章目录关系数据库关系数据库简介关系数据结构及形式化定义关系操作关系模型的完整性关系代数 关系数据库 关系数据库简介 美国????IBM公司的E.F.Codd 1970年提出关系数据模型E.F.Codd, “A Relational Model of ...
  • 关系模式的形式化定义

    千次阅读 2019-12-16 23:21:24
    关系模式由五部分组成,即它是一个五元组: R:关系名 U:组成该关系的属性名集合 D:属性组U中属性所来自的域 DOM:属性向域的映象集合 F:属性间数据的依赖关系集合 ...
  • 形式化验证(Formal verification)让我们可以确保某种错误的状态不会发生。现在已经有很多对以太坊虚拟机语义模型的学术研究以及对使用不同框架的智能合约进行的形式化验证。在这篇文章中,我会描述一种基于符号...
  • (2)定义关系模式 关系模式可以形式化地表示为: R(U,D,DOM,F) R 关系名 U 组成该关系的属性名集合 D 属性组U中属性所来自的域 DOM 属性向域的映象集合 F 属性间的数据依赖关系集合 ·例:· 导师和研究生出自...
  • 开发方法---形式化方法

    千次阅读 2018-08-28 21:30:17
    形式化方法  形式化方法是指采用严格的数学方法,使用形式化规约语言来精确定义软件系统。非形式化的开发方法是通过自然语言、图形或表格描述软件系统的行为和特性,然后基于这些描述进行设计和开发,而形式化开发...
  • 智能合约形式化验证

    千次阅读 2018-06-19 10:59:19
    参考: 智能合约的形式化验证方法 以太坊用形式化验证提高智能合约的安全性 伦敦金融科技公司Aesthetic Integration为基于区块链智能合约推出形式化验证平台...
  • 需求分析学习指导目录:... (1)形式化语言 用户容易理解 描述复杂 不同人理解容易产生歧义 (2)形式化语言(逻辑描述、集合描述、代数描述) 理解困难 表达准确 不会产生歧义 ...
  • DAO、Parity、BEC 等著名项目的市值几乎一夜归零,都是由于智能合约漏洞引起,智能...形式化验证如何保障合约安全? VaaS 平台的作用及优势? 实际案例展示。 关键词:智能合约,形式化验证,VaaS 平台,安全漏洞。...
  • 周以真教授认为计算思维的内容,本质是抽象和自动化,特点是形式化、程序化和机械化。周教授同时给出了计算思维的6个特征。(1)概念化,不是程序化。计算机科学不是计算机编程,像计算机科学家那样去思维意味着远不止...
  • 以B方法和CompCert等软件的出现为标志,形式化软件开发方法实实在在地进入了实际软件系统开发的领域。本文介绍近年软件形式化开发的一些重要进展。今后我们会看到越来越多的经过严格证明的软件系统或者系统部件。另...
  • 形式化验证技术

    万次阅读 2014-10-13 21:46:50
    形式化验证就是基于已建立的形式化规格,对所规格系统的相关特性进行分析和验证,以评判系统是否满足期望的特性。形式化验证并不能完全确保系统的性能正确无误,但是可以最大限度地理解和分析系统,并尽可能地发现...
  • 形式化方法

    千次阅读 2018-03-18 22:20:45
    形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法,其模型、技术和工具已延生成为计算思维的重要载体。...
  • B方法-拓展你形式化方法的视野

    千次阅读 2013-11-26 23:11:41
    形式化的自然语言描述软件规范容易引起二义性等其他问题,人们将数学引入软件开发,建立起了形式化方法。形式化方法在软件开发中有其特殊用途,为我们开发软件提供了更严格的数学逻辑。本文将通过B方法,让你对...
  • 软件工程课后习题,作业范围: 形式化说明技术+总体设计+详细设计 第一题、画出下列伪码程序的流图,计算它的环形复杂度。你觉得这个程序的逻辑.. 第二题、 (1).假设只有SEQUENCE和DO_WHILE两种控制结构,怎么利用...
  • 基于这种技术,VaaS平台经过一年半左右时间研制出的形式化验证平台,是采用了多种形式化的技术开发的一套面向多个区块链的平台,“减少人工干预,更多由机器完成”需要被强调。 以下为成都链安科技CEO &创始人...
  • 形式化、半形式化和非形式化

    千次阅读 2008-07-25 12:38:00
    形式化、半形式化和非形式化是三种类型的规范风格。形式化规范就是用一套基于明确定义的数学概念的符号来书写,并且通常伴随着支持性的解释(非形式化)语句。这些数学概念被用来定义符号的句法和语义,以及支持逻辑...
  • 三种形式化语言和方法

    万次阅读 2010-03-26 13:10:00
    VDM --VDM是在1969年为开发PL/1语言时,由IBM公司维也纳实验室的研究小组提出的,VDM是... VDM技术的基本思想是运用抽象数据类型、数学概念和符号来规定运算或函数的功能,而且这种规定的过程是结构的,其目的是要在

空空如也

空空如也

1 2 3 4 5 ... 20
收藏数 2,211,937
精华内容 884,774
关键字:

形式化