低级语言组合推理的基本理论研究—证明携带代码的安全性和正确性

理论计算机科学电子笔记156（2006）151-168www.elsevier.com/locate/entcs低级语言Ando Saabas and Tarmo Uustalu安藤萨巴斯和塔尔莫乌斯塔卢1，2塔林理工大学控制论研究所Akadeemia tee 21，EE-12618 Tallinn，Estonia摘要携带证明的代码的出现引起了人们对低级语言推理的极大兴趣。人们普遍认为，具有跳转的低级语言必须由于其固有的非模块化而难以推理。我们认为这是不真实的。我们认真对待这一点，与高级语言的语句不同，低级代码段是多入口和多出口的。我们将一段代码定义为由单个带标签的指令或代码段的有限联合组成。因此，我们得到了一个组合的自然语义和匹配的Hoare逻辑的基本低级语言与跳转。通过它们的简单性和直观性，这些可以与标准的自然语义学和霍尔逻辑的WHILE相媲美。霍尔的逻辑是健全和完整的。的语义，并允许汇编证明霍尔逻辑的WHILE。关键词：自然语义，程序逻辑，低级语言，组合推理，认证代码献给Enn Tyugu在他70岁生日1介绍证明携带代码（Proof-Carrying Code，PCC）是一个口号，它的意思是软件生产者有责任确保其安全性或正确性。软件与消费者可以检查的证明一起运送给消费者因此，消费者只需要信任一个证明检查器，它通常是一个可以一劳永逸地手动验证的小程序1研究活动部分得到爱沙尼亚科学基金会第5567号赠款的支助。由欧盟FP5 IST项目eVikings II支持的旅行。2 电子邮件地址：ando@cs.ioc.ee，tarmo@cs.ioc.ee1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.031152A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151PCC的流行引起了人们对低级语言形式化推理的极大兴趣，因为软件通常以编译形式发布。低级语言被广泛认为是难以推理的，因为它固有的非模块性。模块性的缺乏归因于低级代码被重写以及完全不受限制的跳转的显著存在非模块化语言的坏结果是它不能有组合语义或逻辑。在本文中，我们认为，非模块性的前提是不真实的。虽然低级代码片段没有明确的明确结构是正确的，毕竟，它们只是标记指令的有限集合，但它们确实具有固有的部分可交换monoidal结构，由具有非重叠支持的代码片段的有限并集给出事实上，任何一段代码要么是一条带标签的指令，要么是具有非重叠支持的代码段的有限联合（在许多方面都是如此，但绝不是绝对的）。我们表明，这种看似平庸的结构提供了一个非常好的事实上，人们只需要注意到，与高级语言的语句不同，低级代码的片段是多入口和多出口的，然后对于任何合理的低级语言，都不难制定遵循这种短语结构的组合自然语义和Hoare逻辑此外，低级代码自然是由有限个联合体构成的：编译以这种方式生成代码，对于任何通过将较小的代码片段组合在一起来生成代码的过程来说，这一点更普遍从技术上讲，我们制定了一个结构化的版本，大藤SG基本的低-水平（实际上，中间）语言GOTO。然后，我们开发了一个完美的合成自然语义的SG奥托，同意标准的非合成小步操作语义的G奥托。我们还开发了一个霍尔逻辑的SGOTO是健全的和完整的wrt。自然的语义。与PCC相关，我们定义了一个从WHILE到SGOTO的编译函数，允许与程序一起编译证明。我们还显示了这种反向编译的规则提供了关于为什么我们的自然语义规则和SGOTO的Hoare逻辑是这样的额外见解。我们的想法与Tan和Appel [11]关于低级语言的组合逻辑的然而，与我们不同的是，他们没有引入组合语义（对我们来说，这是标准语义和逻辑之间非常方便的联系），他们的逻辑是延续式的，对霍尔三元组进行了相当复杂的解释，涉及显式的定点近似。我们的逻辑是直接的。A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151153本文的结构如下。在第二节中，我们介绍了我们主要的低级学习语言GOTO，它是一种斯巴达语言，具有通用的跳跃，与你好。 在第三节中，我们提出了我们的概念，GOTO代码中的隐式结构，并在几乎相同的语言SGOTO的语法定义中对其进行解释。然后我们给出了SGOTO的一个合成自然语义，证明了它与GOTO的标准操作语义一致，给出了一个合成Hoare逻辑，并最终证明了它听起来很完整。在第4节中，我们定义了从WHILE到SG奥托，表明这保留和reactions评价和可导出霍尔三元组的方式，允许在第5节中，我们展示了一个人也可以从SGOTO翻译成WHILE。第6节是相关工作的讨论，第7节结束。为了参考和修正符号，我们在附录A中回顾了WHILE的语法，自然语义和Hoare逻辑。假设读者熟悉编程语言语义的基本操作和公理化方法，并且应该欣赏组合性的好处。2Goto，一种低级语言我们首先定义一个简单的带有跳转的低级语言，我们称之为GOTO及其标准的非组合小步语义。后藤会是我们将在本文的其余部分开发组合语义和逻辑GOTO码的基本组成部分是标号l∈Label、算术表达式a∈AExp、布尔表达式b∈BExp和指令instr∈Instr。标签是自然数：标签=dfN。算术表达式、布尔表达式和指令由文法3在可数的程序变量x∈Varn∈Za：：= n |X |0+ 1|......这是什么？b：：= a0= a1|......这是什么？ |TT |ff|欧元b|......这是什么？instr：：= x：= a|后藤|如果不是最好去L成对的标签和说明形成带标签的说明：LInstr=dfLabel×Instr。一段代码c∈Code是一个有限的标记指令集：Code=Pfin（LInstr）。如果代码中没有标签，则代码c[3]选择使用ifnotbgotol而不是ifbgotol似乎不合常规，但实际上对我们来说是一个更自然的选择，考虑到while和if语句通常是编译的（见第4节）。154A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151（l，x：=a）∈cc<$（l，σ）→（l+1，σ[x<$→<$a）σ]）：=（l，gotom）∈cc（l，σ）→（m，σ）goto（l，if notbgotom）∈cσ |= bifngotott（l，ifnotbgotom）∈cσ |= bfngotoc<$（l，σ）→（l+1，σ）c<$（l，σ）→（m，σ）Fig. 1. GOTO标准操作语义规则标记两个不同的指令，即，i ∈（l，instr）∈c和（l，instrJ）∈c意味着instr=instrJ.一段代码的域被定义为出现在该段代码中的标签集：dom（c）=df{l|（l，instr）∈c}.GOTO的语义是根据状态来定义的。状态是一对标签l∈Label和存储σ∈Store=dfVar→Z，它们决定了程序计数器（pc）和程序变量在某个时刻的值：状态=dfLabel×Store。算术和布尔表达式的语义是以指称风格定义的，如WHILE，见A节。的代码片段的标准小步操作语义通过由图1中的规则定义的索引单步归约关系→∈ Code → P（State × State）给出。 相关的多步归约关系→E1被定义为它的自反传递闭包。这其中的主要缺点是语义是它是完全非组合的：没有短语结构，并且由于跳转指令，所有代码必须始终可用。引理2.1（确定性）如果c≠（l，σ） →（lJ，σJ） 和c（l，σ）→（LJJ，σJJ），则（LJ，σJ）=（LJJ，σJJ）。Lemma2. 2（Stuckstatetes）c∈（l，σ）/→i ∈l∈/dom（c）.引理2.3（定义域的扩张）如果c0<$c1且l∈dom（c0），则c0<$（l，σ）→（LJ，σJ）i <$c1<$（l，σ）→（LJ，σJ）.3SGoto，结构化版本3.1SGOTO的语义和自然语义定义一个结构化版本的五户一个自然的（自然的），为此，我们用语法定义的结构化代码段sc∈SCode替换了GOTO的非结构化代码段，sc：：=（l，instr）|0|sc0-sc1这个想法是，一段代码要么是一个单一的标记指令，要么是一段代码的有限联合和前面一样，我们定义了一段代码的域由其说明书的标签组成更正式地，域运算由等式dom（（l，instr））={l}，dom（0）={ l }，A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151155NSNSNSNSdom（sc0<$sc1）= dom（sc0）<$dom（sc1）。如果一段代码的所有指令的标签都是不同的，则该代码是良构的：单个指令总是良构的，0是良构的，sc0= sc1是良构的，sc0和sc1都是良构的，并且dom（sc0）= dom（sc1）= dom。请注意，结构良好（片段的域）并不需要相邻性代码的长度不一定是间隔。还要注意，在原始的结构化代码片段上，可以将域和格式良好性理解为一个小的组合类型系统一段非结构化的代码当然可以有很多种结构化的方式，所以如果我们要使用SGOTO的语义或逻辑来推理一段GOTO在相反的方向上，我们有一个健忘函数U∈SCode→Code，归纳定义为：U（（l，instr））=df{（l，instr）}，U（0）=df，U（sc0<$sc1）=dfU（sc0）<$U（sc1）.我们的合成语义SG的其他部分的代码是一个自然的语义。求值关系>−NodeState×SCode×State由图2中的规则定义。 像往常一样，求值关系将从进入一段代码的时刻（初始状态）到相应的可能退出时刻（最终状态）的可能状态，其思想是评估应该对应于导致卡住的状态前四条规则不言自明。边条件m/=l在规则中转到ns和ifngoto表示goto或ifgoto指令只有当它不循环回自身时才终止4。规则00说，如果我们想从pc处于某个状态开始计算sc0和sc1，域sc0，我们需要先计算sc0，然后再计算整段代码，但是从我们被sc0卡住的新状态开始。 规则1是对称的。 规则是需要OODNS来满足终止减少序列一旦PC是程序域之外（规则可以通过从规则i中删除前提l∈dom（sci）来简化。然而，这将使规则的非确定性;额外的前提保证对于任何代码段sc和状态（l，σ），恰好一个规则适用。请注意，由于我们的语义将状态与状态相关联，并且状态为pc赋值，因此可以从任何标签输入一段代码（不仅4 或者，我们可以说，例如，gotons规则的形式（m，σ）>（l，gotom）<$（l′，σ′）（l，σ）>（l，gotom）（l′，σ′）gotons其与规则OD_NS结合给出完全相同的评估。但这感觉太复杂了：在单个带标签指令的情况下，循环检测微不足道。⊕156A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151NS（l，σ）>（l，x：=a）<$（l+1，σ[x<$→a）σ]）：=nsm/=l（l，σ）>（l，gotom）<$（m，σ）后藤NSσ |= b（l，σ）>（l，if notbgotom）<$（l+1，σ）伊芬戈托σ |= b ml伊芬戈托河（l，σ）>（l，if notbgotom）<$（m，σ）nsl∈dom（sc0）（l，σ）>sc 0<$（lJ，σJ）（lJ，σJ）>sc 0<$sc 1<$（lJJ，σJJ）JJ公司简介（l，σ）>sc0<$sc 1<$（l，σ）nsl∈dom（sc1）（l，σ）>sc 1<$（lJ，σJ）（lJ，σJ）>sc 0<$sc 1<$（lJJ，σJJ）JJJJ1（l，σ）>sc0<$sc 1<$（l，σ）nsl∈/dom（sc）（l，σ）>sc（l，σ） 乌德内斯图二. SGOTO的自然语义假设域是左闭右开区间），并退出到任何标签（不仅是结束标签）。乍一看，这可能看起来很奇怪，但实际上隐藏着一个中心思想。一个WHILE语句总是单入口，单出口：它从开头进入，从结尾退出但对于低级代码，情况就不同了：考虑到跳转的存在，允许我们从任何标签进入（甚至从域外的标签;在这种情况下，我们立即被卡住，因此完成，正如规则oodns规定的那样）并在原则上退出到任何地方（它将是我们可以到达的标签，但我们卡住了;这样的标签总是在域外）是完全有意义的我们只获得组合性，因为我们将代码段视为多入口，多出口。很容易证明求值是确定性的（但部分-一段代码可能会循环），并且最终状态下的pc值总是在域之外。引理3.1（确定性）如果（l，σ）>sc_j（lJ，σJ）且（l，σ）>sc_j（lJJ，σJJ），则（lJ，σJ）=（lJJ，σJJ）.Lemma3. 2（Postlabels）If（l，σ）>sc∈（lJ，σJ），则nlJ∈/do m（sc）.更重要的是，我们的SGOTO语义与GOTO的标准非组合操作语义一致。定理3.3（保留评价）若（l，σ）>sc<$（lJ，σJ），则U（sc）<$（l，σ）→<$（lJ，σJ）.证据 通过对（l，σ）>sc_j（l_J，σ_J）的推导进行归纳.QA. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151157定理3.4（卡住的减少序列的若U（sc）<$（l0，σ0）→k（lk，σ k）/→，则（l0，σ0）>sc<$（lk，σ k）.证据 通过对sc结构的归纳和对k.Q的从属归纳，这是一个直接的结果，SG OTO的语义是中性的，相对于在一个GOTO程序上实现的结构。我们写s c0=s c1可以说两段结构化代码在语义上是等价的，即，对任意（l，σ），（lJ，σJ），（l，σ）>sc0<$（lJ，σJ）i <$（l，σ）>sc1<$（lJ，σJ）.定理3.5（中立性wrt。如果U（sc0）= U（sc1），则nsc0=s c1。从非结构化代码片段上的集合论有限并（0，0）的部分交换monoidal结构，我们很容易得到我们的语法有限并运算符（0，0）是结构化代码片段上的部分交换monoidal结构，直到语义等价。推论3.6（部分交换幺半群结构）（i）（sc0<$sc1）<$sc2<$=sc0<$（sc1<$sc2），(ii) 0sc=sc=sc0，(iii) s c0s c1= s c1s c0.3.2SGOTO的霍尔逻辑类似于组合自然语义，我们可以为SGOTO定义一个组合Hoare逻辑。虽然语义与状态相关，其中状态不仅包含程序变量的值，而且还包含pc在某个时刻的值，但Hoare逻辑将使我们能够关联关于状态的断言。当状态为pc赋值时，断言语言将有一个常量来引用pc值。因此，有可能做出将状态约束为对应于某个标签的断言。这使得推理模块化：人们可以只对进入或退出特定代码段的标签进行断言，从而消除了对主代码段的所有标签的全局不变量上下文的需要该逻辑的中心语法单元是断言P∈Assn，断言P ∈ Assn是环境逻辑语言的公式，其签名包括（a）con-用于整数和函数的stants和用于标准整数算术运算和关系的谓词符号，以及（b）作为常数的程序变量x∈Var和用于pc的特殊常数pc 我们写σ |= αP来表示断言P在由（a）标准确定的Z上的结构中成立算术常数、函数和谓词符号的含义，(b)状态σ，在逻辑语言变量的赋值α下158A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151：=hoa{（pc=l<$Q[（pc，x）<$→（l+1，a）]）<$（pc/=l<$Q）}（l，x：=a）{Q}后土和{（pc=l<$（Q[pc<$→m]<$m=l））<$（pc/=l<$Q）}（l，gotom）{Q}（（pc=l<$（（b<$Q[pc<$→l+1]）（<$b<$（Q[pc<$→m ]（l，if notbgotom）{Q}因戈托和电脑（PC）（1999年）0hoa{P}0{P}{pc∈dom（sc0）<$P}sc 0{P}{pc∈dom（sc 1）<$P}sc1{P}{P}sc0<$sc1{pc∈/dom（sc0）<$pc∈/dom（sc1）<$P}阿托霍阿J J J JP| = P{P}sc{Q}Q{P}sc{Q}|= Q conseq HOA图三. 霍尔法则（参数）。一个典型的断言是pc= 0<$x = 1。它在状态（l，σ）i中成立，pc值l为0，变量值σ（x）为1。写作P| = Q表示（l，σ）|= αP蕴涵（l，σ）|=αQ对于任何（l，σ）和α。逻辑的可导出判断，称为霍尔三元组，是一个关系{}−{} ΔAssn×SCode×Assn由图3中的规则归纳定义。和自然语义一样，霍尔逻辑也是组合的。特别是，不存在全局收集不变量。 额外的析取由于语义规则odns，前三个规则的前提条件中的pc/=lQ是必需的。析取m=l是为了说明这种情况当一个跳跃循环回到自身时。没有这些析取，逻辑就不完整。二进制联合的规则可以被看作是while和WHILE语言的顺序组合规则的混合：如果从满足P的状态中的sc0或sc1开始，我们在满足P的状态中结束，那么在运行之后，它们的联合sc0从满足P的状态开始，我们保证在满足P的状态中结束（因为我们将交替地重复sc0和sc1此外，我们知道我们在sc0和sc1的域之外。结果规则与霍尔的规则相同，但注意我们使用侧前提指的是蕴涵的表述，而不是在潜在逻辑的某些（必然不完整的）证明系统中的演绎。我们所给出的逻辑是健全和完整的。证明模仿标准的证明为WHILE。定理3.7（合理性）如果{P}sc{Q}，则对任意（l0，σ0），（lJ，σJ），α，（l0，σ0）|= αP且（l0，σ0）>sc∈（LJ，σJ）意味着（LJ，σJ）|= αQ。证据 通过归纳法推导出{P} sc {Q}。QA. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151159为了证明完备性，我们必须假设我们的断言语言是表达性的，遵循Cook[5]对WHILE的Hoare逻辑的完备性证明。(It这就足以让一个最大的定点运算符可用。）我们将wlp（sc，Q）定义为某个断言P，它表示一段代码scwrt的最弱自由前提断言Q，即，一个状态（l，σ）在赋值αi ≠下所定义的属性，对于任何（lJ，σJ），（l，σ）>sc∈（lJ，σJ）蕴涵（lJ，σJ）|= αQ。引理3.8 {wlp（sc，Q）} sc {Q}。证据 通过归纳总结，对供应链的结构进行了分析。Q定理3.9（完备性）如果，为任何（l0，σ0），（lJ，σJ）和α，（l0，σ0）|= αP且（l0，σ0）>sc∈（LJ，σJ）意味着（LJ，σJ）|= αQ，则{P} sc {Q}。证据设对任意（l0，σ0），（lJ，σJ）和α，若（l0，σ0）|= αP且（ l0，σ0）>sc∈（LJ，σJ），则（LJ，σJ）|= αQ。根据这个假设，P|= wlp（sc，Q）.由引理3.8我们已经知道，{wlp（sc，Q）} sc {Q}。因此，规则conseq hoa给我们{P} sc {Q}。Q4从While到SGoto4.1评价的汇编和保存/审查我们现在继续定义从WHILE程序到SGOTO程序的编译函数，并证明它是合理的，即，保存并反映评估结果。此外，我们还将证明它保持和反射可导Hoare三元组。这几乎是显而易见的，因为WHILE和SGOTO的逻辑都是健全和完整的。但对于PCC更相关的是，编译还保留并反映了建立可推导性的实际Hoare三重推导，从而有效地允许编译证明。我们使用的编译实际上是标准的，除了它产生结构化的代码（我们选择了对我们来说最方便的结构），而且不用说，它是组合的。它由图4中的规则定义。编译关系−\−Label×Stm×SCode×Label将一个标签和一个WHILE语句与一段代码和另一个标签相关联。的思想是编译语句的域将是左闭右开区间。(It可能是一个空的区间，甚至不包含它的临界点）。第一个标签是区间的起始点，第二个标签是相应的终点。编译是完全的和确定的，即，一个函数，并产生一段代码，其支持正好是所需的间隔。160A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151s\scÆÆÆ100+1tff01我的天0分01分钟1x：=a\n+1（l，x：=a） skip\01+1“”% s% 0;%s %1% s\' %sc%0%s %1st\''sctsf+1\'scfÆ Æifbthenseleses\'（l，ifnotbgotolJ+1）<$（（sc<$（lJJ，gotolJ））<$sc）s+1\“”scwhile e bdo s“（l，ifnotbgotolJJ+1）”（sc“（lJJ，gotol））图4.从WHILE到SGOTO引理4.1（编译的总体性和确定性）对于任何l，s，存在s c，lJ这样sl\lJs c。如果sl\lJsc0和sl\lJsc1，则sc0=sc1和LJ01= lJ.Lemma4. 2（Domainofcompiledc ode）Ifsl|lJs c，则dom（s c）=[l，lJ）= df{m |l ≤ ms <$σJ，则n（l，σ）>s c<$（lJ，σJ）.证据 通过对σ>s<$σJ的推导进行归纳。Q定理4.4（评价的反射）如果sl\lJsc且（l，σ）>s c<$（lJJ，σJ），则lJ=lJJ且σ>s <$σJ.证据通过对sc的结构的归纳和对（l，σ）>sc（LJJ，σJ）的导子的从属归纳，得到了sc的结构。Q这可能是值得解释的选择，使用ifnotbgotom 指令，而不是标准的ifbgotom指令在SGOTO。其背后的原因是bdos语句通常的编译方式：{（l，if<$bgotolJJ+1）}{（lJJ，gotol）}在这种情况下，环路保护必须A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151161被否定，或者到{（l，gotolJJ）}跳转{（lJJ，ifbgotol+ 1）}，在这种情况下，在第一次检查保护之前执行跳转。由于在编译到带有ifnotbgotom指令的语言时，这两个都不是必需的，因此我们认为它是目标语言更自然的选择4.2可导Hoare三元组PCC使得编译证明的概念相当有吸引力。很容易证明编译保留了可导出的WHILEHoare三元组（以适当的格式，考虑到WHILE语句证明假设从编译点进入并保证退出到端点）。但也可以给出一个构造性的证明：通过定义一个合成翻译的WHILE程序证明到SGOTO程序证明，即，一个证明编译功能。定理4.5（可导Hoare三元组的如果sl\lJsc和{P}s{Q}，则n{pc=lj证据[非构造性证明]直接从霍尔逻辑的可靠性，评价的汇编和完整性的霍尔逻辑的SG奥托。Q证据[构造性证明：保Hoare三重导子]通过对{P} s {Q}的导子的归纳。Q可导的反射大藤SG通过编译Hoare三元组还可以显示.与保存一样，证明反射的非建设性是一个简单的问题，但同样也有一个建设性的证明。给定一个WHILE程序，我们可以将对于构造性证明，我们必须利用程序证明承认某种范式的事实。定理4.6（可导Hoare三元组的反射）如果sl|lJsc和{P}sc{Q}，则n{P[pc<$→l]}s{Q[pc<$→lJ]}。大藤SG证据[非构造性证明]从SGOTO的Hoare逻辑的可靠性，通过汇编和WHILE的Hoare逻辑的完整性来保持评价。Q证据[构造性证明：保留Hoare三重推导]通过对sc的结构的归纳，利用任何Hoare逻辑推导可以被规范化为一种形式的事实，其中适当的推理与后果推理严格交替：适当的推理总是后跟一个后果推理，而后果推理又后跟一个适当的推理，除非它是一个逻辑推理。162A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151结论是推导的最终判断等。规范化是平凡的：一个序列的几个连续的后果推理可以压缩成一个和一个失踪的后果推理可以扩展成一个平凡的后果推理。Q4.3例如作为一个简单的编译例子，我们给出了一个WHILE阶乘程序及其证明，然后给出了目标SGOTO程序及其证明。WHILE中的阶乘程序是S=dfwhilexndo（x：=x+1;s：=s<$x）。对于这个程序，我们有以下霍尔三重证明（我们在这里从显式地拼出后果推理的附带条件来看，这些从上下文来看是显而易见的）。{x+1 ≤ns}x：=x+1{x≤n}s=x！{x sc <$（lJ，σJ），则有nσ[xpc<$→l]>s <$σJ[xpc<$→lJ]. Ifsc3s且σ>s <$σJ，则（σ（xpc），σ [xpc<$→ n]）>sc<$（σJ（xpc），σJ [xpc<$→n]）.对SGOTO的霍尔规则也可以进行类似的观察。有了从SGOTO到WHILE的翻译，人们可以从霍尔法则你好。类似于从与SGOTO一样，我们也有它在这里，可导霍尔三元组是预先服务和反射。这可以从两个方面来证明：非建设性的和建设性的。定理5.3（可导Hoare三元组的保持与反射）若sc3s且{P}sc{Q}，则n{P[pc<$→xpc]}s{Q [pc<$→xpc]}. 如果sc3s和{P}s{Q}，则n{P[xpc<$$>→pc]}sc{Q [xpc<$→pc]}。6相关工作在霍尔逻辑的早期，相当多的注意力都放在了一般跳跃和限制跳跃的推理上。第一个霍尔逻辑是为 当[7] 和特点的各种建议，[2019 - 04 - 19 00：00：00][2019 - 04：00][2019 - 01：00]当或类似的结构用一般或限制跳转扩展的高级语言。Clint和Hoare，Kowaltowski和deBruin [4，8，6]的逻辑使用条件Hoare三元组（因此证明系统是一个自然演绎系统），能够使A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151165并使用关于标签不变量的假设。在Arbib和Alagic[1]的解中，Hoare三元组有多个出口条件，反映了涉及gotos的语句是多出口的事实非结构化低级语言的推理是随着PCC思想的出现才成为一个活跃的研究课题感兴趣的典型语言是Java字节码或.NET CIL（的子集）。奎格利的逻辑[10] 基于反编译，所以它适用于特定编译器映像中的代码片段在Benton的逻辑[ 3 ]中，存在全局标签不变量，如在D e B rush的逻辑[ 6 ]中。Bannwart和Müller的我们的基本思想是利用低级语言的隐式有限联合结构，并结合对代码片段不仅是多出口而且是多入口的理解，这出现在Tan和Appel的新工作[11]五、与我们不同的是，他们的逻辑是延续式的，并且由于他们选择制定二元联合规则的方式，他们必须使用一个状态（l，σ）对于一段码sci是k-安全的，如果不存在jk和（lJ，σJ）使得U（sc）<$（l，σ）→j（lJ，σJ）/→.的状态（l，σ）k-伪函数P i ∈ P，对任意（lJ，σJ），U（sc）∈（l，σ）→φ（lJ，σJ）和（lJ，σJ）|= P这意味着（lJ，σJ）是k-安全。一个Hoare三元组{P}sc{Q}被定义为有效的，对于任何状态（l，σ），如果（l，σ）k-伪Q，则（l，σ）（k+1）-伪P。7结论和今后的工作我们已经证明，由有限联合给出的代码片段上的明显但看似无趣的结构实际上是低级语言所需要的全部，以便承认具有每一个理想的元理论属性的组合自然语义和Hoare逻辑。此外，这样实现的语义和逻辑描述并不比标准高级语言的标准描述更复杂，我们发现这是了不起的。我们的工作与Tan和Appel [11]的工作有关，但他们没有引入自然语义，我们的逻辑比他们的逻辑更简单，避免了延续，并且通过以标准方式解释Hoare三元组而更常规。我们的工作显然与PCC相关，首先是因为它涉及低级语言，其次是因为有限联合是现实情况下的自然构造，在这种情况下，较大的代码片段通常会作为单独产生的较小片段的总和出现，通常由不同的生产者，然后也应该分别证明正确从PCC的角度来看，我们的方法的一个小问题可能是，我们的逻辑的证明5 令人困惑的是，当两个安装的结构中包含一个或多个组件时，会在两个工作中包含一个或多个组件的组件和一个或多个组件的组件。166A. Saabas，T.Uustalu/理论计算机科学电子笔记156（2006）151结构化的代码片段，所以如果生产者要向消费者提供一段带有证明的低级代码，她还必须揭示她使用的结构，这使得消费者可以恢复原始的高级程序及其证明（如果生产者使用简单的非优化编译器并且消费者知道编译规则）。但这并不重要。更有价值的是，消费者保留了不必自己编译并信任编译器的好处我们认为所有这些对于目前的工作来说都是次要的，因为我们在这里的重点是语义描述。它仍然需要验证我们的方法在现实代码和证明演示（认证代码格式）中的实用性。对于证明编译，这种方法似乎是理想的。引用[1] Arbib，M. A. 和S。 Alagi'c，Proofrule s forgotos，ActaIn form. 11（1979），pp. 139-148。[2] Banwart，F. 和P. Müller，Aprogramlogicforrbytecode，in：Proc. 一个星期的时间。 《语义学、验证、分析和转换》，BYTECODE 2005（英国爱丁堡，2005年4月9日），《理论电子注释》。Comput.科学，出现。[3] 本顿，N.，A typed logic for stacks and jumps，draft（2004）.[4] Clint，M. 和C. A. R. Hoare，程序证明：跳转和函数，Acta Informatica1（1972），pp. 214-224[5] 库克，S。一、一个公理系统验证的可靠性和完备性，SIAM J。7（1978），pp. 70比90[6] de Bruin，A.，Goto语句：语义和演绎系统，Acta Inform。 15（1981），pp. 385-424.[7] 霍尔角A. R.，计算机编程的公理基础，Commun。ACM12（1969），pp. 576-583.[8] Kowaltowski，T.，公理化方法的侧效应和一般跳跃，学报通知。7（1977），pp. 357-360[9] 奥唐奈，M。J.，A critical of the foundations of Hoare style programming logics，Commun.ACM25（1982），pp. 927-935[10] 奎格利角L.，Java字节码程序的编程逻辑，在：D