理论计算机科学电子笔记141（2005）5-32www.elsevier.com/locate/entcs计算机科学对软件实现者的数学推理要求达到什么水平？1从德语开始：一个软件实现者在秋天的信息科学中的数学论证是什么？汉斯·朗马克InstitutfurInforfrmatikderCristian-Albrechts-Universit？atzuKiel奥尔绍森海峡40，D-24098 Kiel，Germany E-Mail：hl@informatik.uni-kiel.de摘要本文从观察软件工程分为两大活动领域开始：软件规范及其验证和软件实现及其验证。为了找到标题中问题的答案，本文研究了一个实用的系统软件工程领域，与其他领域相比，该领域的理论发展得更好：嵌入式构建。我们的答案来自DFG项目Verifix的工作，U.Karlsruhe，U.Kiel，U.Ulm，1995-2003。一个非常复杂的合作任务是为一个现实的高级编程（和编译器编写）语言构建一个所谓的初始正确编译器，该编译器在现实生活中的主机处理器上正确实现和执行。编译规范和编译器实现之间的接口是由代数风格的条件公式转换或程序项重写规则给出的，规范必须证明这些规则是正确的。R. t.源程序和目标处理器语义以及数据和状态表示。编译规范和编译器实现者的密切合作表明，实现者的数学推理是中等深度的代数推理。规范者超越了语义问题，并进行了归纳证明，这是一个更加复杂的数学推理领域。关键词：编译器，规范，实现，正确性，代码检查，项重写，代数推理1本文中的研究得到了德国研究共同体DFG的支持，编号为Go 323/3- 1，2，3，He 2411/2-1，2，3，La426/15- 1，2，3，La 426/16-1。1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.05.0076H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）51提问动机1968年，在加米施北约会议上，F。L.鲍尔创造了软件工程的概念。自20世纪70年代以来，像VDM [45]，CIP（代数学校）[2，64]，Z [70]或ASM [4]这样的学校将软件工程分为两大领域：软件规范和软件实现。关于软件的数学推理被称为软件验证，分为两个学科：软件规范验证和软件实现验证。转换软件的第一个学科手段：从抽象输入到抽象输出数据的指定映射的正确性的数学证明表征面向问题的属性。第二个原则是指：将指定映射转换为可正确执行的编程语言的实现程序的正确性证明如果验证在一个步骤中完成，则指定映射可以看作是由实现程序的语义给出问题：软件规范和实现验证是否需要不同的数学推理水平、种类和能力数学的复杂性有不同的层次吗软件实现验证需要哪种特殊的数学由于软件工程的领域很广，因此首先将其限制在信息学家和软件工程师更熟悉的软件上似乎是明智的：系统软件。因此，我们保护应用软件，这些软件的基本属性不仅由计算机科学家定义，而且首先由应用工程师和科学家定义。第二个限制：在系统软件中，有一个领域到目前为止比其他系统软件领域的理论发展得更好：嵌入式构造。因此，在本讲座中，我们将研究编译规范验证（简称：编译验证）与编译器实现验证，这是从欧盟资助的项目“可证明正确的系统- ProCoS”中接管的，由D.Bjørner和C.A.R.Hoare指导，1989/95 [ 3，50 ]，并在DFG资助的项目“编译器规范，实现和生成技术（编译器）的验证”中进行了更多扩展，由G.Goos，F.W. von Henke 和H.Langmaack ，1995/2003 [19，49，20，26，35，12，21]。[10]的作者可能是第一个提出这两个编译器验证区域之间的区别的人施工人员可以在两个缓解假设下工作[34]：(i) 源代码级应用程序被认为是正确的w.r.t. 它们的特性。这里由应用程序员负责，编译器构造器只需要考虑格式良好的H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）57源程序，而不是应用程序侧的任何进一步意图（除非源程序是编译器构造中使用的系统程序(ii) 硬件，即目标处理器和主机处理器被假定为如它们的说明手册中所描述的那样正确地工作硬件工程师在这里负责，编译器构造器只需要考虑处理器语言的裸语义，而不管硬件编译中的任何错误这一假设的进一步证明是：硬件工程师在故障处理方面比软件工程师有更严格的文化，硬件对恶意攻击表现出更好的抵抗力[53]。由于上面的硬件正确性假设（2.）每个格式良好的二进制编码处理器程序都是可正确执行的。如果有一个相应的编译器（或解释器）程序被正确地实现为格式良好的二进制编码处理器程序，则高级语言程序是正确可执行的。尽管有这两个令人宽慰的假设，但实际上没有可执行的工业-商业编译器，其规范和实现都在完全扩展中得到严格验证参见编译器错误的长列表[21，5，44]。我们必须承认，到目前为止，严格的编译器验证主要是在学术机构或接近学术界的公司中进行的，没有受到激烈的工业竞争。因此，我们应该找出工业软件工程师和编译器构造者必须具备哪些资格，才能进行验证。更好的构造加上严格的验证需要良好的系统软件工程资格和理论信息学和程序语义学的适当掌握，这在某种意义上是数学的特殊领域工业软件工程领域需要大量的理论考虑，这一点并不矛盾每一个良好的工业实践都是基于理论的，在我们的情况下是数学理论L. 玻尔兹曼宣称，没有什么思想比好的理论更实用A.爱因斯坦甚至说，只有理论才能说明什么是适当的实验。我们可以从编译器构造和验证活动中学到什么，以探索哪些类型和风格的数学是相关的？首先，我们试图通过区分编译器的规范和实现来找出问题稍后，为了获得更决定性的答案，我们将查看编译器验证项目中的细节[66，57，58，34，15，52]。本条的初稿见[51]。8H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）52正确实现程序语义和程序的当我们在文献中看到短语“编译器验证”时此外，编制规范验证的结果必须小心处理，其结果通常不切实际，因此存在严重的困难，难以使结果符合工业要求：困难的根源，例如。从过于理想化的目标处理器的有问题的选择，其中每个单元都能够存储任何源语言数据[66]。在理论信息学中，有一种令人遗憾的倾向，即在抽象和具体的数据和程序之间隐藏描述和检索的对于行业中的软件工程师（以及学术信息学家）来说，在规范验证的结果中包含缺失的表示和抽象通常是非常危险的。这些困难还源于目标程序（语义）对源程序（语义）的正确实现的概念的可疑选择也就是说，不同的应用领域和程序员有不同的观点和兴趣：安全关键过程的程序员期望保持程序的整体正确性，作为他正确实现的概念[8，38，56]。这意味着在等效的话：如果一个源程序成功终止，那么目标程序也同样终止。对应的源结果和目标结果。大多数程序员在“通常的”信息处理中既不太注意保证成功的程序终止，也不太注意程序的 这种类型的保存可以等价地表述为：如果目标程序成功终止，那么源程序也同样终止。对应的源和目标结果。编译器的构造函数喜欢把自己看作是一个让他的编译器，用一种特定的或高级的主机语言编写，在主机处理器上实现。由于这个处理器和目标处理器只有有限的资源，因此要求或期望每个格式良好的源程序都能被成功地翻译，并且每个生成的目标程序都能在目标处理器上正确地实现是不合理的然而，编译器构造器必须考虑进一步的和不同的实现正确性概念，这取决于要编译成现实目标处理器代码的源语言的H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）59优化编译器（更好：目标代码改进编译器）值得对源代码和目标代码中的错误进行认真的考虑。总的程序正确性不保证任何愉快的程序属性的情况下，至少有一个不成功的计算开始与相关的前提域中的输入所有错误，如被零除的操作错误、其他执行不足、数组边界违反、循环或递归过程的有限计算、数字或内存溢出以及其他目标处理器错误报告，都被认为是不可接受的、混乱的、不可原谅的，程序用户应避免。另一方面，在部分程序正确的情况下，所有错误都被认为是可接受的，可原谅的，不可避免的。在出现错误的情况下，程序用户只是尝试不同的计算，也许是不同的输入，并希望成功。但是，一旦我们优化了一个保持部分正确性的编译器，情况就发生了用户必须通过输入数据限制来避免错误在实践中，最突出的优化是消除生成的目标代码中的数组边界测试，这是一种特殊的死代码消除。新的编译器不再保持部分程序的正确性.目标代码计算可以成功终止，而不存在以相同的响应成功结束的对应的源程序计算。相应的结果。因此目标处理器如果我们想避免被优化编译器欺骗，那么我们必须在源程序语义中声明数组边界违反为不可接受的错误，用户必须通过对所谓的可接受输入进行适当的限制来避免因此，我们有一种广义的程序正确性，所谓的相对程序正确性，以及在保持相对程序正确性的意义上的实现正确性[59，60，76]。优化编译器的用户手册，特别是商业编译器，必须非常清楚地警告用户，他必须将输入限制为可接受的输入。[62]严厉地批评了现实生活中编译器手册的实际技术水平实现的可执行优化编译器通常不会也不能说哪些输入可能导致具有不可接受的错误的计算用户必须避免它们。在未来，C.A.R.Hoare [40]意义上的验证编译器可能能够警告甚至阻止用户使用不可接受的输入启动翻译程序。让我们把想法形式化正确实现±的概念涉及程序语义fs，ft，数据表示ρi，ρo和数据（状态）do-10H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）5我OS不交换图中的电源Ds，Ds，Dt，Dti o i oDfssi~ D oρi [ H|[ρoDftti~D o其中~或[表示部分定义的多值函数（关系）。由于[59，60，76]，数据域D包括不相交的错误集D = DregAU = Dreg Ω = DaccU。我们有常规数据Dreg、可接受误差A、不可接受误差U和可接受数据Dacc。语义和表示需要是强错误严格的，即Ω上的总数，错误严格，以及除此之外，不可接受的错误严格。定义2.1（交换性或模拟意义下的正确实现）ft对所有容许输入d∈Daccs正确实现fs（fs±ftft（ρi（d））<$ρo（fs（d））<$DacctI o其中d的可容许性意味着fs（d）≠Daccs。没有提到不可接受的d和ft如何处理不可接受的目标输入数据。进一步警告用户将ft应用于ρi表示的容许输入之外的目标输入数据。定义2.2（相对程序语义正确性）f相对于r.t.前置和后置条件Φ<$Di，<$<$Do（简称Φ> f <$>）i <$<f s>蕴含<ρi（Φ）>ft<ρo（φ）><对于所有Φ φDs，Φ φDt.I o这是显而易见的正确的实施意义上的部分resp的保存。总的程序语义正确性。下面的定理对于在通道中编译很重要：定理2.4正确的实现是水平和垂直传递的，即交换图可以在两个方向上组合。将相对正确性和正确实现的概念从程序语义f转移到程序设计语言L的良构程序π是简单的：π被称为相对正确i，它唯一关联的语义[π]L∈SemL是这样的。 并且πt正确地实现了πsi <$[πt]]TL，故[πs]]SL，即[πs]]SL±[[πt]]TL。语义空间SemL定义为：{f：Di~Do}其中Di和Di是与L相关联的输入和输出数据域。语义空间如SemSL、SemTL可以被认为是二阶数据域，并且实现关系SemSL±SemTL（由ρi和ρo参数化）作为对应的程序语义。总的程序正确性意味着部分正确性，并且通常更难证明。另一方面：在维护全面尊重的意义上执行正确。部分程序正确性在逻辑上是独立的。然而，从某种程度上说，部分正确性保持的证明比完全正确性保持的证明更难这一有趣的观察是否有数学依据我们在[55，59，60，76]中找到了答案：作者假设源语言具有指称谓词Transformer语义，目标语言具有操作步骤语义。决定性的分歧是由分歧是否被认为是一个不可接受的错误（总的程序语义正确性）的前提引起的是可接受的（部分程序语义正确性）。完全正确性保持的归纳证明仅仅利用了汇编指令语义的一系列代数定律。但是，部分正确性保持的证明必须在此之上，利用操作目标语义的定点特征化[15]的作者用他们的基于PVS的机械证明对上面的问题给出了以下答案：12H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）5对于完全正确性保持的证明，规则归纳法是可行的，而部分正确性保持则需要更复杂的测度归纳法。我们应该记住，有一个双重成因的不可接受的错误和相关的不可接受的输入的一个良好的源程序，这是正确的实现和执行的目标程序。在不允许输入的情况下，存在与定义2.1中所表达的源程序语义相矛盾的目标程序计算;或者应用于输入的源程序语义不满足用户因此，不可接受的错误的原因是弱点1。的实现技术或2.源程序W。R. t. 其应用。fs的容许输入d也在两个特征子域中分裂第一个是d-s的域，ft（ρi（d））<$ρo（fs（d））<$DregtI o其中规则输入的所有目标计算导致规则结果。对于其他可接受的输入表示ρo，它允许是多值的，利用程序员的慷慨，他准备接受所谓的可接受的目标错误，除了接受常规的3对官方软件认证委员会的要求如何生成最高质量的程序和软件1989/94 年 ， GermanBundersamtfuürSicherheitinderIInformationstechnikBSI发布了IT安全和安保的官方IT认证规定[77，78，9]2。 BSI引入了八个质量级别的可信度，从Q0（一个给定的程序被不充分地检查）到Q7（一个程序的高级语言版本被正式地验证）。特征属性，证明和程序或专业承认的工具）。官方承认意味着：一个官方验证测试套件成功通过由于BSI认为这种承认不符合证明正确性[13]，BSI为编译器工具添加了以下更严格的代码检查要求“The transformations from source to target code exe-cuted by the admitted compiler program must be a-posteriori2其他国家也有类似的活动。H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）513令人惊讶的是，更高的质量水平Q8（程序及其在处理器上的实现被证明是正确的; i.o.w.一个程序被正式验证，就像Q7一样，证明和程序尽管如此，BSI的最高质量等级Q7的IT认证处方已建议我们的ProCoS和验证项目[ 50 ]，[19，49]在如何开发正确的现实编译器的方法中使用检查或检查（通过程序或手动）生成的程序或代码，甚至在二进制真实世界主机处理器代码中尽管BSI没有考虑证明正确和正确实现的编译器（仅在学术上承认），但我们的一个调查结果是，BSI.BSI没有冒险要求更严格的工具广告的原因是-当配方Q7被应用于以高级主机语言HL编写的SL到TL编译器τ 1的验证（上可交换性）和被实现为可执行二进制主机程序（代码）HML的编译器τ2的检查（下可交换性）时，mittance变得知道SemSL±SemTL程序语义[[]]SL↑↑[[]]TLSLH|TL抽象良构程序[英SLJ[[τ1]]HLT LJJ~TLLj[H|[T]LJ具体的形式良好的程序和其他HL-数据SLJJSLJJ[[τ2]]HMLT LJJJJ~TL具体的形式良好的程序其他HML数据14H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）5在下面的图中，ρ-s是程序的表示，与HL和HML等编程语言的输入和输出数据的表示ρ相同。如果BSI要求HL到HML自举编译器工具τ0不仅要经过测试，而且要证明它是正确的和可正确执行的，那么，一方面，τ2的检查是不必要的，但另一方面，需要一个具有同样高质量的进一步的编译器（即τ0），因为我们打算为所谓的初始τ2证明它们。通过BSI但是BSI由于这是讨厌和耗时的[65]，人们可能会考虑开发程序来执行代码检查，但总是有一定数量的代码检查必须手动完成[68，49]。从信息科学的角度来看，认证委员会有义务引入更高的软件质量级别Q8，因为Q8编译器的存在使得（低级）代码检查变得不必要（编译器构建之外），并且因为Verifix项目已经证明，可以构建实际证明正确且正确实现的初始编译器，这些编译器可以在现实世界的处理器上翻译高级系统编程（编译器编写）语言[34，41]。4编译规范与编译器实现BSI的配方Q7并不容易应用。这是因为代码检查（较低的交换性，即如果实现者不知道τ0构造器的抽象HL -到抽象HML -语言特征的算法编译规范C 0，以及他对抽象源和目标数据以及状态的具体表示，则τ2）的正确实现就没有机会仅仅基于HL和HML语义的自然编译规范CC0[34BSIτ0的准入必须包括一个可读的算法编译规范，规范者有义务关心正确性证明。对τ2的精确检验是徒劳的。我们有一个类似的要求来验证编译器τ1。无论验证是用手还是通过机械检定仪的支持完成，了解或定义算法编译规范C1：SL~TLH. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）515不不不不JTL首先，验证C1（即，C1正确实现了SemSL±SemTL的实现关系，即.O. W.对于所有良构π，πsC1πtπt也是合式的，[[πs]]SL±[[πt]]TL ）3其次证明τ1正确实现了C1：C1±[[τ1]]HL(i.e.如果将τ1应用于可接受的表示，πJ∈<$SL（π）<$SLJsSLJs的抽象良构πs4终止于πJ，则有πt∈ C1（πs）<$TL与πJ∈<$TL（π）<$T LJ，tT LJt和πJ是一个可接受的HL-输出数据。如果πJ是不可接受的错误但是一个正规的数据，那么πJ是良构的，[[πt]]TLJ=[[πt]]T L）。大多数情况下，编译器构造器为了节省正确的初始编译器的构造，N.Wirth在20世纪70年代就建议[75] ， 识 别 源 语 言 和 宿 主 语 言 SL=HL ， 目 标 机 和 宿 主 机 TM=HM ，TL=HML，编译规范C1=C0。因此，我们将编译规范的概念理解为（最好是算法）C1的定义，其验证为3自然编译规范CC1=[[] SL; ±;[[] −1是平凡正确的。4.因此，诸如SL或SL′之类的不具有语义的预处理语言的元素被认为是诸如C1或[τ1]]HL之类的翻译的不可接受的输入数据。这些被认为是在输出数据域中将不可接受的错误分配给每个不可接受的输入数据。16H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）5~~TLSemSL ±SemTL[[]]SL↑H|↑[[]] TLC1SL~ TL概念编译器实现自然地分为以高级语言编写的编译器版本τ1和以低级（机器）语言编码的版本τ2的构造，并具有SLC1TL中文（简体）|[2014 - 06 - 25]SLJ[[τ1]]SLT LJJ~TLLj[H|[T]LJSLJJSLJJ[[τ2]]T LT LJJJJ正确的编译器的概念并不要求它配备有完整的语法和静态语义检查器（尽管它的实际重要性），程序员只允许将格式良好的源程序提供给编译器。如果我们有一个SL的超语言SL0的验证编译器，那么我们不需要改变编译器代码来得到一个证明正确的SL编译器，我们只需要通过以下方式（心理）改变代码分配一组更大的不可接受的源程序。5实际正确的初始编译器实现本文的主要目标是弄清楚编译器实现者（而不是第4章末尾定义的编译规范者）应该掌握的数学推理水平因此，我们可以假设编译规范已经正确地完成了他的工作，包括所有的规范验证（规范正确性假设）。SL的一个清晰的操作语义和一个等价的指称语义有助于进行严格的规范验证。为了更好的可信度，应该使用机械定理证明器，例如Acl2，PVS，HOL或KIF[57，7，58，31，32，63，15，12，11，69]，尽可能使用数学家一个可验证的代数编译的可用性规范C1使高级和低级编译器实现验证成为一种纯粹的语法代数推理活动;实现者不需要更长时间地研究所涉及语言的语义方面[34]。H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）517形式方法项目已经为规范和程序开发了正确的细化或实现规则[45，23，2，64]，[42，70，1，14]。但是我们很少看到完整的有据可查的真实编译器程序的派生，这些程序是用二进制真实主机处理器代码写下来的，并且可以被这个处理器或它的一个家族正确5.1实际正确的高级初始编译器实现编译器编写和源语言SL应该与所选择的规范语言非常接近。后者由机械定理证明器确定，如果采用这样的证明器。特别地，SL应该具有良好的编程设施，其允许写下SL-程序片段，其在执行时操纵源和目标程序项作为SL的内部和外部数据。理想情况下，规范语言的抽象程序术语也应该是源语言的内部数据。SL-工具应该允许读者直接证明，只有这样的程序项是规范的条件项重写规则允许的结果在某种程度上，[57，58]使用SL本身作为规范语言，即Boyer-Moore或Acl 2-Lisp。结果：如果SL编写的良构编译器程序τ1的计算以一个格式良好的源程序πs，并以一个规则的结果完成，那么这是一个格式良好的目标程序πt，它也可以由指定演算生成;即τ1被正确地实现。我们演示了一个编译器τ1的构造，这是由于Verifix项目中的相关C1规则，其中SL被定义为ComLisp[24] ， ANSI-Common Lisp 的 子 语 言 [71] ， 有 几 个 很 好 的 理 由 。 一 个ComLisp程序本质上是一个非嵌套函数声明的列表，带有通过值（严格）参数传输的调用。ComLisp只有一种数据类型：s（符号）-表达式，它是具有标准字符串表示的抽象二叉树抽象响应具体的ComLisp程序是特殊的抽象程序。具体的s表达式。ComLisp执行动态类型，编译器可以比标准ML中的静态类型和类型推断更容易处理[54]。这一事实排除了ML的子语言作为SL的候选者。特别是，ComLisp操作符的每一个未定义的应用都会导致在每个实现级别上发出可接受错误的信号。这使得能够实现部分程序正确性的期望的保持。C [46]也不是SL的超语言。C不仅级别太低（而且与二进制处理器代码相距甚远），C这妨碍了可靠的可移植性18H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）5关于C程序的推理C1CLform[[（pf1.. . fn）]]ρ γk=CLfrm[[f1]]ρ γk.CLform[[fn]]ρ γk+n−1（p k）局部和全局变量环境ρ和γ以及相对于堆栈帧的地址k是演算运算符的参数。编译器实现者将此规则作为τ1中函数声明的一部分实现[27]：（defun CL form（form lenv genv k）（cond（（consp form）(let* （（key（carform））（args（cdr form））（n（list-lengthargs）（cond.;;处理形式为;;ComLisp关键字应用程序.（T;;将形式作为标准运算符;;或用户定义的函数应用程序（append（CLformsargs lenvgenvk）（list（listkeyk）.;;处理形式为;;文本或变量.））5.2实际正确的低级初始编译器实现出现了两个问题H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）519(i) 我们在哪里或如何得到一个可执行的编译器τ0，它对应于BSIC1=C0？(ii) 我们如何安排工业上可行的τ2代码检查？广告1.：我们应该将SL定义为工业上使用的超语言SL0的语法和语义子语言，SL 0是由可执行的工业级编译器τ00在现实生活中的处理器M0（例如Intel-Pentium）上实现的|SLτ1TL ||5|5|SL τ1T L|SL|SLτ0T L|T L||SL|SL0τ00ML0|ML0||ML0|由于我们对“编译器”概念的理解，也由于SL程序τ1是格式良好的，因此在成功终止的情况下，τ 00的执行将以结果τ 0结束，该结果τ 0最有可能是τ 1的正确可执行实现。 在成功终止的情况下，τ 0的执行将以结果τ2结束，其最有可能也是τ 1的正确可执行实现。一旦我们根据验证过的编译规范规则C1=C0对程序对（τ1，τ2）进行了严格的代码检查，我们就可以确定τ2也是正确的如果偶然τ00没有正确工作，并且在τ2中侵入了一个错误，严格的代码检查（τ1，τ2）会发现错误，请参阅稍后关于特洛伊木马的如果没有已知的τ 00的算法编译规范C 00，则（τ 1，τ 0）的代码检查是不可行的。广告2.：如果规则过于广泛和复杂，并且源/目标文档非常长，甚至语法代数检查也可能变得难以管理下一节5.3给出了一个现实的方法。5.3多遍编译，良好的编译规范规则和方向检查方法三种行为模式对于语法-代数代码检查的现实、实用验证以及低级编译器实现验证至关重要：[5]我们用麦基曼20H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）5(i) 多遍编译：为了提出只会引起适度扩展的规则，我们将SL= ComLisp到ML= Transclutter代码TC0的翻译C1分为五遍：CLComLispCSintCCCA CT−→SIL −→C −→TASM−→ TC1−→ TC0Project Verifix选择了主容量为1 MByte的 Transcutter T400作为目标的存储器和主处理器M。6这一选择是由于在ProCoS项目中的良好经验，T400可作为独立处理器使用(a) SIL是一种栈中间语言，以s表达式作为数据，操作栈语义和变量名由小的相对地址代替底层堆栈机（也用于下面的Cint）与N.Wirth的P（Pascal）-machine相似(b) Cint类似于C，类似于Java(c) TASM是汇编语言，这里面向Transceiver，没有符号地址，子程序按顺序枚举并通过序列索引调用。(d) TC1是二进制或十六进制字节表示的外部Transcription语言（分别为字）的子程序和初始堆栈和堆。一个小的，253字节长的引导程序是CT的代表，并加载一个格式良好的TC1程序作为一个格式良好的TC0程序。如果前者是COM，则后者以1：1的方式模拟前者从一个格式良好的ComLisp程序中堆出来的。ComLisp、SIL和Cint是独立于机器的。所有的中间语言都像ComLisp一样有s表达式语法。值得一提的是，现实的实践（严格的验证不是主要目的）出于某些原因，使用类似的中间语言进行编译。(ii) 良好的编译规范规则：我们认为translation规则是s表达式上可能多值的部分定义函数的归纳定义的子情况。良好规则的一个最重要的特征是：源和结果s-表达式的并置允许读者识别每个推导（重写）步骤和规则应用的每个相关位置[43]。即使是非常流行的算术也违反了这一特点。看看自然数6代码生成器为i386，DECα，MC68000，C和Forth也可用，但到目前为止，它们依赖于未经验证的软件，如汇编器或辅助编译器，缺乏验证。H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）521加法和乘法：A[[（on）]] =nA[（（+1n）m）]] =（+1A[[（n m）]]）M[[（on）]] =oM[（（+1n）m）]]=A[[（mM[[（nm）]]）]纯加法A是好的，但乘法M不是。例如，为了检查M[[（N M）]的结果N，检查器通常必须进行全新的推导，并查看其结果是否真的等于N[16]。这种现象使得手动结果检查不可行。另一方面，W.Goerigk和U.Ho Bertmann [43，25，26]发现，所有的C1，CL，CS，CC，CA允许结果检查，而无需重复推导结果s表达式。作者指出了以下善良的属性：(a) 没有左或右嵌套的演算运算符应用程序，如第5.1节中的CLform[[· · ·]]··。(b) 组合性，即左手是一个演算运算符应用程序，没有多个左手变量出现，并且右手变量也出现在左手上。(c) 没有出现多个右侧变量。(d) 左边变量出现的顺序保留在右边。变量p和它的无序是不相关的，因为p只代表ComLisp运算符和函数名，它们是原子的（！）s-表达式。这些性质（a）至（d）必须考虑s表达式重写规则的应用所经受的可能条件只有那些s表达式的变量与可行的可检查性相关，这些变量代表可能的非原子（！）s-表达式。上面提到的所有语言都有子例程的概念，并且子例程被翻译成子例程，这是一个巨大的帮助上面的第二个乘法规则违反了（a），（c）和（d）。优化编译使用不满足良好性质的规则因此，初始编译器的构造函数应该放弃优化，并等待以后的引导，当低级别的编译器实现验证不再需要时。所有通道的编译规范规则可以在[25]，[15]中阅读，SL = ComLisp中的规则22H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）5(iii) 对角检查方法：放弃一遍编译，将C1拆分成多遍（见1）不仅导致编译规范规则的扩展性更小。当传递被细化到TC1代码并进行检查时，还有一个更大的优势（实现正确性的水平和垂直传递性）：矩形实现图中对角线以下的所有检查（见下文）实际上都是多余的例如让CA通过实现，向下检查TC1，包括读取和打印例程，并让CC通过，仅向下检查TASM 。 然 后 ， 我 们 可 以 生 成 一 个 正 确 的 TC1- 实 现 τ53 的 CC 上 的Transcutter由于硬件的正确性假设，第1章，第2章。等，CS为τ52，CL为τ51。最有趣的是：这种检查冗余和N.Wirth进一步：打印例程可以改进[52]，以便在高级ComLisp 7中正确实现读取例程（而不是在二进制TC 1中），并将打印例程用作正确实现的结果检查器。剩下的手工工作就是检查给定的和打印的s表达式是否相等。为了一窥Verifix的语法-代数检查方法的可行性1一个完整的代码检查文档，用于一个简短的ComLisp函数声明示例f（x y）[34]：虽然检查是纯粹的语法检查，检查员不需要语义洞察力，原则上，一些语义注释可能有助于理解翻译。ComLisp函数体有两个操作符调用，其重写规则我们在5.1节中已经考虑过。 0、1、2、3是本地地址，SIL（帧长度4），它们对应于Cint、TASM和TC 1（帧长度8）。51 = 33hex，30 =1 ehex，28 = 1chex是f，*和+的跳转表索引;74 = 4ahex字节是TC 1中f的编码体长度。（DEFUNF（* 0）（COPYC6 1）（+0））也是函数声明f（x y）的语义正确的编译结果，但在CL中没有指定，因此会被Verifix的语法检查拒绝7.阅读例程只是形式语言理论中证明正确的词法-上下文无关分析和转换算法H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）523~8CLComLisp~CSSIL~CintCC（defun f（x y）（DEFUN F（DEFUN F（8）（+（*x（COPY0 2）（ SETL（ L0）4）（环境运输及劳工局局长（L1）5）y（副本1 3）（SETL（ L2）6）（环境运输及工务局局长（L3）7））（* 2）（* 4）6（COPYC6 3）（ SETL36）（ SETL67））（+2）（+4））（COPY2 0））（ SETL（ L4）0）（环境运输及工务局局长（L5）1））TASMCL~TC1（DEFCODE F 51（33 z 4aENTCD（75 e0 73 75 e1 73 fa d375 52 d5 75 74 f9 a2 21f0 73 5871 f9 a2 21 f0）LDL 3 LDNL 0 LDL 3 STNL 473 30 73 e4LDL 3 LDNL 1 LDL 3 STNL 573 31 73 e5LDL 3 LDNL 2 LDL 3 STNL 673 32 73 e6LDL 3 LDNL 3 LDL 3 STNL 773 33 73 e7最不发达国家4低密度脂蛋白0低密度脂蛋白 70 21 3ef6最不发达国家3 LDL 3 STNL 6 43 73 e6最不发达国家6 LDL 3 STNL 7 46 小行星73 e7最不发达国家4低密度脂蛋白0低密度脂蛋白 70 21 3cf6LDL 3 LDNL 4 LDL 3 STNL 073 34 73 e0LDL 3 LDNL 5 LDL 3 STNL 173 35 73 e1EXTCD）（75 60 5e d5 7531 d3 75 30 f6））Fig. 1. 代码检查文档除了几个简单的打字错误之外，机械证明者PVS [15]还发现了一个基本错误，该错误发生在[27]其中一个出现在TC1中操作员和功能体的入口代码ENTCD中，即-24H. Langmaack/Electronic Notes in Theoretical Computer Science 141（2005）5['['~结构73 58（LDL 3 LDNLP 8）。LDNLP（加载非本地指针）进行隐式索引计算，而不进行整数算术检查。模232运算在几个地方完成，大多数都是正确设计的，其中四个可能会导致实际的失败，行动时间。[15]3 ADD）。MUL和ADD做过流检查。上述3中的矩形实现图是：SemSL±SemSIL±SemCint±SemTASM±SemTC1↑[[]]SL↑[[]]SIL↑[[]]Cint↑[[]]TASM↑[[]]TC1CLCSSLintCC CASLSL'~SILSILSIL~CintCCint~TASMTASMTASM'~TC1TC1TC'1SLJ[[τ11]]SLJ[[τ12]]SLint'[[τ13]]SLJ[[τ14]]SLJ~SIL~C~TASM~TC1[参考译文][参考译文][参
