CafeOBJ实现硬件/软件划分验证的重写系统

理论计算机科学电子札记95（2004）63-82www.elsevier.com/locate/entcs使用CafeOBJ实现软硬件划分环境下的约简Andr'eLuisSilva1ManoelMessiasMenezes2LeilaSilva3DepmentodeCienciadaComputacaoeEstatsticaUniversidadeFederal de SergipeCEP49100-000-SaoCristovao-SE，Brazil摘要这项工作的重点是硬件/软件划分验证。该方法使用occam作为规范和推理语言。分块系统是从系统的原始描述出发，应用变换规则导出的，这些变换规则都是由奥卡姆基本定律证明的这项工作的目的是显示如何重写系统CafeOBJ可以用来自动证明的划分规则，以及实现的减少策略，指导这些规则的应用通过这种方式，重写系统可以被视为构建分区环境的支持工具，其重点是正确性。关键词：重写系统，硬件/软件划分，划分验证。1介绍硬件/软件协同设计（Hardware/Software co-design）或简称为协同设计（co-design）是一种设计范式，用于混合硬件/软件系统的联合规范、设计和综合。对自动协同设计技术的兴趣是由系统的日益多样性和复杂性以及对早期原型的需求驱动的，以验证规范并在设计过程中为客户提供反馈[7]。1电子邮件：andre@ufs.br2电子邮件：manoel@ufs.br3电子邮件：leila@ufs.br1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.00664A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-在过去的几年中，已经发布了一些支持嵌入式系统硬件/软件协同设计的工具和方法（例如，[4，7，9]，[16]）。协同设计中的一个关键点是算法的可用性，以执行将系统划分为硬件和软件组件。划分是一个众所周知的NP完全问题，除了上面提到的方法之外，还定义了一些算法来指导划分过程（例如，[1，19，21]）。这些方法通过仿真验证了划分系统的有效性。很少有文献[9，10]使用形式化的方法来证明原系统的某些性质在划分之后仍然保持不变由于应用程序的复杂性和多样性的增加，仅仅对分区系统进行验证不足以保证安全性。因此，划分过程的形式化验证，即证明划分后的系统保持了原始描述的语义，是协同设计流程中的一项重要任务在[25，26]中，Silva等人提出了一种强调正确性的分区方法。这种方法接受一个任意的occam描述[14]作为输入，并从该描述中通过应用变换规则（也用occam编写）导出分区系统这些规则的证明，在[25]中给出，使用定义occam [20]语义的代数定律。此外，在[25]中，对将原始描述转化为分块描述所采用的归约策略进行了详细说明，并对所采用文法的构造子进行了结构归纳，证明了该归约策略的正确性已经开发了一些案例研究来验证[25]中提出的方法，其中包括ATM通勤者[12]、静脉输液系统[2]和数字信号处理中使用的卷积问题[11]。为了进行这些案例研究，Iyoda开发了分区策略的实现[11，12]。此实现使用SML [8]，并假设[25]中给出的手动证明是正确的。在[17]中，Menezes等人通过使用重写系统BOBJ [5]详细证明一个这样的规则，说明了重写系统如何用于证明划分规则。然而，[17]没有讨论在重写系统的上下文中，[25]中提出的划分的归约策略的机制。这项工作的目的是补充[25]的形式严谨性，通过使用重写系统CafeOBJ [18]来证明划分规则，以及实现指导这些规则应用的归约策略。为了验证减少战略，在这项工作的背景下，已经开发了一个案例研究，并在结论中总结了结果。实际上，由于篇幅的限制，本文主要研究的是一种单阶段的划分方法，即分裂阶段。然而，这里说明的过程因此，重写系统，A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-65tems可以被看作是开发划分环境的支持工具，其重点是正确性。虽然这项工作在协同设计的背景下是一个新颖的东西，但是已经提出了使用重写系统来实现代数归约策略，例如，Sampaio [22]在编译器验证的背景下（使用OBJ3 [6]）和由里拉[15]在面向对象语言的归约策略的背景下（使用Maude [3]）。此外，已经提出了几种用于硬件验证的形式主义（不一定限于分区），并在[13]中进行了总结。本文的组织结构如下。第2节介绍了在这项工作中使用的形式主义。第3节描述了分区方法，其中详细介绍了拆分策略。重写系统CafeOBJ在第4节中简要介绍。第5节介绍了划分规则的证明最后，第6节给出了结论和未来工作的一些方向。2使用的形式主义：奥卡姆语言Silva等人 [25]使用occam有两个主要原因。第一个是occam是一个强大的模型来表达并发和并行性，对于捕获硬件和软件组件之间的通信第二个原因是奥卡姆的语义是由一组代数定律定义的[20];这些定律在证明分割规则时表现为公理。事实上，[25]采用了奥卡姆的一个子集，定义如下，使用BNF风格。为了方便 起见 ，本文 有时 将occam的语 法线 性化。 例如 ，可 以将 SEQ （ P1 ，P2，...， Pn）而不是标准的垂直样式。P：：=跳过|停止|x：= e| ch？ X |ch！ e| 如果（c 1P 1，c 2P 2，.， cn Pn）| 丙氨酸氨基转移酶（c 1& g 1P 1，c 2& g 2P2，...， c n& g nP n）| SEQ（P1，P2，...， Pn）| PAR（P1，P2. Pn）| VAR x：P| CHAN ch：P在下文中，给出了这些命令的简短描述（更多细节参见，例如，[14]）。SKIP构造没有语义效果，并且总是成功终止。STOP是表示66A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-陷入僵局，无法取得进一步进展。 命令CH？x，ch！e和x：=e分别是输入、输出和分配命令; occam中的通信是同步的。IF和ALT命令根据布尔条件（IF）或保护（ALT）的评估选择要执行的进程。 IF选择是确定性的，也就是说，为真的最低索引布尔条件激活相应的进程;多个布尔条件可以同时为真。在ALT命令中，如果满足多个保护，则选择是不确定的。 虽然IF条件始终是布尔表达式，但ALT保护通常涉及输入命令。 命令SEQ和PAR分别表示进程的顺序和并行组成。VAR和CHAN结构分别声明局部变量和通道。该方法避免在声明变量和通道时提及特定类型;任何类型都适用于这些声明。虽然这种方法没有考虑任意循环，但在构造函数IF、ALT、PAR和SEQ上允许复制器，并且对于处理进程数组很为了简洁起见，这项工作不考虑复制因子。因此，它们在语法描述中被省略了，在3.1节描述的策略中也是如此。Silva等人 [25]扩展了occam的子集，以包括新的构造函数，这些构造函数可以被视为注释，以指导分割规则的应用。这些构造函数没有语义效果。BOX构造函数的目的是在分区过程中将代码块标记为一个整体。CON构造函数表示一个进程是由划分策略引入的，并且不属于系统的原始描述。PARhw和PARsw构造函数分别用于表示硬件和软件组件。PARpar和PARser构造函数指明了流程在每个组件中组合如前所述，奥卡姆的语义由一组代数定律定义。在这项工作中，我们只提出了必要的法律，以了解第3节所述的战略。每一个定律都有一个名字，表明它的用途，还有一个数字。每一条定律的操作性都来自[20]。以下两个定律表达了顺序和并行com的同一性。岗位公式2.1（SEQ-SKIP单位）SEQ（SKIP，P）= SEQ（P，SKIP）= SKIP定律2.2（PAR-跳跃单位）PAR（跳跃，P）= PAR（P，跳跃）=跳跃SEQ操作符按顺序运行多个进程。如果它没有参数，它只是终止。 否则，它会运行第一个参数直到它终止，然后依次运行其余的因此，它遵循A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-67k=1k=1k=1k=1k=1k=1k=1k=1遵循第一定律。PAR算子是结合的和可交换的，这些事实分别由定律2.4（PAR对称）和2.5（PAR对称）捕获法则2.3（SEQ asd）SEQ（P1，P2，.，Pn）= SEQ（P1，SEQ（P2，P3，...，Pn））。定律2.4（PAR asynchronous）PAR（P1，P2，.，Pn）= PAR（P1，PAR（P2，P3，...，Pn））。定律2.5（PAR sym）PAR（P1，P2）= PAR（P2，P1）.条件C是一个布尔表达式，后面跟一个进程或IF构造函数。法则2.6（IFasynchronous）适用于非嵌套IF构造函数，这样所有参数都是布尔表达式，后面跟着一个进程。ALT构造函数也遵循类似的法则。公式2.6（IF asynchronous）IF（C1，IF（C2），C3）= IF（C1，C2，C3）.法则2.7（ALT升高）ALT（ALT（G1），G2）= ALT（G1，G2）。下一个定律允许我们处理IF构造函数，当它们被嵌套为进程而不是条件时。在本书的其余部分，nk=1bkPk用于表示IF（b1P1，b2P2，.，bkPk）。 类似注释-构造器VAR和SEQ也采用了第2.8（如果分配）IF（C，bIFnbkPk）= IF（C，IFnbbkPk）。条件的评估不受随后发生的事情的影响，因此SEQ通过条件来分配条件。第2.9条（按顺序分配）SEQ（IFnckPk，Q）= IFnckSEQ（Pk，Q）。赋值通过一个有条件的、改变条件中赋值变量的发生概率来分配变量。法律第2.10条（转让-如果分配）SEQ（x：= e，如果nckPk）= IFnck[e/x] SEQ（x：= e，Pk）.符号P[e/x]表示对于P中x的每个变量xi的每个自由出现，e的每个x表示ei的替换结果，假设e和x具有相同的长度。x在P中的出现是自由的，如果它不在P中x的任何声明的作用域中，否则它是有界的。如果满足某些条件，则操作符IF可以通过SEQ来分配II F 。法律2.11（SEQ-IF权利分配）SEQ（P，IFnckQk）= IFnckSEQ（P，Qk），如果68A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-k=1如果c1≠c2≠. cn第2.12条（跳过）<>：=>=跳过。在变量作用域的最末端给它赋值是没有意义的，因为给它赋值是没有效果的。同样，如果一个声明的变量从未被使用过，那么它的声明就没有效果。接下来的两个定律抓住了这些事实。第2.13条（转让elim）VAR x：（ + y）：=（ + f）= VAR x：（y：= f）。定律2.14（VAR elim）VAR x：P = P，如果x在P中不是自由的。绑定变量的作用域可以在不影响其他同名变量的情况下增加。法则2.15（VAR-IF distrib）指出，如果条件的每个子过程都声明了变量x，并且这个变量在布尔条件中不是自由的，那么声明可以被移动到构造函数之外。 类似的推理也可用于扩大渠道声明的范围，如第2.16号法律（CHAN-PAR）。第2.15条（VAR-IF分配）nk=1 ck（VAR x：Pk）= VAR x：IFnckPk，前提是x在无ck中是自由的。第2.16（CHAN-PAR）号PAR（CHAN ch：P，Q）= CHAN ch：PAR（P，Q）。变量是在一个列表中声明还是单独声明都没有关系。第2.17条（增值税）VAR x1：（VAR x2：（. VAR xn：P））.） = VAR x1，x2，...， xn：P.VAR运算符可以在SEQ.第2.18条（VAR-SEQ 1）SEQ（VAR x：P，Q）= VAR x：SEQ（P，Q），条件是X在Q中不是游离我们可以更改绑定变量的名称，前提是新名称尚未用于自由变量。第2.19条（VAR更名）VAR x：P = VAR y：P[y/x]，如果y在P中不是自由的。如果A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-69在[25]中引入的用于指导划分策略的构造函数没有语义效果。例如，对于BOX和PARpar构造函数，这一事实由下面的两个定律所捕获。第2.20条（PAR标准单位）PARpar（P）= PAR（P）。第2.21条（BOX单位）BOX（P）= P。3分区方法[25]中提出的划分方法通过应用特定于划分的变换规则和一些奥卡姆定律，从原始描述中推导出对划分系统的描述。整个过程可以概括为：原系统=<分割规则，奥卡姆定律>分区系统实际上，划分过程分为三个阶段：拆分、组件定义和连接。分裂阶段的目的是将系统的原始描述转换为分裂范式的描述。定义3.1（分裂范式）如果一个进程具有以下结构，则它处于分裂范式中：CHANch1，ch2，. ，chm：PAR（P1，P2，. ，Pr）当r是一个Pi，1≤i≤r时，它是一个简单的函数。基本上，每个简单进程最多执行一个原子进程，它可以是原始进程（SKIP，STOP，x：=e，ch？ x，ch！ e）或由BOX构造函数封装的一组进程。简单过程的详细形式与本工作的背景无关，可以在[24，25，26]中找到。这种转换的目的是隔离所有相关过程，以便在下一阶段进行分析，在下一阶段中决定组件由于所有的进程都在同一级别的描述（immedi- ately下的外部PAR构造器）和PAR运营商是联合和可交换的，分裂范式允许充分的可扩展性分组时，无论是在硬件或软件组件的进程。请注意，在不改变70A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-说明.在定义组件的阶段，描述没有实质性的改变。在这个阶段，应用逻辑学来决定哪些进程将组成硬件和软件组件，以及这些进程应该组合的方式，是串行还是并行。划分算法考虑的度量包括进程间的功能相似性、并行度相似性、并发行为相似性和数据依赖性。在这个阶段中采取的决定是使用构造器PARhw，PARsw，PARser和PARpar以及并行运算符的结合性和交换性来表示的。图1示出了该阶段之后的系统描述。例如，进程P9、P10、P15和P18属于同一硬件组件（ 由PARhw 注 释） 。 此外 ， 要求 在分 区 系统 中 ，进 程 P15和 P18 并 行执 行（PARpar），其它两个进程与它们串行执行（PARser）。Fig. 1. 组件定义阶段之后生成的描述示例分区系统的最终描述实际上是在连接阶段通过应用转换规则实现的，就像在分裂阶段一样。该阶段的目的是将在拆分阶段生成的描述（并在组件定义阶段进行注释）转换为连接范式的描述，该描述将系统划分为硬件和软件组件。定义3.2（连接范式）如果描述具有以下结构，则该描述处于连接范式中CHANch1，ch2，. ，chs：PAR（Q1，Q2，. ，Qt）其中，通过将g与h定义为3.1，s≤m，t≤r和eac hPi，1≤i进行比较，1≤j≤t时，EachQk，1≤k≤t-1表示两个波形或波形的所有部分都是互补的，Qt表示该部分硬件和软件之间的过程在[25]中，总共提出了90条划分规则，并进行了人工为了展示重写系统（特别是CafeOBJ）如何A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-71k=1本文重点讨论了分裂阶段，它可用于此类规则的证明的机械化和划分的归约策略的实现。然而，这里所示的过程是通用的，并且可以扩展到整个分区流程。在下一节中，将详细介绍分裂范式3.1分裂战略分裂阶段的目的是将系统的原始描述转换为定义3.1给出的规范形式的描述。为了实现规范形式，应用的减少策略，基于代数规则的应用。这一战略包括两个主要步骤。在第一步中，IF和ALT命令被简化为简单的形式。在第二步中，在第一步中生成的描述的过程被并行放置。要将任意程序（使用第2节的语法描述）转换为分裂范式的描述，八条规则是必要和足够的。出于简洁的原因，在本文中，我们详细介绍了一些这样的规则。该策略的完整描述可以在[24，25]中找到。规则3.1（IF分段）将任意条件转换为二元条件序列，每个二元条件对应于原始条件的每个分支。这一规则的应用允许通过组件的定义阶段对条件的每个子过程进行灵活的分析。第3.1条规则（国际条约不成体系）nk=1=VARnbkPkCkSEQk=1BOX（序列号Ck ：=）nk=1SEQnBK Ck ：=TRUEIF（ck Pk，真跳过）k= 1假设每个c k是新变量（仅在明确示出的情况下出现）。请注意，Rule右侧的第一个IF运算符的作用3.1（IF分段）是做出选择，并允许随后的条件在序列中执行。这就是为什么新变量c1，c2，.Cn的引入。否则，一个条件的执行可能会干扰序列中后续条件的执行。请注意，规则的两边具有相同的行为。在左手边，第一个如果如果72A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-k=1k=1k=1bitobetruea ctivatesthecorre spondingprocess sPi. 另一方面，当bi为真时，ci为真，而其它ck，ki=i为假。 只有Pi执行。第3.2条（低价竞标不成体系）nk=1=nk=1（b k） &（gkPk）CkSEQBOX（序列号ck：=）nk=1nk=1（b k） &GK Ck ：=TRUE）（IF（ckPk，TRUESKIP））假设每个c k是新变量（仅在明确示出的情况下出现）。ALT构造函数也遵循类似的规则，即规则3.2（ALT分段）。IF和ALT规则之间的区别在于用等价的ALT进程（在规则的两侧）替换具有多个分支的条件进程。此外，注意，由于BOX过程是原子的，这些规则右边的第一个过程是简单形式的。此外，带有多个分支的IF和ALT命令只执行一个基本过程（对布尔变量的赋值），因此也很简单。通过这种方式，这些规则的应用统一了ALT和IF命令的处理，因为只有二元条件可能不是简单的，因为Pk可能不是原子的。 在这种情况下，规则是在SEQ、PAR和IF构造函数上分发连接所必需的;在本工作的其余部分中，这些规则被称为IF分发规则。这些规则的目的是将所有条件句移动到描述的最内部层次。例如，规则3.3（IF-SEQdistrib）用于将IF构造函数分布在SEQ构造函数上。规则3.3（IF-SEQ分配b）IF（b VAR x：SEQnPk，真跳过）=VAR c： SEQ（c：= b，VAR x：SEQn假设c是新变量。IF（c Pk，TRUE SKIP））在减少IF和ALT命令之后，系统的描述是并行和顺序构造器的层次结构，并且在第二步骤中，这些构造器被减少，目的是实现分裂范式。第二步开始于应用法则2.1（SEQ-SKIP单元）、2.2ALTVARALTSEQA.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-73（PAR-SKIP单元）、2.3（SEQ ASSEMBLY）和2.4（PAR ASSEMBLY）将第一步中生成的描述转换为二进制形式的描述。法则2.19（VAR重命名）也可以用来保证局部变量的名字与全局变量的名字不相交。在此之后，命令SEQ和PAR最终被减少。规则3.4（序列分割）用于将两个原本按顺序排列的进程并行放置。由于顺序进程可能具有数据依赖性，并且由于oc-cam并行进程不共享变量，因此引入了通信来执行这种转换。在这个规则中，每个原始过程都是封闭的，在这个意义上，所有使用和分配的变量都是局部的。原始过程通过控制过程（用CON操作符注释）与环境交互，当然，原始过程包括输入或输出命令时除外。控制过程充当原始过程之间以及原始过程与环境之间的接口。第3.4条规则（按序号分列）VAR z： SEQ（P1，P2）=CHAN CH1、CH2、CH3、CH4：PARVAR x，z：SEQ（ch？ x，z，P，ch！ xJ，zJ）1 111 1121 1VAR x，z：SEQ（ch？ x，z，P，ch！ xJ，zJ）2 232 2242 2CON（VAR z：SEQ（SEQ（ch！ x，z，ch？xJ，zJ），1 1 221 1SEQ（ch ！ x，z，ch？xJ，zJ）3 2 242 2免费提供（P1）=x1 z1，free（P2）=x2 n=2，x=1 2002年，z=z<$z，xJ<$zJ=ass（P），i=1，2，ch，ch，ch和ch12i ii1 2 3 4仅在明确显示的情况下发生。项z是SEQ（P1，P2）的局部变量的列表，free（P）代表P的自由变量，ass（P）代表在P内分配的自由变量。注意，尽管所有进程在规则3.4（SEQ分割）的右侧并行，但控制进程保证P2与P1顺序执行（P2仅在通过通道ch2同步后执行）。因此，规则的两边具有相同的行为。为了减少PAR构造函数，该策略包括一个类似于Rule的规则3.4（SEQ分裂）。此外，还需要一个辅助规则来分配通信。这三条规则被称为本工作其余部分 在这一步之后，第2.4条（PAR assumption）和第2.16条74A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-（CHAN-PAR），得到分裂正规形.这些规则中的每一个都在[25]中得到了证明，以规则3.3（IF-SEQ distrib）的二元情况证明的风格，如下所示。证明从方程的右边开始，通过应用一些奥卡姆定律，推导出方程的左边。这个证明使用引理3.3（IF分支elim）在[25]中证明，并在下面给出引理3.3（IF分支elim）IF（b1P1，b2P2，. ，biPi，. ，bjPj，. ，bnPn）=证据IF（b1P1，b2P2，. ，biPi，. ，bnPn）提供dbjbi.VAR c： SEQ（c：= b，VAR x：SEQ（IF（c P1，TRUE SKIP），IF（c P2，TRUE SKIP）={公式（2.9）}VAR c： SEQ（c：=b，VAR x：IF（c SEQ（P1，IF（cP2，TRUESKIP））TRUE SEQ（SKIP，IF（cP2，TRUE SKIP）={c/∈free（P1），laws（2.11） and（2.1）}VAR c： SEQ（c：=b，VAR x：IF（c IF（c SEQ（P1，P2），TRUE P1）TRUE IF（c P2，TRUESKIP）{定律（2.8）<$−IF distrib >和布尔代数}，c/∈x，定律（2.15）VAR c：SEQ（c：=b，IF（c VAR x：SEQ（P1，P2），TRUE VAR x：SKIP））={定律（2.14）和（2.10）<赋值-IF distrib>VAR c：IF（b SEQ（c：=b，VAR x：SEQ（P1，P2）），TRUE SEQ（c：=b） b，SKIP））={c/∈free（P1）free（P2），laws（2.15），（2.13） and（2.14）}IF（b VAR x：SEQ（P1，P2），TRUE SKIP）QA.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-75分割策略可以通过以下描述的算法来总结：76A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-算法1（分割策略）第1步：全面适用第2.6条（IF ASSEMBLY）、第2.7条（ALTASSEMBLY）和第2.17条（VARASSEMBLY）。第2步：全面适用规则3.1（IF分段）、3.2（ALT分段）和IF分配规则。步骤3：详尽地应用定律2.1（SEQ-SKIP单元）、2.3(SEQ 2.2（PAR-SKIP单位）和2.4（PAR_（asd））。第4步：如有必要，适用法律2.19（VAR重命名）第五步：彻底应用第二步的规则第6步：彻底应用第2.4条（PAR assumption）和第2.16条（CHAN-PAR）。4CafeOBJCafeOBJ [18]是新一代代数规范和编程语言。作为OBJ家族（OBJ 1，OBJ 2，OBJ 3）的继承者[6]，它继承了以下特性：强大的类型系统和子类型;复杂的模块组合系统，具有多种导入;参数化模块;用于实例化参数和模块表达式的视图，以及其他问题。CafeOBJ实现了新的范例，例如重写逻辑和隐藏代数，以及它们的组合。它主要用于系统规格说明、规格说明的形式验证、快速原型、编程和自动定理证明。选择CafeOBJ是由于一些特征，其中包括文档的可用性、使用缩减机制的便利性、以两种方式应用规则的可能性以及要缩减的术语的子项。CafeOBJ中的模块的语法定义为模块mod id>mod elem，其中mod id>是模块的名称，mod elem是模块的元素。<<模块元素可以是导入声明、排序声明、运算符声明、记录声明、变量声明、等式声明或转换声明。这些要素分为三个主要部分。第一部分，导入，指定哪些模块应该被导入，也就是继承。导入模块有三种形式：保护（导入的模块不能被改变）、扩展（导入的模块可以被扩展，但原始描述保持不变）和使用（导入的模块可以被扩展或可以改变原始描述）。第二部分，签名，声明模块使用的排序，运算符，记录和子排序。最后，公理包括变量、方程和转换的声明，并表示模块的行为。为了说明CafeOBJ中的模块描述，考虑以下示例。模块SQRINT继承了A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-77INT和NAT模块。节签名声明了两个排序Nat和Int。符号表示Nat是Int的子排序。< 由op引入的sqr运算符接收一个整数参数并返回其平方，这是一个自然数。sqr的行为由eq引入的表达式捕获。%模块SQRINT{imports{保护（NAT）保护（INT）}签名{[NatInt]操作sqr：Int-> Nat}公理{varI： Int等式sqr（I）=（I * I）。}}%5使用CafeOBJ使用CafeOBJ的分裂策略的机械化有三个主要阶段：奥卡姆定律和分裂规则的实现（第5.1节），这些规则的证明（第5.2节）和归约策略的实现（第5.3节）。在下文中，我们将详细介绍这些阶段。5.1奥卡姆定律和分裂规则在实现奥卡姆定律和分裂规则之前，定义一个模块BASE这个模块包括其他模块 使用的排 序和运算 符的声明 例如， 模块BASE 包括 分类Process 、Expression、List_Processes和List_Expressions，分别用于对进程、表达式、进程列表和表达式列表进行分类。符号奥卡姆定律在OCCAM-LAWS模块中实现。在下文中，示出该模块的片段以说明在第3.1节中呈现的规则3.3（IF-SEQdistrib）的证明的两个初始步骤中使用的法则2.1（SEQ-SKIP单元）、2.9（SEQ-IF分布）和2.11（SEQ-IF右分布）的实现。在本文的其余部分，代码的行数是出于教学目的而编号的。%78A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-1模块OCCAM-LAWS{2导入{3保护（BASE）}4签名{5 opSEQ：列出进程->进程{strat：（1 0）}6 op IF：列出进程->进程7 op条件：进程->表达式8 op进程：进程->进程9 opconditions：List Processes -> List Expressions 10 opprocesses：List Processes -> List Processes 11... }12公理{13 var Q，P：过程14 varL：列出过程15 varG：表达式16 varE：列出表达式17 varC：列出条件18 eq [seq-skip 1]：SEQ（P，SKIP）= P。19 eq [seq-skip2]：SEQ（SKIP，P）= P。20 eq [条件]：条件（GP）= G。21 eq [conditions1]：conditions（SKIP）= null。22等式[条件2]：条件（P）=条件（P）。23 eq [条件3]：条件（P， L）=条件（P），条件（L）. 24 eq [过程]：过程（G P）= P。25 eq [processes1]：processes（SKIP）= SKIP。26 eq [processes2]：processes（P）=process（P）。27 eq [processes3]：processes（P，L）=process（P），过程（L）。28当量[aux-seq-if-distribl]：G：P：Q = G SEQ（P，Q）。29eq [aux-seq-if-distrib2]：G，E：P，L：Q =（GSEQ（P，Q）），（E：L：Q）。30 eq [seq-if-distrib]：SEQ（IF(C) ，Q）= IF（条件（C）：过程（C）：Q）。31当量[aux-seq-if-r-distribl]：Q：G：P = G SEQ（Q，P）。32eq [aux-seq-if-r-distrib2]：Q：G，E：P，L =（G SEQ（Q， P）），（问：英：左）。33 eq [seq-if-right-distrib]：SEQ（Q，IF（C））= IF（Q：条件（C）：过程（C））} }。%第5行到第10行描述了实施Occam法。第18行和第19行表示法则2.1的实现（SEQ-SKIP单元），并捕捉到这样一个事实，即带有SKIP的进程P的顺序组合没有效果。 30号线实施法律2.9（SEQ-IF distrib）.该实现使用辅助函数、条件和过程来分别收集条件过程的列表C的条件和过程。这些职能的执行情况见第20至27行。使用“：：“操作符（第28和29行）将SEQ操作符分配到IF操作符上。 该运算符接收两个长度相同的列表（布尔表达式（G，E）和进程列表（P，L））和进程Q。它生成一个条件过程的列表，以ciSEQ（Pi，Q）的形式，其中reci（G，E）和Pi∈（P，L），1≤ i ≤ n，n = |G、E|为|P、L|. 同样，法律的实施2.11（SEQ-IF右分配）使用相同的辅助运算符和函数。拆分规则在RULES模块中实现。由于空间的重新-限制，在本文中，我们只显示主要方程的实现第3.3条（IF-SEQ distrib） 本规则实现中用到的几个辅助运算符和函数没有详细说明。模块RULES的完整描述见[23]。% 1模块规则{2导入{保护（OCCAM-LAWS）}3签名{. .}4公理{.. .eqgerIf（c（P，LP））=IF（cP，真SKIP），gerIf（c LP）。6等式gerIf（c P）=IF（cP， true跳过）。7 eq [IF-SEQ-distrib]：IF（b（VAR LV： SEQ（LP）），真A.L. Silva et al. / Electronic Notes in Theoretical Computer Science 95（2004）63-79SKIP）=VAR getV（1（b（LP）：SEQ（（getV（1（b（LP）：=b），（VARLV：SEQ（gerIf（getV（1（b（LP）LP）。八......} }个文件夹%第7行实现了规则3.3的主方程（IF-SEQ distrib）。的getV操作符用于创建新变量（规则3.3（IF-SEQ分布）描述中的变量c要执行此任务，操作员接收要创建的变量数量（在本例中为单个变量）以及与这些新变量相关的进程列表传递此列表的目的是标识哪些变量名已经被使用，以避免名称冲突。gerIF 运算符负责生成出现在规则3.3（IF-SEQdistrib）右侧的条件进程，格式为IF（c Pk，TRUE SKIP）。为此，操作符接收新变量（由getV生成）和进程列表P1，P2，...，PK。gerIf的实现在第5行和第6行中给出。5.2证明分裂规则为了保证约简策略的正确性，需要证明分裂规则。这些证明的机械化遵循类似于3.1节中所示的风格。因此，为了证明规则3.3（IF-SEQ distrib），我们从规则的右手边开始，通过连续应用已经实现的奥卡姆定律，我们推导出规则的左手边。下面，为了简明起见，我们举例说明在3.1节中描述的证明的两个初始步骤中所进行的归约。此外，我们只详细说明有关奥卡姆定律的应用减少。完成这些证明步骤所需的辅助程序没有详细说明。%1开始VAR c： SEQ（（c：= b），（VARx： SEQ（IF（c P1，trueSKIP），IF（c P2，真SKIP）。2apply .seq-if-distrib at（21 2 2）。3结果VAR c：SEQ（（c：= b），（VAR x：IF（conditions（c P1，true SKIP）：processes（c P1，trueSKIP）：IF（c P2，true SKIP）：Process 4.5结果VARc： SEQ（（c：= b），（VAR x：IF（cSEQ（P1， IF（cP2， trueSKIP））， trueSEQ（SKIP，IF（c P2，true SKIP）：应用过程 6.seq-if-right-distrib at（2 1 2 1 1 2）.七...8个结果VARc：SEQ（（c：= b），（VAR x：IF（c IF（cSEQ（P1，P2），trueSEQ（P1，SKIP）），真SEQ（SKIP，IF（cP2，真SKIP））））：过程9应用.seq-if-right-distribat（21 22 1 22）。十......11结果VARc：SEQ（（c：= b），（VAR x：IF（c IF（cSEQ（P1，P2），trueSEQ（P1，SKIP）），true IF（cSEQ（SKIP，P2），trueSEQ（SKIP，SKIP）：过程12应用. seq-skip 1在（2 1 2 1 1 2 1 2 2）处。13结果VARc：SEQ（（c：= b），（VAR