简介：
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语句，和指针。
理论计算机科学theoretical computer science
关于计算和计算机械的数学理论，也称为计算理论或计算机科学的数学基础。
学科的产生 在几千年的数学发展史中，人们研究了各种各样的计算，创立了许许多多的算法，但以计算或算法本身的性质为研究对象的数学理论却是到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年代后期诺伊曼和图灵等人提出的。诺伊曼等在一篇论文中提出借助于证明来验证程序正确性的方法。后来图灵又证明了一个子程序的正确性。他的方法是：设有一给定的程序，且有变量X1，X2，…，Xn以及输入谓词P(X1，…，Xn)与输出谓词Q(X1，…，Xn)。如果能证明下列指掘事实：若在程序执行前谓词P（X1，…，Xn）成立，则在程序执行后,谓词Q(X1，…，Xn)成立，程序的正确性得证。
图灵的这一结果长期未引起注意，一直到P.瑙尔在1963年和E.F.费洛伊德在1966年重新提出这一方法后，才引起计算机科学界的重视。此后，有不少理论工作者在从事这方面的研究。但正如E.W.戴克斯特拉在70年代中期曾指出的，实际有效的方法是边设计边验证，在设计完毕时证明或验证的过程也同时结束。J.T.施瓦兹和M.戴维斯70年代后期提出了一种他们称之为“正确程序技术”的软件技术。这种方法是先选定成千种基本程序模块，并借助已知的各种验证方法（包括程序正确性证明）来保证这些基本程序的正确性。然后再提出一组能保持正确性的程序组合规则。这样，就可以通过不断的组合，生成各种各样的程序。
有人指出，程序正确性证明技术所发展出来的“循环不变式”，即一个程序中的某一循环的入口或出口点上所附的谓词，有些文献中称作“归纳断言”，可以用来供程序研究用。也就是说，不像过去那样，对一个给定的程序找出其若干个循环不变式，然后借助这些不变式来证明这个程序的正确性；而是在编制这个程序之前，根据对这一程序的要求，找出若干个循环不变式，然后根据这些不变式来生成这个程序。
自动程序设计的概念也是从40年代提出的。图灵在1947年的一篇论文中，提出借助定理证明的方法来设计程序。他的想法大致如下:设要求设计一个程序,使成为计算一个给定的递归函数F(X)的程序，并令F(n)=m（这里n是任一自然数，m是自然数），需要找到一个证明F(n)=m的构造性证明。在有了这样一个构造性证明以后，就可以从这个证明中提取出F(X)的求值算法，然后生成所需要的程序。图灵的这一思想长时间不为人所知。1969年又有人独立地提出了这一想法。
程序语言的形式语法的研究，从50年代中期起有了较大的发展。而形式语义的研究自60年代以来虽有不少研究工作者从事这方面的工作，提出几种不同的语义理论，主要是 *** 作语义学、指称语义学或称数学语义学、公理语义学和代数语义学，但仍没有一种公认在软件技术中够用的形式语义学，因而需要提出一种更适于用到实际计算中的新的语义学。
在程序正确性证明和形式语义学中应用的程序逻辑，是60年代末发展起来的。这是谓词逻辑的一种扩充。原来的谓词逻辑中是没有时间概念的，所考虑的推理关系是在同一时间里的关系。程序是一种过程，一个程序的输入谓词与输出谓词之间的逻辑关系就不是同一时间里的关系。因此，在有关程序性质的推理中，原来的谓词逻辑不够用，需要有一种新的逻辑。
60年代末，E.恩格勒等人创立了算法逻辑。C.A.R.霍尔也创立了一种程序逻辑。这种逻辑是在原来的逻辑上增加一个程序算子而得到的。例如，可以将程序作为一种新的算子置于一个谓词公式的前面，如表达式 ｛S｝P(X1，…，Xn)表示在程序S执行完毕时,谓词P(X1，…，Xn)成立（这里的）X1，…，Xn是程序S 中的变量）。
算法分析和计算复杂性理论 关于算法的复杂性的研究。关于这一领域的名称曾有争论。一般认为，各类具体算法的复杂性的研究称作算法分析，而一般算法复杂性的研究称作计算复杂性理论。计算复杂性理论原是可计算理论的一支，是以各种可计算函数(即递归函数)的计算复杂性（在早期称作“计算难度”）为其研究对象的。可计算性分为理论可计算性和实际可计算性两种。作为可计算性理论一支的计算复杂性理论，是以前者的复杂程度为其研究对象的；而作为计算机科学一个领域的复杂性理论，则是以后者的复杂程度为其研究对象的。
这一分支的基本问题是要弄清楚实际可计算函数类的结构和一些性质。实际可计算性是一个直观的概念。如何对这一概念进行精确的描述，是一个并不容易的问题。60年代中期以来，有关的研究工作者一般是以计算时间多项式有界的函数作为实际可计算的函数。这实际上是一个论题，而不是一个可以在数学中加以证明或否证的命题。有人指出，在有关的多项式次数较高时（如n100的情形），很难说是实际可计算的。
另一个带根本性的问题是：确定性机器与非确定性机器的解题能力的比较问题。人们早已知道，确定性图灵机与非确定性图灵机的解题能力是相等的。因为非确定性机器虽比确定性机器效率高，而如果计算时间没有限制，则确定性机器总可以用穷举的方法来模拟非确定性机器。因此，二者的解题能力是一样的。但在计算时间多项式有界时，二者的解题能力是否相等，这就是有名的P=? NP问题。
关于计算和算法（包括程序）的研究，对串行计算的性质研究较多，而对并行计算性质的研究则还很不够（特别是对异步的并行计算更是如此）。因此，关于并行计算的研究很可能将成为计算机理论的研究重点。
[编辑]补充
关于计算和计算机械的数学理论，也称为计算理论或计算机科学的数学基础。
学科的产生 在几千年的数学发展史中，人们研究了各种各样的计算，创立了许许多多的算法，但以计算或算法本身的性质为研究对象的数学理论却是到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年代后期诺伊曼和图灵等人提出的。诺伊曼等在一篇论文中提出借助于证明来验证程序正确性的方法。后来图灵又证明了一个子程序的正确性。他的方法是：设有一给定的程序，且有变量X1，X2，…，Xn以及输入谓词P(X1，…，Xn)与输出谓词Q(X1，…，Xn)。如果能证明下列事实：若在程序执行前谓词P（X1，…，Xn）成立，则在程序执行后，谓词Q(X1，…，Xn)成立，程序的正确性得证。
图灵的这一结果长期未引起注意，一直到P.瑙尔在1963年和E.F.费洛伊德在1966年重新提出这一方法后，才引起计算机科学界的重视。此后，有不少理论工作者在从事这方面的研究。但正如E.W.戴克斯特拉在70年代中期曾指出的，实际有效的方法是边设计边验证，在设计完毕时证明或验证的过程也同时结束。J.T.施瓦兹和M.戴维斯70年代后期提出了一种他们称之为“正确程序技术”的软件技术。这种方法是先选定成千种基本程序模块，并借助已知的各种验证方法（包括程序正确性证明）来保证这些基本程序的正确性。然后再提出一组能保持正确性的程序组合规则。这样，就可以通过不断的组合，生成各种各样的程序。
有人指出，程序正确性证明技术所发展出来的“循环不变式”，即一个程序中的某一循环的入口或出口点上所附的谓词，有些文献中称作“归纳断言”，可以用来供程序研究用。也就是说，不像过去那样，对一个给定的程序找出其若干个循环不变式，然后借助这些不变式来证明这个程序的正确性；而是在编制这个程序之前，根据对这一程序的要求，找出若干个循环不变式，然后根据这些不变式来生成这个程序。
自动程序设计的概念也是从40年代提出的。图灵在1947年的一篇论文中，提出借助定理证明的方法来设计程序。他的想法大致如下:设要求设计一个程序，使成为计算一个给定的递归函数F(X)的程序，并令F(n)=m（这里n是任一自然数，m是自然数），需要找到一个证明F(n)=m的构造性证明。在有了这样一个构造性证明以后，就可以从这个证明中提取出F(X)的求值算法，然后生成所需要的程序。图灵的这一思想长时间不为人所知。1969年又有人独立地提出了这一想法。
程序语言的形式语法的研究，从50年代中期起有了较大的发展。而形式语义的研究自60年代以来虽有不少研究工作者从事这方面的工作，提出几种不同的语义理论，主要是 *** 作语义学、指称语义学或称数学语义学、公理语义学和代数语义学，但仍没有一种公认在软件技术中够用的形式语义学，因而需要提出一种更适于用到实际计算中的新的语义学。
在程序正确性证明和形式语义学中应用的程序逻辑，是60年代末发展起来的。这是谓词逻辑的一种扩充。原来的谓词逻辑中是没有时间概念的，所考虑的推理关系是在同一时间里的关系。程序是一种过程，一个程序的输入谓词与输出谓词之间的逻辑关系就不是同一时间里的关系。因此，在有关程序性质的推理中，原来的谓词逻辑不够用，需要有一种新的逻辑。
60年代末，E.恩格勒等人创立了算法逻辑。C.A.R.霍尔也创立了一种程序逻辑。这种逻辑是在原来的逻辑上增加一个程序算子而得到的。例如，可以将程序作为一种新的算子置于一个谓词公式的前面，如表达式
｛S｝P(X1，…，Xn)表示在程序S执行完毕时，谓词P(X1，…，Xn)成立（这里的）X1，…，Xn是程序S 中的变量）。
算法分析和计算复杂性理论 关于算法的复杂性的研究。关于这一领域的名称曾有争论。一般认为，各类具体算法的复杂性的研究称作算法分析，而一般算法复杂性的研究称作计算复杂性理论。计算复杂性理论原是可计算理论的一支，是以各种可计算函数(即递归函数)的计算复杂性（在早期称作“计算难度”）为其研究对象的。可计算性分为理论可计算性和实际可计算性两种。作为可计算性理论一支的计算复杂性理论，是以前者的复杂程度为其研究对象的；而作为计算机科学一个领域的复杂性理论，则是以后者的复杂程度为其研究对象的。
这一分支的基本问题是要弄清楚实际可计算函数类的结构和一些性质。实际可计算性是一个直观的概念。如何对这一概念进行精确的描述，是一个并不容易的问题。60年代中期以来，有关的研究工作者一般是以计算时间多项式有界的函数作为实际可计算的函数。这实际上是一个论题，而不是一个可以在数学中加以证明或否证的命题。有人指出，在有关的多项式次数较高时（如n的情形），很难说是实际可计算的。
另一个带根本性的问题是：确定性机器与非确定性机器的解题能力的比较问题。人们早已知道，确定性图灵机与非确定性图灵机的解题能力是相等的。因为非确定性机器虽比确定性机器效率高，而如果计算时间没有限制，则确定性机器总可以用穷举的方法来模拟非确定性机器。因此，二者的解题能力是一样的。但在计算时间多项式有界时，二者的解题能力是否相等，这就是有名的P=? NP问题。
关于计算和算法（包括程序）的研究，对串行计算的性质研究较多，而对并行计算性质的研究则还很不够（特别是对异步的并行计算更是如此）。因此，关于并行计算的研究很可能将成为计算机理论的研究重点。
欢迎分享，转载请注明来源：内存溢出
微信扫一扫
支付宝扫一扫
评论列表（0条）