没有合适的资源?快使用搜索试试~ 我知道了~
100理论计算机科学电子笔记65第二次(2002年)网址:http://www.elsevier.nl/locate/entcs/volume65.html15页走向优化的可接受性:一个扩展的正确性观点Wolfgang Goerigk沃尔夫冈·戈里克1,2InstitutfurInformatikundPraktischeMathematikChristian-Albrechts-Universitaüt德国基尔摘要相对程序正确性理论及其保存允许正确实现概念的快速和实际充分的定义,因为它们是通过编译器中实现的转换建立的它通过将有限和无限错误分类为可接受(不可避免)或不可接受(混乱,要避免)来概括Hoare我们将通过特殊的组成图交换性来定义正确的实现,并且我们将进一步扩展这个理论,以表达编译规范和编译程序及其在相同的统一关系设置中的实现的正确性不可接受的错误结果可以在语义上对前置条件进行建模,例如编译器的格式良好性我们的理论允许区分不同的正确的实现要求,例如(水平)为用户程序或(垂直)为编译器实现,就好像我们会打开和关闭编译器选项,并调整一个编译器,以适当地保持正确性在不同的应用程序域。1介绍相对程序正确性及其保存可以充分地模拟正确实现的现实需求,特别是关于有限的运行时错误。机器资源违规有时被认为是不可避免的,我们可以通过可接受的错误来建模在由前提条件指定的领域之外运行程序会导致可避免或不可接受的错误。基本上这个想法是可接受的错误使程序的结果1电邮地址: wg@informatik.uni-kiel.de2本文所报告的工作得到了德国研究共同体的支持(DFG)在Verifix和VerComp项目中,2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。格里格101未定义,因此必须由实现发出信号,而不可接受的错误允许(混乱地)任意程序结果,并且用户必须避免它们以安全地使用程序正确的实现(第2节和第3节)是可传递的(组合,模块化)。可交换实现图可以垂直和水平组合,这对于多遍编译的正确性至关重要,但至少对于编译规范中的模块化编译器正确性也同样重要(即,转换)正确性和编译器实现正确性(第4节)。我们这样定义这些概念:正确的编译器程序是正确编译规范,它们返回的最多是格式良好的源程序的正确实现最后,我们将展示如何将该框架应用于优化和优化编译器(第5节)。我们的工作3介绍了德国联合项目Verifix对Cor-recter的结果[10,31,13,12],并与M. 缪勒-奥姆A. 沃尔夫我们使用关系(逐点)方法,但实际上,最弱的相对谓词变换及其优雅的代数指称理论和证明风格可以用作抽象[30],因此对于构建正确的编译规范以及寻找和呈现特别是手写的正确性证明有很大的帮助到目前为止,我们出于不同的原因而倾向于建立关系。例如,在一个示例中,对于机械证明支持,我们使用PVS我们不仅关注(hor- izontally)应用程序的实现正确性,而且(垂直)关注编译器及其实现,特别是编译器自举本身,这两者联系在一起,严重涉及数据表示问题。为了证明一个现实的完全可信的初始编译器是正确的,并正确地实现为机器可执行文件,我们希望尽可能多地保留数学自由[12]。1.1相关工作为了证明编译器是正确的,我们需要证明指定的转换(定义为抽象的格式良好的程序)是语义正确的,编译器(以及它的机器可执行文件)正确地应用了指定的转换(对于具体的程序表示),并且最多返回格式良好的源程序的正确实现。规范验证是理论信息学和编程语言理论的一部分,J. Mc- Carthy和J.A.1967年的画家[18]。证明风格是操作性的[18,1,2]或指称性的[19],这取决于源语言语义的定义。如果源语言有循环或(函数)过程,则术语重写或3本文件第2、3和4节所界定框架的扩展介绍可以在[12]中找到,该报告作为技术报告提供格里格102∈∈复制规则语义贯穿[16,17]。 其他操作风格分为自然[24]或结构[25]操作或类似状态机[14]。指称语义学始于D。斯科特作者在[15,27,21,23]中使用基于状态变换或谓词变换的代数指称风格 我们还发现大量的机械支持的证明,有时包括编译器源程序的正确性,例如。对于Stanford-Pascal [26],Lisp [7,20]或Standard-ML [4]。高级编译器实现验证-证明编译器源程序的正确性-是一项软件工程任务。在许多正式的软件工程方法和项目中,如VDM(Jones,1990)、RAISE(George et al.,1992年)、CIP(F.L. Bauer,1978)、PROSPECTRA(Ho Bürmann和Krieg-Br ückner ,1993) 、 Z (Spi v e y,1992 ) 、B(Abrial等,1991年),以及PVS系统[6]。机器级编译器实现验证的- 证明二进制编译器可执行文件的正确性-到目前为止几乎还没有,尽管已经制定了要求,例如,[29]第29话:我的世界Chirica和D.F.Martin [3]或J S.摩尔[20]。2正确实施程序是顺序转换程序。编译器采用源程序π SL的(语法表示),有时它成功地终止并返回目标程序mTL。如果是这样,我们需要保证m是π的正确实现。一个实用的编译器,如何-在大多数情况下,实际上几乎在每个源程序上都会失败(几乎每个源程序都有精确的数学含义)。通常有无限多个任意大的源程序。虽然很烦人,但我们都生活在软件错误中。然而,我们仍然希望应用程序员、编译器构造者、操作系统设计者和硬件工程师能够足够明智地检测和发出信号,或者预测和避免每个运行时错误。未检测到的错误可能会产生有害的后果,特别是如果它是故意的所谓病毒或特洛伊木马[8]。不幸的是,攻击者往往比编译器用户更了解编译器的弱点。构造函数不能减轻应用程序员证明其应用程序正确的负担实际上,我们不得不在不知道源程序意图的情况下构造编译器但是编译器不可能保留源程序的所有属性.我们必须在用户、语言设计者和实现者之间协商一个契约,这个契约基于对源语言和目标机器的数学上足够精确的描述,这样用户和实现者就可以在没有误解的情况下达成一致正确实施差异的要求。我们可能会认为源程序是它们的机器实现的规范,因此需要格里格103∪ ∩∅我Ω目标程序应该能够成功地计算出正确的结果,如果源程序可以。另一方面,我们不希望看到目标程序执行计算出的不正确结果,并且每个目标程序结果都应该相对于源程序语义正确[26]。不幸的是,只有当且仅当源程序被定义时,我们才能保证目标程序被定义,这是不现实的。3转型计划我们用输入域Di和输出域Do之间的部分关系(多值部分函数)f<$Di×Do来建模转换程序的语义.因此f是元素f ∈ Di~Do = def2Di × Do. Di和Do中的数据被认为是规则的或非错误的输入/输出数据或状态。为了处理不规则数据,即我们犯了无数的错误,假设每个数据域D由单独相关联的不相交非空误差集D扩展,即,,D=defD·和D= . 为 每个转换程序语义f,我们假设一个扩展版本f∈Di~Do我们用相同的符号f表示。错误是最终的。任何计算都不能从错误中恢复.我们要以“以德待人,以礼待人”为己任。,f是在αi和f(αi) αi上的总和。错误的种类有本质上的不同:它们或者是不可避免的,我们必须接受它们;或者是不可接受的,因此必须避免。实现必须保证可接受的错误被发送信号,因此不会导致意外的错误结果,而不存在不可接受的错误必须由用户证明,例如,如果她/他想要使用省略数组边界检查的优化编译器。我们将允许不可接受的错误导致不可预测的(或混乱的)后果。为了对这种现象进行建模,我们在可接受的非空集A和不可接受或混沌错误的非空集U = def\A中划分。所以我们要求i=Ai Ui和o=Ao 乌奥和f的强误差严格性,即f是在n上的全和,f(Ai)和 f(Ui)Uo.假设误差集包含一个特定的标准误差元素∞,该元素用于模拟有限计算(发散)。我们还要求(d,∞o)∈f,只要有一个从d∈D开始的f的非终止(无限)计算。4、错误不是我们的错误。 我们认为异常是非局部常规控制流程。格里格104ODD⊆⊆我我O我OO我OOOss3.1正确实施设fs为源程序语义,ft为目标程序语义,ρi∈Ds~Dt和ρo∈Ds~Dt是源和目标输入和输出数据。我们要求两个关系ρi和ρo,以及它们的逆ρi−1和ρo−1是强严格误差的(在两个方向上)。定义3.1(正确实现)ft被认为是fs相对于ρi和ρo以及相关误差集(ρi;ft±fs;ρo或更短的ft±fs)i的正确实现。(ρi;ft)(d)<$(fs;ρo)(d)<$At对所有d ∈ Ds成立,其中fs(d)<$Ds<$As(即fs(d)<$Us=<$)。fsfs∈Sems:ioρiρof∈Sem:DtDtt tioft图1.一、表示正确(相对)实现的交换图如果ft是fs的正确实现,那么ft要么返回一个正确的结果,要么返回一个可接受的错误,或者,如果fs可以计算一个不可接受的错误,那么ft可以(混乱地)返回任何结果。3.2保持相对正确性设P Di 和Q Do 分别为前置条件和后置条件。 f是 相对于(前条件和后条件)P和Q称为(相对)正确,Pf(P)QAo如果f以P中的输入开始,那么它要么以Q中的输出结束,要么以可接受的错误结果结束,例如表示机器资源违规的状态。定理3.2(相对正确性的保持)项fs(ρi;ft±fs;ρo)当且仅当对所有P∈Ds和Q∈DsP正确的实现是垂直和水平传递的(组合的)。这是一个关键属性,以便掌握现实的编译器正确性证明的复杂性。我们参考[12]以获得进一步的细节和证明,以及对一些变化的讨论我们在[22]中定义了相对正确性和正确实现的概念,在错误严格关系的非均匀世界中以及在源和目标级别之间存在数据表示的的关键格里格105CLCLdef我O定理(即使在较弱的意义上,可组合性,以及正确实现和相对正确性的保持之间的等价性)仍然有效,当然,该模型仍然概括了部分和全部正确性及其保持。4正确的安装程序程序设计语言的主要组成部分是它的抽象语法程序集L和它的语言语义[·]]L:L−→SemL,从L到相关语义空间SemL的部分函数。 [[·]]L的域是所谓的良构程序的集合如果是良构π和我们所针对的顺序命令式编程语言,[π]]L可以定义为扩展输入和输出数据域DL和DL之间的关系,如前几节所述:I oΩ Ω[[π]] ∈ Sem =(DL ~DL )的。对于源语言SL,目标语言TL和适当的源程序πs∈ SL和πt∈ TL,语义为fs=[[πs]] SL和ft=[[πt]] TL,前一节定义了正确实现的语义关系ft± fs。4.1编写规范每一个编译器程序都在源程序和目标程序之间建立一个映射,实际上是在源程序和目标程序表示之间建立一个映射,例如一方面是字符序列,另一方面是目标代码为了抽象地讨论这种映射,并在语义上将源程序和目标程序联系起来,我们假设我们已经或可以定义编译(或转换)规范。C:SL~TL,抽象的源程序和目标程序之间的数学关系 可能由封闭的归纳定义给出,或多或少是建设性的,或者由术语或图形重写系统应用的一组自下而上的重写规则给出(例如,自底向上重写系统,BURS),例如用于基于规则的代码生成器。定义4.1我们称C为正确的,当且仅当对于任何良构源程序πs∈SL,每个相关的目标程序πt∈ C(πs)都是π s的正确实现,即,当且仅当图2中的图在某种意义上是([[·]] SL−1; C)<$ (±;[[·]] TL−1).请注意,我们不需要为所有格式良好的SL-程序定义,我们也不需要编译器程序语义的这个属性。由于有限主机的资源限制,我们编译程序,无论如何。格里格106CCCCCCCCCCCSLTL公司简介SLTLCCCSemSL[[·]]SLSLvSemTL[[·]] TLTLC图二. 编译规范C对于任何两种编程语言SL和TL,都有一个隐含的自然正确编译规范,它简单地将SL中的任何格式良好的源程序与TL中的每个正确实现联系起来:CC=def [[·]]SL ;±;[[·]]TL当然是正确的。实际上,如果我们只考虑格式良好的程序,它是最大的正确编译规范。但通常不是的子集,反之亦然。可能是确定性的,甚至是空的,因为格式良好可能很难决定,甚至是不可决定的,编译器和编译规范可能会将非格式良好的SL程序(没有语义)与TL程序联系起来。因此,到目前为止与无关,因此将是任何正确的实现。仅仅将我们的编程语言限制为一组格式良好的程序是没有帮助的,因为这样我们将在编译器程序的表示层上遇到同样的问题这一观察表明,程序将SL和TL设置为数据域,并通过特定不可接受的错误元素。 这将使我们也能够正式表达在特别是格式良好的先决条件,即源程序要被正确编译就必须完全填充。我们也将对语义空间SemSL和SemTL这样做。对于SL和TL,我们需要一个不可接受的错误nwf(在USL 关于UTL,对于Sem和Sem我们需要一个不可接受的错误uds(对SL、TL、[[]]SL、[[ ]]TL和±进行了扩展,使这些人为误差元素相互关联,并与SL和TL中的非良构程序相关联。我们再用同样的符号表示扩展的关系。(一)vSemSLSemTL(b)第(1)款vSemSem[[·]]SL[[·]] TL[[·]]SL[[·]]TLSLTLC、 CCSL系列C、CCTL图三.扩展编译规范的正确性。原始图(a)(对于和)是可交换的,当且仅当相应的扩展图(b)是.注意,我们在图3(b)中使用±v来表示(水平)正确实现±和(垂直)正确编译器实现之间的差异。v−1格里格107±CCCCCCTL注释±v(见第4.3节)。F或v(respectivi vely±v)只有相对(部分)正确性的保留在实践中才有意义,即只有±v表示正确的相对(部分)实现,图(b)的交换性才成立扩展的是扩展的正确实现(图4),因此该步骤均匀地适合于建立正确转换和实现步骤的进一步交换图的堆栈,所有这些都正确地联系在一起并通过垂直组合相关。与任何编译器程序一样,编译规范也反映了设计决策。它已经从所有可能的正确实现中选择了特定的目标程序公司简介IDSL系列CTLIDTL见图4。 扩展编译规范定理4.2(正确的编译规范)编译规范C是正确的,当且仅当它是CC的正确实现。4.2正确的安装程序为了证明编译器程序(有时也称为编译器实现或简单的编译器)是正确的,我们希望将其语义与编译规范联系起来。 用编译器自己的源语言编写编译器通常是一个很好的建议。 不过,一般来说,编译器将实现在具有语义空间高级或低级机器主机语言HLSem=(DHL) ~DHL).HLi o如果我们想把一个HL-程序τh称为从SL到TL的编译器,那么我们需要表示关系τs和τt来表示SL-和TL-程序作为数据,在SLj=DHL resp.在TLj =DHL中。请注意,defidefoSL我们倾向于让编译器程序τh就像任何其他HL程序一样。情 况如 图5所 示。 然而,为了将SL' 和TL '等具体程序表示的语言=def−s1;[[·]]SL 和[·]]T LJ =def[[·]]是单值部分函数。我们,一个具体的代表-格式良好的SL或TL程序的表示具有唯一的语义。定义4.3(正确的编译程序)我们称τh为正确的编译程序program,i<$[[τh]]HL ±vCC,即,i[[τh]]HL 是C C的正确实现。如果τh是一个正确的编译器,那么图5下面的图,以及由于垂直组合,外部的图也是可交换的。任何正确v格里格108vSLTLC CCCSem[[·]]vSem[[·]]TL[[·]]SL'中文(简体)CC[[·]]TL'斯瓦特SLjTLJ[[τh]]HL图五、与编译规范相关的编译程序如果下面的图也是可交换的,我们称τh为正确的编译程序编译器程序τh诱导一个相关的正确的扩展编译规范,阳离子Cτ=def(τs;[[τh]];τ−t):SL ~TLsuch使得[τh]]±C±CC.1 Ω Ωvτv如果是正确的话,那就是正确的。分离,即,,[[τh]]HL ±v±v,则τh是一个正确的编译程序(cf. 图6)。也就是说:一个编译器程序是正确的,当且仅当它是一个正确的编译规范的正确实现公司简介ID id中文(简体)C斯瓦特vSLjTLJ[[τh]]HL见图6。编译程序和编译规范。由于垂直组合,正确编译规范的正确实现就是正确的编译器定理4.4设Letτh是一个可压缩的压缩程序,πsJ∈πs(πs)是一个良构SL-程序的表示。 则任意正则πtJ∈[[τh]] HL(πsJ)r表示πs的一个精确实现π t。如果我们将一个正确的编译程序应用于一个格式良好的源程序的表示,我们最多将得到源程序的一个正确实现的表示我们称之为“SL数据πsJ或πtJwell-formed,如果它表示well-formedSL-或TL-程序。则πsJ或πtJ具有语义[πJ]]SLJ res pecti vely[πJ]]TLJ.根据定理4.4,正确编译程序τh的每一个正则结果πtJ∈[[τh]]HL(πSJ),应用于well形式的πsJ,正确实现了πsJ。那就是say:Acorrect应用于格式良好的源程序的编译器最多返回正确的源程序的实现。4.3正确的实施与正确的制造商实施如果我们引导编译器程序,我们一般要区分两个不同的概念正确的实现。源程序将被vHLHL格里格109我我OSL我OTL我O我我我SLSLO一方面,由目标程序正确地实现(将源程序语义与目标程序语义相关联),而编译器本身要在主机上正确地实现(将编译器源程序语义与编译器机器程序语义相关联应用程序πSL、πTL及其表示形式πSLJ、πTLJ、πSLJJ、πTLJJ的错误行为和所需的参数化通常具有不同的性质,并且与编译器的预期错误行为和所需的参数化无关,即:、C语言和编译程序τHL、τHML及其语法规范representations. 我们通过区分±和±v来表示这种区别。例如,让我们假设SL是一种过程编程语言。工艺程序员不希望在以下情况下看到任何不确定性或错误:源程序的计算时间分别为πSLJ,πSLJJ。源亲-g被写为使得[πSL]](ds)<$Ds保持,只要πSL 施加到计算域之外的输入ds∈Ds\[[πSL]]−1(Us)这可能导致不可接受的错误。但这涉及到定期终止,因此πSL的总正确性,过程程序员需要保留任何正确的实现πTL。要求是[[πTL]](dt)Dt每当目标程序πTL应用于表示dt∈ρi(ds),ds/∈ [[πSL]] −1(Us)。这可以通过保持完全正确来保证另一方面,同一个进程程序员将(并且通常必须)接受编译时错误报告,例如HM-memory over loglow,而πSL被编译为πTL,即。,而编译器机器实现在πSL的(语法)表示πSLJJ上运行。关于编译,进程程序员希望保证πTLJJ的执行只要编译器在主机上成功生成πTLJJ,就在定义±和定义±v的误差集之间没有明显的自然映射编 译器程序。F或编译器只实现保持相对(部分)正确性的变体才有意义。然而,幸运的是,我们没有看到这两个正确的实现概念之间有任何进一步的重大干扰。5优化在语言定义中,我们经常会发现这样的短语:“它是未定义的,如果... . ”, 有时编译器甚至会默默地忽略那些使程序语义变得不明确的条件优化涉及对源程序的额外证明义务,以便预测或保证正确的结果。理想情况下,优化不应该改变程序的语义。但是,nec-格里格110我我/∈O我我我安全使用所生成的可执行文件的必要前提条件很难确定,并且常常是不可确定的。因此,它们不会在编译时检查,而运行时检查的开销很在实践中,打开或关闭编译器优化选项可能会产生令人惊讶的,有时甚至是有害的效果,例如,如果一个定理证明器由于实现C编译器的优化而最终证明了错误的定理,那么Otter定理证明器不久前就发生了这种情况。例如,冗余(死)代码消除可能通过消除对于某些输入数据ds∈Ds会导致运行时错误(例如被零除)的代码来违反相对(部分)正确性的保持。的源程序πs相对于r.t.可能是部分正确的一些前置条件和后置条件P_t和Q_t,而优化的目标程序π_t如果应用于d_t,则可能返回未预期的规则但不正确的结果ρi(P),危险地欺骗依赖于在运行时发出错误信号的用户作为另一个例子,如果π1和π2都对布尔表达式c的值没有影响,那么所谓的非切换可能会转换为while(b,if(c,π1,π2))<$→if(c,while(b,π1),while(b,π2))把C移出LOOP。考虑输入dt/∈ρi(P)suc h,b值为false,c导致运行时错误。在这种情况下,πt将不正确地不规则地中止错误,并可能导致危险的情况,例如。,如果πt控制安全关键过程。 变换一般不提供相对于常规(总)正确性。P和Q。出于实际原因,因为我们想要效率,编译规范C或编译器程序语义(如[τh]]HL)有时可能甚至必须返回不正确的目标程序,如果无法保证其输入的额外但是这样一个编译程序如何被证明是正确的呢?一种解决方案是允许任何优化,从而使这些目标程序在定义上是正确的但在实践中,这让用户独自计算出哪些额外的预...条件已被假定,因此需要他的程序输入。我们对正确执行的看法提供了一个更详细的答案。我们将编译器警告作为潜在的可接受错误添加到ATL(编译器输出域),并将特定的不可接受错误添加到Us(源代码)程序输出域):让我们考虑一个编译器警告(例如“警告:数组索引检查忽略行.“)作为潜在的错误消息,即,作为生成的目标程序πt潜在地属于ATL中的可接受错误的集合的指示,在以下意义上:这需要额外的先决条件PDs为您的程序输入,稍等如果您不能保证P,请将此视为错误消息,因为如果将πt应用于ρi(P)之外的输入dt,也就是说:除了通常的编译规范C,每个源代码格里格111我O∈TL·我SL我O我SL我我O程序πs带有一个附加的(优化)先决条件Φ =PC(πs)Ds,PC:SL→2Ds,这导致修改的源语言语义我我[[πs]] SL、PC=def[[πs]]SL(Ds\PC(πs))× {pcf},其中pcfUs读取为现在,如果编译规范或编译器程序将目标程序与优化警告一起交付,则这保证了πs乘πt的较弱正确实现(ρi;[[πt]])(ds)<$([[πs]];ρo)(ds)<$At对所有ds∈ PC(πs)成立,其中[πs]](ds)<$Ds<$As。这种较弱的概念,正确实现(关于[]]SL)可以等价地表示为通常的正确实现,但是关于较弱的语义关系[·]]SL,PC。虽然这是一个值得进一步研究的有趣话题,但我们不希望编译器计算或检查优化前提条件或产生检查它们的代码。但为了正确,不允许默默地忽视它们。它必须产生警告时,它假定目标程序输入的额外优化的先决条件因此,用户希望获得所有必要的信息,以决定目标程序是否可以安全地使用或必须被视为(可接受的)错误。我们的方法的一个关键属性是,可接受的错误必须被检测到,并通过任何正确的实现信号如果一个编译程序τHL相对于一个可接受错误的(垂直)集合ATL被证明是正确的,那么它的任何正确实现也必须用信号表示这些错误。6结论和今后的工作我们的贡献是一个有用的数学框架的发展,以分析实际相关的要求,现实的正确实现和编译器的正确性。 我们的工作是一个全面的,严格的和机械支持的正确性证明的理论基础,具体和实现完全可信的编译器的规范,编译器程序和初始编译器机器码实现(见[12])。在[9]中,我们机械地证明了一个特定的Lisp编译器是正确的。关键的猜想是:如果源程序是良构的,那么任何产生的目标程序都是部分正确性保持意义上的正确实现,即。最多只能产生正确的结果。格式良好的条件是至关重要的.编译器为非格式良好的程序生成不合理的代码虽然没有检查良构性,但已证明的性质仍然很有用:如果我们可以保证源程序是良构的,那么生成的目标程序可以安全地使用。在水平方向上,我们保持部分正确性,但对于编译器,我们证明相对正确性的保持,因为我们不需要或证明从非良构源程序生成的目标程序的任何东西。格里格112我们坚信,我们的理论也足够丰富,可以满足现实世界的优化和优化编译器的要求。保证目标可执行文件正确性的已验证编译器不需要固有地生成无效代码。今后的工作将集中在两个主要专题上。首先,我们已经增强了我们的理论,以捕获正确实现顺序反应程序的需求,这些程序在输入和输出通道上进行语义通信。我们可以把这些程序作为转换程序的一个特殊情况来处理,在我们的意义上,正确的实现实际上等同于保留一个底层状态转换系统的可观察行为,例如我们在卡尔斯鲁厄(和哈雷)的Verifix同事所使用的[13]。第二个主要主题是进一步利用(相对)部分正确性及其保持的重要作用,我们将进一步结合程序检查和运行时结果验证的技术[11]。致谢我们要感谢Verifix项目中的同事,特别是Axel Dold、Thilo Gaul、Gerhard Goos 、 Andreas Heberle 、 Friedrich von Henke 、 Ulrich HoMülmann、Hans Langmaack、Vincent Vialard和Wolf Zimmermann。特别感谢Hans Langmaack;我们在这篇文章的数学框架上一直在密切合作。特别感谢MarkusMüller-Olm和AndreasWolf在相对程序正确性及其保护方面所做的工作,并感谢匿名评审的意见,这些意见有助于改进本文的草稿。引用[1] E. B?orger和D.Rosenz Weig. WAM的 定 义 和 正 确 性。 技术报告TR-14/92,Dip. 信息学大学1992年,意大利,比萨[2] E. Büorger和W. 我很好。将Java虚拟机定义为可证明正确的Java编译平台。第23届计算机科学数学基础国际研讨会(23rd International Symposiumon Mathematical Foundations of Computer Science,LNCS)Springer,1998年。[3] L. M. Chirica 和 D. F. 马 丁 实 现 的 正 确 性 证 明 。 ACM Transactions onProgramming Languages and Systems,8(2):185[4] 寇松。Vista程序的验证编译。内部报告,计算机实验室,剑桥大学,1994年1月[5] A. Dold 和 V. Vialard 。 Lisp 编 译 器 的 一 个 机 械 验 证 编 译 规 范 。 In R.Hariharan,M. Mukund和V. Vinay,编辑,FST TCS 2001:软件技术和理论 计 算 机 科 学 的 基 础 , LNCS 的 第 2245 卷 , 第 144-155 页 。 SpringerVerlag,2001年。格里格113[6] 阿克塞尔·多德使用通用开发步骤进行正式软件开发。Logos-Verlag,柏林,2000年。德国乌尔姆大学博士论文[7] A. D. 弗拉托一种具有动态存储分配。博士论文,德克萨斯大学奥斯汀分校,1992年。[8] W.哥里克重新审视验证者。In M. Kaufmann,P. Manolios,andJ S.计算机辅助推理:ACL2案例研究。Kluwer Academic Publishers,2000.[9] W.哥里克用ACL2证明部分正确性的保持性:一个机械编译器源代码级正确性证明。In M. Kaufmann和JS. Moore编辑,美国德克萨斯州奥斯汀市德克萨斯大学ACL2'2000研讨会论文集2000年10[10] W. Goerigk,A. Dold,Th. Gaul,G. Goos,A. Heberle,F. W. 冯·亨克,联合Ho Bertmann,H. Langmaack,H. Pfeifer,H. Ruess和W.齐默尔曼验证器正确性和实现验证:Verifix方法。In P. Fritzson,editor,Proceedings ofthe Poster Session of CC[11] W. Goerigk,Th. Gaul和W.齐默尔曼没有证据的正确程序?基于标记的程序验证。In R. Berghammer和Y. 李文,《系统规格说明、开发与验证之工具支援》,国立台湾大学计算机科学研究所硕士施普林格出版社[12] W. Goerigk和H.朗马克信息学能够证明大型计算机系统的建设吗?2015年技术报告,Institutfur?rInformatik,CAU,2001年。[13] G.古斯和W.齐默尔曼验证验证者。在E. R.奥尔德罗格和B. Ste Escheren编辑,《正确的系统设计》,LNCS第1710卷,第201 - 209230. Springer Verlag,1999年。[14] Y.古列维奇演化代数:导论。Bulletin EATCS,43:264[15] C. A. R. Hoare , He Jifeng , and A. 桑 帕 约 规 范 形 式 的 设 计 方 法 。 ActaInformatica,30:701[16] H.朗马克论高级程序设计语言中过程参数的正确传递。Acta Informatica,2(2):110[17] 雅克·勒克斯和库尔特·西伯。程序验证的基础(第二版)。John Wiley andSons,纽约州纽约市,一九八七年[18] McCarthy和J.A. 画家.算术表达式编译程序的正确性。 在J.T. Schwartz,editor , Proceedings of a Symposium in Applied Mathematics , 19 ,Mathematical Aspects of Computer Science.美国数学学会,1967年。格里格114[19] R. Milne和Ch.Strachey。程序设计语言语义学理论。查普曼和霍尔,1976年。[20] JS. 摩尔Piton:一种机械验证的汇编级语言。Kluwer Academic Press,Dordrecht,荷兰,1996年。[21] M. 穆勒-奥姆M odular的抽象验证:一个重新定义-一个lgebraic方法提倡逐步抽象,卷1283的讲义在计算机科学。Springer-Verlag,柏林,海德堡,纽约,1997年。[22] M. Müller-Olm和A. 沃尔夫。 论可原谅与不可原谅的错误--兼论翻译正确性 的 合 理 性 。 在 J.M. Wing , J.Woodcock , andJ.Davies , editors ,Proceedings of Formal Methods FM'99,volume 1709 of LNCS,pages 1107-1127,Toulouse,France,1999. 斯普林格。[23] M. Müller-Olm和A. 沃尔夫。关于程序到有限机的转换。In G. Smolka,编辑,编程语言和系统。《2000年职工持股计划》,LNCS第1782卷,第290-304页,柏林,2000年3月。[24] H. R. Nielson和F.尼尔森语义与应用:正式介绍。约翰威利父子公司,奇切斯特,1992年。[25] G. D.普洛特金操作语义学的结构化方法。技术报告DAIMI FN-19,计算机科学系,奥胡斯大学,奥胡斯,丹麦,1981年9月。[26] W.波拉克制造商规范和验证。Hartmanis G.古斯,编辑,LNCS,LNCS的第124Springer-Verlag,1981.[27] A.桑帕约代数方法在设计中的应用。 博士论文,牛津大学计算实验室,编程研究组,1993年10月。技术专著PRG[28] D. S. Scott.计算的数学理论概要。第四届普林斯顿信息科学与系统年会论文集,第169-176页,普林斯顿,1970年[29] K.汤普森关于信托的建议。Communications of the ACM,27(8):761-763,1984.此外,在ACM图灵奖讲座:第一个二十年1965-1985,ACM出版社,1987年,并在计算机攻击:入侵者,蠕虫和病毒,ACM出版社,1990年。[30] A.狼最弱的相对前提语义-平衡认可的理论和相对的转换验证。 博士论文,Te chnis che Fakul tétderChristian-Albre chts-Uni versitét,报告编号:2013年,基尔,2001年6月。[31] W. Zimmermann 和 Th. 高 卢 人 关 于 正 确 编 译 器 后 端 的 构 造 Journal ofUniversal Computer Science,3(5):504
下载后可阅读完整内容,剩余1页未读,立即下载
![doc](https://img-home.csdnimg.cn/images/20210720083327.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 电力电子与电力传动专业《电子技术基础》期末考试试题
- 电力电子技术期末考试题:电力客户与服务管理专业
- 电力系统自动化《电力电子技术》期末考卷习题精选
- 电力系统自动化专业《电力电子技术》期末考试试题
- 电子信息专业《电子技术》期末考试试题解析
- 电子与信息技术专业《电子技术》期末考试试题概览
- 电子信息工程《电子技术》期末考卷习题集
- 电子信息工程专业《电子技术》期末考试试题解析
- 电子信息工程《电工与电子技术》期末考试试题解析
- 电子信息工程专业《电子技术基础》期末考试计算题解析
- 电子技术期末考试题试卷(试卷B)——电子技术应用专业
- 电子科技专业《电力电子技术》期末考试填空题精选
- 2020-21秋《电力电子技术》电机电器智能化期末试题解析
- 电气工程及其自动化专业《电子技术》期末考试题(卷六)
- 电气工程专业《电子技术基础》期末考试试题解析
- 电气自动化专业《电子技术》期末考试试题解析
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)