简介：
Hoare 逻辑(也叫做Floyd–Hoare 逻辑)是英国计算机科学家C. A. R. Hoare开发的形式系统，随后为 Hoare 和其他研究者所精制。它发表于 Hoare 1969年的论文"计算机程序的公理基础"中。这个系统的用途是为了使用严格的数理逻辑推理计算机程序的正确性提供一组逻辑规则。
Hoare 认可 Robert Floyd的早期贡献，他为流程图提供了类似的系统。
Hoare 逻辑的中心特征是Hoare 三乱察元组。这种三元组描述一段代码的执行如何改变计算的状态。Hoare 三元组有如下形式
{P}C{Q}这里的 P 和 Q 是断言而 C 是命令。P 叫做前条件而 Q 叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做: 只要 P 在 C 执行前的状态下成立，则在执行之后 Q 也成立。注意如果 C 不终止，也就没有"之后"了，所以 Q 在根本上可以是任何语句。实际上，你可以选择 Q 为假来表达 C 不终止。
这叫做"部分正确"的。如果 C 终止并且在终止时 Q 是真，则表达式就是"全部正确"的。终止必须被单独证明。
Hoare 逻辑为简单的命令式编程语言的所有构造提供了公理和推理规则。除了给 Hoare 论文中的简单语言的规则，其他语言构造的规则也已经被 Hoare 和很多其他研究者开发出来了。包括并发、过程、goto语句，和指针。
本来,闻道有先后,树业有专工。要求一个领域的人理解另一个领域的知识是有些过分。在今天,如果一个计算机科学的硕士或博士不知道什么是不可判定问题,什么是停机问题,为什么停机问题不可解,什么是NP=?P问题,也有可能会受到讥笑。因为这些问题对于计算机科学而言,太基本、太重要了,它们都属于一门称为可计算理论码祥的学科。是计算机科学研究人员应具备的修养型知识。 可计算理论是关于计算机械本身的数学理论。20世纪前,计算机械总是”算计”别的对象,很少”算计”自己。20世纪 30年代,为了要解决一个基础问题,即是否有存在不可判定问题,数理逻辑 学家提出了几种不同的(后来证明是彼此等价的)关于算法的定义,从而建立了可计算性理论。 科学家令计算机械 自己”算计”自己,奇迹出现了。图灵用对角线方法,把图灵机自己编码,搅进其自己的计算对象中,证明了停机问题不可解。在一定程度上说明了计算机(程序)的能力有限性。30年 代前期,K.哥德尔和S.C.克林尼等人创立了递归函数论, 将数论函数的算法可计算性描述为递归性。30年代中期, A.M.图灵和E.L.波斯特彼此独立地提出了理想计算机的 概念,将问题的算法可解性描述为在具有严格定义的理想计算机上的可解性。30年代发展起来的算法理论,对在40年代后期出现的存储程序型计算机的设计思想是有影响的。图灵提出的理想计算机(称为图灵机)中的一 种通用机就是存储程序型的。
可计算理论主要内容有:自动机论与形式语言理论程序理论(包括程序正确性证明、程 序验证等)形式语义学算法分析和计算复杂性理 论。自动机理论和形式语言理论是50年 代发展起来的。前者的历史还可以上溯到30年代,因为图灵机就是一类自动机(无限自动机)。50年代以来一些 学者开始考虑与现实的计算机更相似的理想计算机,J. 诺伊曼在50年代初提出了有自繁殖功能的计算机的概念。
王浩在50年代中期提出了一种图灵机的变种,这是一种 比原来的图灵机更接近现实机器的机器。他还提出一种 存储带上的内容不能清除的机器,并证明这种机器是与图灵机等价的。
60年代前期,又有人提出具有随机存取 存储器的计算机(简称RAM)以及多带图灵机等。 形式语言理论 导源于数理语言学中的乔姆斯基理 论。在这种理论中,形式语言分为四种:①0型语言②1 型语言③2型语言④3型语言。相应地存在着0型、1型、 2 型、3型四种形式文法。1型语言又名上下文有关语言, 2型语言又名上下文无关语言,3型语言又名正则语言。其中2型语言最受人注意。60年代中期,还发现了这四类 语言与四类自动机之间的对应关系(见表形式语言与自 动机的关系) 在上表中,左边所列的语言恰好是右边与之对应的自动机所能识别的语言(见形式语言理论)。 程序设计理论 包括程序正确性证明和程序验证, 它的一些基本概念和方法是40年代后期诺伊曼和图蠢模嫌灵等 人提出的。诺伊曼等在一篇论文中提出借助于证明来验证程序正确性的方法。
J.T.施瓦兹和 M.戴维斯70年代后期提出了一种他们称之为”正确程序 技术”的软件技术。这种方法是先选定成千种基本程序模块,并借助已知的各种验证方法(包括程序正确性证 明)来保证这些基本程序的正确性。然后再提出一组能 保持正确性的程序组合规则。这样,就可以通过不断的 组合,生成各种各样的程序。
有人指出,程序正确性证明技术所发展出来的”循 环不变式”,即一个程序中的某一循环的入口或出口点 上所附的谓词,有些文献中称作”归纳断言”,可以用来供程序研究用。也就是说,不像过去那样,对一个给 定的程序找出其若干个循环不变式,然后借助这些不变 式带手来证明这个程序的正确性而是在编制这个程序之前, 根据对这一程序的要求,找出若干个循环不变式,然后根据这些不变式来生成这个程序。 自动程序设计的概念也是从40年代提出的。
1969年又有人独立地提出了这一想法。 程序语言的形式语法的研究,从50年代中期起有了较大的发展。而形式语义的研究自60年代以来虽有不少 研究工作者从事这方面的工作,提出几种不同的语义理 论,主要是 *** 作语义学、指称语义学或称数学语义学、 公理语义学和代数语义学,但仍没有一种公认在软件技术中够用的形式语义学,因而需要提出一种更适于用到 实际计算中的新的语义学。 在程序正确性证明和形式语义学中应用的程序逻辑, 是60年代末发展起来的。
这是谓词逻辑的一种扩充。原来的谓词逻辑中是没有时间概念的,所考虑的推理关系 是在同一时间里的关系。程序是一种过程,一个程序的 输入谓词与输出谓词之间的逻辑关系就不是同一时间里 的关系。因此,在有关程序性质的推理中,原来的谓词逻辑不够用,需要有一种新的逻辑。 60年代末,E.恩格勒等人创立了算法逻辑。C.A.R. 霍尔也创立了一种程序逻辑。这种逻辑是在原来的逻辑上增加一个程序算子而得到的。
算法分析和计算复杂性理论 关于算法的复杂性的 研究。关于这一领域的名称曾有争论。一般认为,各类具体算法的复杂性的研究称作算法分析,而一般算法复 杂性的研究称作计算复杂性理论。计算复杂性理论原是 可计算理论的一支,是以各种可计算函数(即递归函数) 的计算复杂性(在早期称作”计算难度”)为其研究对象的。可计算性分为理论可计算性和实际可计算性两种。 作为可计算性理论一支的计算复杂性理论,是以前者的 复杂程度为其研究对象的而作为计算机科学一个领域 的复杂性理论,则是以后者的复杂程度为其研究对象的。
这一分支的基本问题是要弄清楚实际可计算函数类的结构和一些性质。实际可计算性是一个直观的概念。 如何对这一概念进行精确的描述,是一个并不容易的问 题。60年代中期以来,有关的研究工作者一般是以计算时间多项式有界的函数作为实际可计算的函数。这实际 上是一个论题,而不是一个可以在数学中加以证明或否 证的命题。有人指出,在有关的多项式次数较高时,很难说是实际可计算的。
另一个带根本性的问题是:确定性机器与非确定性机器的解题能力的比较问题。人们早已知道,确定性图 灵机与非确定性图灵机的解题能力是相等的。因为非确 定性机器虽比确定性机器效率高,而如果计算时间没有 限制,则确定性机器总可以用穷举的方法来模拟非确定性机器。因此,二者的解题能力是一样的。但在计算时 间多项式有界时,二者的解题能力是否相等,这就是有 名的P=? NP问题。 关于计算和算法(包括程序)的研究,对串行计算的性质研究较多,而对并行计算性质的研究则还很不够 (特别是对异步的并行计算更是如此)。因此,关于并 行计算的研究很可能将成为计算机理论的研究重点。
对于一个判定问题,如果能够编出一个程序,以域 中任意元素作为输入,当相应的个别问题的解答是肯定 的时候, 的执行将终止并输出”是”,否则 的执行不 终止,就称该判定问题为半可判定的。可判定的问题总是半可判定的。集合是递归可枚举集的充分必要条件为 对应的判定问题是半可判定的。 图灵在1936年证明,图灵机的停机问题是不可判定 的,即不存在一个图灵机能够判定任意图灵机对于任意输入是否停机。图灵机的停机问题是半可判定的。图灵 机的停机问题是很重要的,由它可以推出计算机科学、 数学、逻辑学中的许多问题是不可判定的。
第一点：int prime[number]={2}，对单一数组元素赋值不能用大括号，改为int prime[0]=2，因为程序逻辑是要把已知的第一个质数2赋值给质数数组第一个元素。嫌团兆第二点：printf("%d\n",prime[i])在输出每一个质数后已或让经有换车回行符，后面的每5个质数输出一个Tab符就没有意芹租义了，这一小段代码更改为:
printf("%d\t",prime[i])
if((i+1)%5==0){printf("\n")
}
欢迎分享，转载请注明来源：内存溢出
微信扫一扫
支付宝扫一扫
评论列表（0条）