精化工具的开发与精化演算的应用

理论计算机科学电子笔记184（2007）63-80www.elsevier.com/locate/entcs程序的机械化改进Manuela Xavier1CentrodeInformm'aticaUniversidade Federal de Pernambuco巴西累西腓安娜·卡瓦尔康蒂2约克大学计算机科学系英国约克摘要精化是一个支持摩根精化演算应用的工具。它旨在支持初学者的教学和使用;它已经在使用中。我们在这里描述的扩展的细化支持的发展（可能递归）的程序在代数风格的细化演算已经采用的细化。关键词：形式化方法，精化演算，精化工具。1引言精化是一个支持计算机系统正确开发的概念。精化技术支持增量开发：在使用规范化和编程的统一符号的上下文中，规范在一系列步骤中被精化。一个精化关系，它模拟了正确性的保持，在精化的连续步骤之间保持，保证最终实现满足原始规范。回到[1]，莫里斯[15]和摩根[16]独立地工作在细化计算上。这里介绍的精化演算是基于摩根1由CNPq支助。电子邮件：max@cin.ufpe.br。2部分得到QinetiQ和英国皇家学会的支持电子邮件：Ana. cs.york.ac.uk。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.01564M. Xavier，A.Cavalcanti/Electronic Notes in Theoretical Computer Science 184（2007）63使用摩根的精化演算，我们可以以精确和一致的方式编写软件。然而，将其应用于任何规模的问题需要大量繁琐的谓词操作，这很容易产生错误。这种情况表明需要开发支持精化演算的工具。一个支持法律应用的工具可以让用户专注于开发的重要元素，避免单调的工作和可能的错误。因此，我们开发了一种用于精炼的教育工具--精炼。该工具的初始版本在[5]中介绍，但它几乎没有开发管理工具。此外，支持的语言不包括过程和递归。在本文中，我们提出了解决这些问题的新版本的Refine。摩根因此，在[6]中提出了一套新的精炼法。这些法律解决现有的困难，并允许一个代数approach递归程序的发展。它们是这里介绍的Refine实现的基础。文献[4，12，13，23，2，21]中引用的大多数精化工具都不能开发过程和递归，或者没有一个友好的界面供初学者使用。此外，他们都没有考虑[6]中提出的方法。在第2节中，我们简要地解释了精化微积分，以及我们考虑的过程和递归定律。第3节介绍了精化，第4节描述了程序和递归律的集成结果最后，在第5节中，我们总结了相关的和未来的工作。2精化演算精化演算由规范、设计和实现的统一语言以及精化定律组成它基于程序（规格说明、设计或简单的程序）之间的精化关系;这组定律决定了如何以代数方式生成精化使用这种技术的程序开发包括一遍又一遍的法律应用，直到最初的规范被转换为可执行的程序。在精化演算中，如果程序p2比程序p1好，我们写p1±p2。关系式±称为精化：我们说p2精化p1。改进的概念是基于用户的观点，并使用最弱的前提语义对于精化过程中的每一步，当前程序或当前程序的某些子程序都通过应用精化定律进行变换对于某些转换，会生成证明义务。如果证明义务能够被解除，那么生成程序的正确性就得到了保证。一个规范的形式为w：[pre，post]。它的先决条件（pre）描述了程序执行良好的初始状态。后置条件（postcondition）描述了满足前置条件时可以获得的最终状态。框架（w）列出了其值可以更改的变量的言以M. Xavier，A.Cavalcanti/Electronic Notes in Theoretical Computer Science 184（2007）6365定义前置条件和后置条件的是谓词演算。如果初始状态满足前置条件，那么框架中列出的变量可以修改，使最终状态满足后置条件。如果初始状态不满足前提条件，则无法预测结果。前提条件true可以省略。在后置条件中，下标为0的变量可以用来表示相应变量的初始值。作为一个例子，我们有规范x：[0≤x，x2 =x0]。前提条件表明程序具有定义良好的当x的值大于或等于0时， 后置条件indi-在程序执行结束时，从满足前提条件的状态开始，我们在变量x中有其初始值的平方根除了指定语句之外，摩根演算的语言还块构造也可用于声明局部变量和逻辑常量。变量块的形式为[varx：T·p]]，其中x是声明为T类型的新变量的名称，作用域限制为p。类似地，逻辑常数c在块[conc·p]中声明。逻辑常数是一个名称，可用于在开发过程中提及感兴趣的值。不同地，一个变量，一个逻辑常数不是代码，然后，在细化的某个时刻，它必须被删除。在[6]中，一个过程在blocktakehek keform[过程名称=^body·main]]。它引入了过程名和一个程序片段：过程体，可以声明参数。最后，我们有主程序，它可以调用过程。参数可以按值、按结果或按值-结果传递。带参数的过程有一个参数化命令作为主体，也就是说，过程中参数的声明与过程主体相关联，而不是与其名称相关联。参数化命令不是使用或作用于特定变量，而是通用的：它们需要应用于参数。结果程序的行为取决于这些参数。一个例子是这个程序，它增加了一个可用的值x使用一个param eterizedprocedureInc：[[p rocInc=^（valresn：N·n：=n+ 1）·Inc（x）]]。 过程体是一个参数化命令，定义一个参数n，由value-result传递，其值加1。主程序是对过程的调用，传递变量x作为参数，我们要增加它的值。过程块也可以声明递归过程，但在它们的开发中我们使用变量块。除了程序和主程序外，还提供了一个变体块分解器。我有一个表格[程序名=^body变量v是e·main]。该变量是终止的论证的一部分手术过程中。例2.1作为一个例子，我们考虑一个计算正数倒数的平方根的程序。我们采用x：[00作为参数，我们通过参数窗口如图7所示。 结果如下。如果x=0-> f：[V=xx=0，f=fat（ x ） ][]x>0-> f ： [V=xx>0 ，f=fat（x）]fi在第一个规范的细化中，我们应用赋值律来实现递归的基本情况;得到的程序是f：=1。为了开发大于0的数字的阶乘计算，我们应用Next Assignment定律将上面的第二个规范再次划分为两个开发流程：第一个将通过递归调用实现，其中x的值作为参数减少;第二个存储阶乘的临时值。结果如下。f：[V=xx>0，f*x =fat（x）];f：=f*x分析上面的具体说明，我们可以观察到它要求f乘以x的最终值是x的阶乘。因此，f的值必须是x-1的阶乘，这可以通过递归调用来计算。递归调用的引入是基于与过程的初始规范相似的程序的出现，但减少了变量。因此，不能引入导致非终止的递归调用我们将上面的规范转换为一个类似于事实的初始规范的程序，变量被减少。然后，我们应用加强后置条件和弱化前置条件律，分别以（f=fat（x））[x，x0\x-1，x 0 -1]和（0 = xxV&）[x\x-1]为自变量，得到了相应的结果.这导致以下规格。f：[（0 =x&x V）[x\x-1]，（f=fat（x））[x，x0\x-1，x0-1]]上述规范具有适用于价值召唤法的适当格式。结果，我们得到了下面的代码片段。M. Xavier，A.Cavalcanti/Electronic Notes in Theoretical Computer Science 184（2007）6375见图8。 代码收集（valx@f：[0 =xx V，f=fat（x）]）（x-1）再次收集代码，我们可以观察程序的当前状态，如图8所示。现在，我们可以选择整个变量块并应用递归调用引入（带参数）法则。为执行该法律，Refinecar采取了以下步骤：(i) 它验证所选程序是否是变体块;(ii) 它验证过程主体是否是参数化命令;(iii) 它从过程体中提取出参数化命令应用程序的所有占用(iv) 对于找到的每个参数化命令应用程序(a) 它验证它的主体是否是一个具体的陈述;(b) 它验证前提条件是否是谓词：0≤（变量表达式）（变量名称）<(c) 它验证过程名作用域和变量作用域（如例4.1所述）。76M. Xavier，A.Cavalcanti/Electronic Notes in Theoretical Computer Science 184（2007）63见图9。 析因代码与证明义务(d) 如果没有问题，Refine在变量块的开发中搜索过程主体中的指定的出现，该过程主体与参数化命令主体中的指定完全相同，除了前提条件0≤（变量表达式）（变量名称）被替换

下载后可阅读完整内容，剩余1页未读，立即下载