C理论计算机科学电子笔记137（2005）67-92www.elsevier.com/locate/entcs一个流产范式Moshe Deutsch1 Martin C.亨森2埃塞克斯大学计算机科学系Wivenhoe Park，科尔切斯特，埃塞克斯，英国，CO4 3SQ摘要本文开始了一个新的调查，补充了我们以前的调查，其语义是由部分关系（使用Z作为这种语义的语言载体）给出的规范的精化。它围绕着扩展我们的数学设备，以便继续我们的追求，在数学上检验提升-整体化语义的本质（它是Z中精化的事实上的标准概念的基础）和语义元素在模型论精化中的作用，但这一次是在流产的范式中。 我们考虑了操作-精化的更简单的框架，因此（至少在这个阶段）从涉及数据模拟时出现的复杂性中抽象出来：我们通过引入一个更简单的规范理论（SP-精化）来检查这个体系中操作-精化的（事实上的）标准解释，SP-精化直接在语言中并根据前提和后置条件的自然属性来捕获激发条件精化的概念;然后我们总结我们的观察，并将它们与Z中每个可能的极端规范在流产范式中扮演的特定角色联系起来-这为将来在这个范式中更复杂的数据精化最后，我们提供了一个详细的说明，未来的工作概括Miarka，Boiten和德里克的工作相结合的流产和混乱的在我们的数学框架ZC和Z中。保留字：操作细化，规范语言，规范逻辑。1介绍逐步细化的概念构成了对软件领域广为人知的转换软件过程模型1电子邮件：mdeuts@essex.ac.uk2电子邮件：hensm@essex.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.02568M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）67工程学文献。它体现了管理大型软件系统开发过程中出现的巨大复杂性所采用的最重要的策略：软件组件的分离和正交性，以便以系统的方式构建开发，从而更容易为人类消费。其思想是将软件生命周期的设计阶段分解为许多更简单的（因此也是可管理的）步骤，每个步骤将一定抽象级别的系统描述转换为更具体的描述;最后一步将具体的系统描述转换为计算机程序。这些转换中的每一个都由精化规则来验证;这首先确保了过程是渐进的（每个步骤都包括正在开发的系统中的一些更多的设计决策），其次，在开发过程中保持正确性操作细化涉及从给定的抽象操作导出更具体的操作，而不改变其底层状态空间的表示。[3]这实际上是数据细化的退化情况，其中数据模拟是恒等函数。Z是一种基于状态的形式主义，它基于底层的部分关系语义，其中（操作的）规范表示一组绑定，这些绑定可以被解释为输入子绑定和输出子绑定之间的部分关系（参见，例如，[25]和[40，10，37]关于Z逻辑和语义的说明）。 不像其他形式主义，如B[1]和VDM [30]，Z的（标准）语言定义不提供任何细化说明。因此，考虑到Z的流行和在开发过程中加入精化的兴趣越来越大，全面理解Z中精化的基础（以及实用）方面是非常重要的。注意，在基于状态的形式主义的世界中，有两种主要的范式用于部分规范的精化;我们称之为混沌范式和流产范式。前者代表一种更具连续性的观点，即先决条件可能在细化过程中被削弱，而后者代表一种更具并发性的观点，即先决条件在细化过程中保持固定。事实上，我们在以前的工作中（例如， [16，14，13，15，12]），集中于混沌范式中操作细化和数据细化的基础研究。 （事实上的）改进标准方法在这种范式中是一种模型理论范式，其中规范（部分关系）都是完整的（使之成为整体）和扩展的（通过额外的语义值，通常称为底部和书面值）;这种语义通常被称为混沌提升整体化。 我们研究了（同上）。）因此，它通常被称为算法/算法改进或算法设计。M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6769这一语义的本质，并精确地解释了在这一范式中模型论修正中的数值的数学（以及概念）作用。在本文中，我们开始了一个新的研究，它补充了我们以前的工作：我们将扩展我们的数学工具，以便在失败的范式中建立一个操作-细化的研究。因此，我们将开始对一般的精化条件，特别是对这种范式中精化的（事实上的）标准（模型论的）解释进行一些阐述这种解释是基于一种独特的提升-累加语义，这种语义表现在它对底层操作前提条件之外的所有初始值施加的严格性上，相对于区别值λ。我们将开始从根本上阐述这种设置的关键性，以获得一个可接受的模型论的点火条件细化概念，以及λ值在其中所起的关键作用，事实上，我们将看到，λ在这种范式中的数学作用与λ在混沌范式中的数学作用完全不同。我们从修改与Z的部分关系语义相关的各种概念开始我们的追求，并考虑到这个语义来细化规范（第2节）。然后，我们继续定义操作细化的两个基本理论，每个理论都抓住了触发条件细化的一个特定方面（第3节）。 它们是：一个以明显的数学方式捕捉精化中所期望的性质的理论（3.1节）--这是一个纯粹的证明论概念，被用作我们确定在流产范式中任何其他操作-精化概念的有效性的基准;以及一个捕捉标准模型论解释的理论，在这个范式中，它基于流产-提升-总体化语义（3.2节）。然后，我们证明这两个精化理论是等价的（第4节）。在第5节中，我们总结了我们从理论之间的比较观察;特别是，我们强调的关键作用，以及独特的方式，它们与完成，在充实的等价性结果在第4节。然后，我们将这些观察结果与Z中每个可能的极端规范在流产范式中所起的特殊作用联系起来;这种分析不仅非常具有启发性，而且还为我们将来的工作铺平了道路，将其推广到流产范式中更复杂的数据细化最后，在第6节中，我们提供了一个详细的说明，额外的有趣的未来工作，将调查一些概括的Miarka的（等。）框架[32]，用于结合两种流产和混乱的范式进行细化。我们修改这个框架，强调在其中的作用，并讨论（鉴于我们目前和以前的分析）是否一个新的，70M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）67CJJ与语义元素不同的语义元素，对于捕捉其中操作细化和数据细化的模型理论特征至关重要。这样的调查成为可能凭借ZC，逻辑为Z报道，例如。 [25]，和一个简单的 保守扩展Z，报道在例如 [16]，它将非线性项纳入Z C的类型中。我们总结这一点，以及其他符号约定，见附录A。[4]我们采用了一种新颖的技术，将所有的精化理论都呈现为一种证明论的形式：作为一组引入和排除规则。这导致了一个统一的和简单的方法证明的各种结果在续集。因此，它与[9]中采用的更多基于语义的技术形成对比。2Z的部分关系语义在这第一节中，我们将介绍作为我们研究基础的基本数学和概念场景。在这个过程中，我们将修改一点Z逻辑，解决一些符号约定;更多的细节可以在附录A中找到。2.1模式模式符号构成了Z最容易识别的特征（部分原因是它的半图形形式），而且它确实在语言中占据了中心位置，不仅是构建数学文本的一种手段，用于严格描述系统的性质，也用于描述整个系统本身。在[25]中，Z模式，特别是操作模式，被形式化为绑定集。这捕获了文献中的非正式描述（例如[19]，[40]），其中操作模式可以被理解为状态之间的关系：从未启动状态（表示操作“之前”的状态）到启动状态（表示操作“之后”的状态）的转换关系在本文中，我们将使用元变量U（带有装饰）来覆盖操作模式。例如，考虑指定前置操作的操作模式（水平书写）：Pred=^[x，x]：N|x>0<$xJ=x−1]Pred具有类型P [x：N，xJ：N]，并且被理解为模式类型[x：N，x：N]的绑定的集合。 绑定|x$n，x$m| n，其中n> 0，4 这只是为了方便起见，读者可能希望查阅[25]，[28]和[16]关于我们的符号和元符号约定的更多细节。M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6771JDFDFDFXDF都是Pred的元素事实上，在这种情况下没有其他因素。回想一下，未标记的标签（如x）被理解为对操作发生之前的状态，而primed标签（如x）是对国家的事后观察。每个操作模式U将具有形式为PT的类型，其中T是模式类型。此外，类型T总是可以被划分为它的输入（或之前）类型的（兼容）并集T in，其输出（或之后）类型T outJ。 也就是说，T = T inY T outJ。为J模式Pred，我们有Tin=[x：N]和Tout=[J：N]。 本文在分析了现有文献的基础上，由于我们只处理操作细化，我们可以假设所有J操作模式具有类型PT，其中T=dfTinYTout。出于这种位置，我们可以省略类型上标在大多数地方的续集。2.2先决条件Z采用逻辑（即也就是说，作为一个单谓词框架，Z中的前提条件是隐式的，可以通过定义谓词关于其所有后观测的存在闭包来计算我们可以形式化操作模式的前提条件的概念（关系的域，在之前和之后的状态之间，模式表示）来表达所涉及的条件：定义2.1LetT in≤V。PreUxV=<$z∈U·x=. z请注意，如果V恰好是Tin，则上述定义不超过：z·x*zJ∈U当推理前状态变量的前提条件-状态5时，这显著地促进了分析（与在更大的模式类型上的变量相反）。下面的引入和消除规则对于前提条件是可直接推导的：6提议2.2t0∈Ut0=.前U t1t1（前+）PreUty∈U，y=.Pt P（Pre−）5.变量是否在所讨论的规范的前提条件[6]为了后面的方便，我们把前提条件的概念作为谓词引入。在Z语言中，前提条件构成了一个状态模式，它由所讨论的操作的所有有效的前状态（绑定）组成。这在必要时很容易被捕获，因为：{zTin | Pre U z}.72M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）67通常的边条件适用于本征变量y。Q显然，Pred的前提条件不是（并且对于操作模式，通常不会是）[x：N]的整体（通常，Tin）。在这个意义上，操作模式表示部分关系。实际上，Pred是一个部分操作，因为它覆盖所有自然数（它的before类型），但只定义为那些大于零的自然数（它的域）;也就是说，它没有指定行为：⟨|x $0，xJ$m| ⟩对任意m∈N。更确切地说，当在其前提条件应用操作时，它对操作的结果保持沉默。2.3前提条件之外会发生什么上面提出了一个直接的问题：在其前提条件之外，允许什么行为来正确实现（操作的）（部分）规范？为了回答这个问题，我们需要一种细化理论：一种将这样的实现与这样的规范进行比较的方法。对这个问题的一般回答是基于完全正确性改进。也就是说，细化是基于随后的总体关系语义，称为提升总体化。这一解释是Z中修饰的语义基础。它的建模方法是，首先，用一个代表某些不受欢迎的行为的特殊（语义）元素（通常称为“底部”）扩展（即提升）所讨论的操作的源集和共域在基于状态的规范的世界中，有两种著名的基本上不同的规范用于部分规范的精化，其中每一种规范都在精化之下引入了不同的提升-总体化语义。这导致了两个不同的精炼概念，每一个都基于对上述问题的不同回答第一种是混沌范式，有时也被称为契约方法[32][10，ch.2-3];这代表了一种更顺序的观点，因此，是Z中对细化的标准解释的基础。在这种范式中，前提被认为是建立后置条件的最小条件（即它们可能在精化过程中被削弱），因此对上述问题的回答是：在操作的前提之外，任何事情都可能发生。也就是说，操作在其前提条件内应用时表现为指定的行为，而在其前提条件外应用时可能会产生任何任意结果，包括不受欢迎的行为;这通常被称为M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6773[36、32]。在以前的工作中（在第1节中引用），我们彻底检查了这种范式中的操作-细化和数据-细化的模型，其中我们的数学基础使我们能够以一种不可能的方式对这些模型进行外科手术式的仔细检查。事实上，我们解决了许多非正式和半正式的解释在试图确定混沌提升整体化语义学的本质时遇到的各种困难，特别是在模型论细化中，混沌元素的作用精化的第二种范式是流产的范式，有时也称为行为[10]或阻塞[32]方法（在[21]中，这是Grundy有效地表示为部分模型的方法）;这代表了一种更并发的观点：它让人想起进程代数中的“拒绝”或“死锁”概念，因此，它通常在基于状态的形式主义与进程代数相结合时使用（例如：[20]，[4]和[10，ch.18-19]）。在这种范式中，先决条件被认为是守卫[32，10]或触发条件[31，36]（即它们是触发/固定条件-在细化过程中不会被削弱）7，因此上述问题的答案是：在操作的先决条件之外没有任何事情更准确地说，当在其前提条件内应用时，操作的行为与指定的一样，并且在其前提条件外被阻止：它不能在其前提条件外应用，如果是，它将只会导致不受欢迎的行为。本文的大部分内容致力于研究流产范式中操作-细化的基本概念。这个相当简单的框架使我们能够从涉及数据模拟时产生的复杂性中抽象出来，因此，至少可以开始推理这个范式中数值的数学作用（以及与它们在混沌范式中的作用相比）。3细化的基本分析自然地，Z中操作模式的部分关系语义提出了一个直接的问题：在流产范式中，一个操作模式精炼另一个操作模式意味着什么？更一般地说，我们在问：在这个范式中，一个局部关系精炼另一个局部关系意味我们通过引入两个不同的操作概念来开始我们的分析-基于对上述问题的两个不同答案的细化。然后，我们继续分析它们之间的关系，这对它们两者都有了新的认识，特别是对标准（模型论）[7]自然，它们也不会被加强，以便不违反细化的原则（见[9]，[10]，[16]和[13]）;因此，它们在细化的过程中显然是固定的。74M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6711SP−概念在这个范例中，基于中止-提升-总体语义。3.1SP-Refinement我们的第一个理论是SP-细化，即在失败范式中操作-细化的规范理论SP-精化是一个纯粹的证明理论特征，它作为一个基准，用于确定该范式中任何其他操作-精化概念的有效性这一概念基于人们在一个触发条件细化中所期望的三个基本属性：首先，细化保证前提条件不被加强;其次，细化保证后置条件不被削弱;最后，细化保证前提条件不被削弱。注意，前两个属性是精化中的标准属性，因此SP-精化可能涉及非确定性的减少（因此，它确实是S-精化的特殊情况，混沌范式中操作-精化的规范表征-参见[16]的3.2节关于其定义）;然而，第一个和最后一个属性在精化过程中强加了定义域（即前提条件）的稳定性（因此是SP细化可以通过强制细化关系在这些条件适用时恰好成立来捕获。经上所记U0±spU1，由以下ZC定义给出：定义3.1U0±spU1=df（Δz·Pre U1zΔPre U0z）Δ（<$z0，z1·z0*zJ∈U0<$z0*zJ∈U1）1 1以下引入和消除规则可用于SP细化：命题3.2设z，z0，z1是新变量.前U1z<$前U0z z0*zJ∈U0 <$z 0*zJ∈U1+1U0±sp U1sp）U0±sp U1Pre U1 t−（U0±sp U1t0*tJ∈U0（± ）前U0tQ±sp0）t0*tJ∈U1SP1注意，与S-加细相反，在SP-加细（±+）的引入规则中，后置条件前提的先行项中没有合取词Pre U1z0这种结合正是区分（±1M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6775SPCFig. 1.一个例子：前一个操作的失败-提升-累加。S-精化和SP-精化：（± +）的两个前提共同保证了前提条件在精化过程中保持固定。因此，上述两个消元规则为再融资建立了必要条件与之不同的是，它与S-细化（S-细化）类似。−（±sp0）保证前提条件不会加强，而不是−S-加细，（±sp1）保证后置条件和前置条件不要削弱。这种证明论的表述使我们能够把SP-精化看作是在失败的范式中操作-精化的规范表征：这是我们对精化的处方，而另一个理论是可以接受的，只要它至少对于SP-精化是合理的，因为（正如我们将在第4节中看到的）合理性必然意味着它必须满足上述SP-精化的两个必要条件;另一方面，完备性意味着另一个理论至少认可SP-精化所做的事情，即加强后置条件。3.2WQ-精炼在本节中，我们提供了在流产范式中操作-细化的（事实上的）标准（模型理论）概念的基础上的正式技术发展。类似于我们所有的基于模型的理论，这发生在我们的扩展的Z理论中。我们首先在数学框架中表达，意图是-在文献中讨论的流产-提升-总体语义（例如[4]，[10，第3章]和[3]）。将此语义应用于操作的示例QPred（在我们的命名法中写作Pred）如图1所示。 召回（从例如[16]），混沌提升总体语义不区分在其前提条件之外应用操作所导致的任意和不受欢迎的行为：任何事情都可能在操作的前提条件之外发生;这可能包括不受欢迎的行为以及可能[8]这种有效性的衡量在对数据细化的概括中表现得更为明显（见例如， [11]）。76M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）671111+1 1+1⊥110结果的“分歧”。然而，在失败的范例中，没有这样的自由：一个操作被阻塞在它的前提条件之外;因此，在以下定义中，“块”符号用于表示一组绑定的失败-提升-总计：9Q定义3.3U=DF{z0 * zJ∈ T|z0* zJ∈U<$（<$Pre Uz0{\fn方正黑体简体\fs18\b1\bord1\shad1\3cH2F2F2F}{\fnarialblack\fs12\bord1\shad1\4cH00000\b0}请注意，这个定义显式地部署了textvalue，以捕获阻塞解释。这表明（虽然在这个阶段，相当肤浅地），在这个范式中的数学角色与在混沌范式中的数学角色不同;事实上，Boiten和de Roever [3]提到，在此上下文中，将其作为表示“deadlock”的元素。我们将在第5节中进一步详细讨论这一问题。下面的引入和消除规则是可导出的流产提升-总计集：提案3.4t0*tJ∈U（Q）t0*tJ∈T<$Pre U t0tJ=J（Q）不 *tJ∈Q0t* tJ∈Q101UJQJ01UJ J不 *tJ∈Qt0*t1∈ Ut0*t1∈U <$P<$Pre U t0，t1= U P（−01U（Q−）PQ）Qt0*tJ∈T<$1下面的附加规则是可导出的流产提升总计集：引理3.5Q·（i）Q（二）<$Pre U t t∈TinQ（三）U 简体中文∈Ut*<$J∈U不 *tJ∈QPre Utt*tJ∈QtJ/=<$J01U0（iv）t0*tJ∈U01U1（v）t0*tJ∈UJQt0*tJ∈T<$Pre U t0<$tJ/=<$J<$t0*tJ∈UM. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6777t0*t1∈Ut0=U第11条第（七）款tJ=10J不 *tJ∈Q101UQ9为了便于标记，我们将集合Tin*Tout'写成T（注意*用于⊥ ⊥集合，与用于类型的Y78M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）67引理3.5（i）至（vi）表明，定义3.3与文献中描述的意图一致（体现在图1中）。1）：㈠至㈣证明失败的完成包含在混乱的完成中（写·U在我们的命名法中-参见例如[16]的第3.3节对其定义），区别值存在于完成中，并且前提条件之外的一切都被映射到它上，其中基础关系中的所有状态在完成中保持不变;（v）和（vi）一起表示基础关系的前提条件之外的所有初始值相对于完成中的初始化的严格性此外，注意定义3.3可以用蕴涵（以显而易见的方式）而不是析取来表达：引理3.5（vii）构成了引入规则，对于流产-提升-总计，基于蕴涵引入。有了这一点，我们就可以很容易地在抽象范式中定义精炼的标准概念。我们将其命名为WQ-re f nement;它被写为U0±wQ U1，定义如下：Q Q定义3.6U0±wQ U1=dfU0U1明显的引入和消除规则遵循这个定义。4两个等价理论在本节中，我们将证明我们的两个细化理论是等价的。这种分析将帮助我们开始阐明在模型论的修正中，在失败的范式中，这些在方法论上，我们将表明，一种理论中的所有细化判断都包含在另一种理论所认可的细化之中。这样的结果总是可以在理论上得到证明，因为我们甚至已经将我们的模型论方法表达为理论（引入和消除规则的集合）。具体地说，我们将证明一个理论T0的精化关系满足另一个理论T1精化的消去规则（或规则）。由于一个理论的消去定则和引入定则具有通常的对称性质，这足以证明所有的T0-精化也是T1-精化。等价性可以通过互换上述T0和T1我们首先证明WQ-精化满足两个SP-精化消去规则。第一，保证unfinedness不增加的规则。命题4.1下面的规则是可推导的：M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6779⊥⊥1111SP证明U0±wQ U1PreU1tPre U0tδ。.t*J∈UJQ（二）（L.B.4）U前1 t前U1t（二）t*n ∈U1假假假 （二）U前0其中δ代表以下分支：（1）U前1t（3）t*y∈U1t*yJ∈T t∈Tt∈Tin前U0 （1）Qt∈Tin（三）（L. （第3.5㈢段）U0±wQU 1t*J∈UJQt*n ∈U1Q现在转向保证非增广的SP-消除规则既有确定性，又有非确定性。命题4.2下面的规则是可推导的：JU0±wQ U1t0*t∈U0证明t0*tJ∈U1J JJ（1）t0*t1∈U0Qt0*t1∈U0t1= 0t*J ∈UU0±wQU1t0*tJ∈UJQ（1）0假J0（L. B.4）t0*t1∈U1t0*t1∈U1（1）t0*tJ∈U1Q下面的定理可以直接由命题4.1导出和4.2，除了规则（±+）：10[10]通过引入规则和消去规则之间的结构对称性，这类定理的证明总是自动的。因此，我们将不明确地提供它们。10080M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）671110SP1 01011文勤0定理4.3QU0±wQU1U0±sp U1我们现在证明SP-精化满足WQ-消去规则。命题4.4下面的规则是可推导的：U0±spQU1t0*tJ∈U0Q证明t0*tJ∈U1U±U t*tJ∈Ut0*tJ∈U1（一）δ。.jQ jQ jQt0*t1∈U0t0*t1∈U1t0*t1∈U1（1）JQt0*t1∈U1其中δ代表以下分支：QJU±U前U t（一）t0*t1∈U00SP1 0 0（一）t*tJ∈Ts使用前J1t0QtJ=0t0*t1∈U1Q然后，由（±+），从命题i-第4.4条：定理4.5QU0±spU1U0±wQ U1定理4.3和4.5一起证明了SP-加细和WQ-加细理论是等价的。 注意，与混沌范式对应结果不同（证实W·-refinement 11和S-细化-见例如 [16]的第4.2节），其中明确地使用“”是至关重要的只是为了保证前提条件不会加强，明确使用这是建立所有三个结果的关键：两个结果（命题4.1 和4.2）的可靠性定理4.3和结果（命题[11]在我们的命名法中，W·-细化是混沌范式中操作细化的（事实上的）标准（模型论）概念--参见[16]的3.3节。M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）67814.4）的基础上的完整性定理4.5。我们将在下一节中进一步阐述这一观点。5讨论在本文中，我们对失败范式中的操作细化进行了最重要的基础分析我们已经发展了两种精化理论，每一种都构成了混沌范式中相应理论的专门化（例如，参见[16]的第3节），它坚持了激发条件精化的概念。这种范式中的标准解释是一种模型论的解释;它基于一种特殊的提升的总体化概念，在这种概念中，在基本运算的前提条件之外的所有初始值都严格地相对于在完成时被忽略的特殊值。SP-精化属于我们的精化理论的证明论家族。再次，它充当了流产范式中操作-精炼的规范性表征，因为它以一种明显的数学方式，直接地，在语言中，就所涉及的谓词而言，捕捉了激发条件精炼背后的意图：它不涉及辅助语义学的引入，也不涉及辅助元素的引入。我们已经证明，通过将这种方法建立为一种理论（而不是充分条件），我们可以获得一个等价的框架，在这个框架中，带有辅助语义元素的模型扩展对于形式化激发条件细化的概念是不必要的。我们再一次证明，看起来不同的具体化和细化模型实际上是密切相关的。然而，由于被限定为仅仅是操作-细化，这种分析帮助我们仅仅开始解释为什么在这个范式中作为细化的标准特征的流产-提升-总和被以它本来的方式定义（即，坚持关于区别值的严格性）的一些数学原因，以及在发射条件细化的上下文中，这些事实上，在概念上，类似于混沌范式，它代表了一些不受欢迎的行为，但它的数学作用显然与混沌范式不同。这种区别在命题4.1、4.2和4.4的证明中就表现得很清楚：很明显，所有这些证明的完成，不仅取决于明确地使用预值，而且取决于前提条件之外的所有初始值相对于预值的严格性;回想一下，与此相反，在混沌范式中明确地使用预值，只是为了证实标准的精化说明保证了前提条件不会加强，才是至关重要的。 命题4.1182M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）67（16）。这表明，在这种范式中，区别值以及它们与完成的相互作用方式（反之亦然）对于正确捕捉模型论精炼背后的保护解释是绝对重要的，并且似乎没有其他方法可以在关系完成中对拒绝进行建模（即不使用非线性值）。12像往常一样，我们可以通过考虑流产范式中的极端具体化的想法来强调这一点（或者至少开始强调它）。[13]类似于混沌范式，“真”这个具体化表示对行为的明确许可。在一个触发条件精化中唯一被认可的属性是非确定性的归约;因此，由于True是最非确定性的具体化，任何减少这种行为的具体化都构成了它的精化。现在回想一下，True是一个完全的规范。一个数学事实是，当基本规范是总和时，我们所掌握的所有关系完备化模型都是的基础。这一点的证明非常简单：我们在[16]的第6节中建立了严格和非严格混沌提升总体化模型是等价的细化理论的基础;[14]此外，很明显，当基本规范是总体时，严格混沌提升总体化和失败提升总体化模型是等价的，在这种情况下，两种范式中的细化都相当于一个激发条件细化，以防止欠定性的增强。然而，混沌这个具体化的概念，在这个流产的范式中，却代表着完全不同的东西回想一下，在混沌范式中，混沌表示行为的隐含许可，因此，任何规范都可以对其进行细化（参见[16]的第4.4节）。当然，这与这样一个事实相吻合，即在这种范式中，任何行动的前提条件之外都可能发生任何事情。另一方面，在中止范式中，任何操作在其前提条件之外中止，从而阻止了在细化的上下文中从该结果恢复的任何可能性（正如我们在第4节中所看到的，为了获得可接受的模型论概念，这种设置似乎是不可避免的，即细化条件）。 既然一切都在[12]这与混沌范式相反，在混沌范式中，我们建立了一个基于关系完成模型的操作细化的模型理论特征，总体化，但没有提升;我们证明了这种表征捕捉了在该范式中的细化中预期的（必要和认可的）属性。 尽管如此，这一提法的代价是，必须依赖对先决条件概念的另一种解释（详情见[16]第5节）。[13]参见附录A，了解我们的命名法中两个极端的规范真和混沌的定义（定义A.4）。[14]同上书中的严格混沌提升总体语义（在我们的数学框架中）捕捉了[7]中描述的非正式意图：底层关系的前提条件之外的发散性和严格性（即源集合中的严格性仅映射到其共域对应物）。M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6783图二.一个例子：规范Chaos代表了流产范式中的隐式死锁。Chaos，它在这里隐含地表示一种情况，在这种情况下，一切都被阻塞，即隐式死锁;这种情况由Roscoe [35，ch.0]定义如下：“如果没有组件可以取得任何进展，则并发系统是死锁的。“.事实上，在一个激发的精炼条件下，混沌不能精炼任何东西（当然，为了防止先决条件加强，这是自然的），但实际上，在这个制度中也没有什么Q因此，我们称之为流产-提升-总体化混沌（abortice-lifted-totalised chaos）。混乱）作为僵局，不可能从中恢复;这在图2中示出。在[3]中，Boiten和de Roever提到了死锁（在流产范式的上下文中）作为代表“死锁”的元素。由于前面讨论过的原因，我们更愿意遵循并发形式主义文献的路线（例如[ 35 ]），并参考情况（即，提升的总体化规范）作为死锁，并将其作为流产元素，显然在防止从这种情况下进行非严格恢复方面起着至关重要的作用。这样，我们仍然证明了在[3]中讨论过的直觉。 实际上，我们将在今后的工作中- 在对基于模拟的数据细化的概括中，加强了我们关于在失败范例中的模拟的作用的结论（和术语），以及在获得有效的前向模拟和有用的后向模拟模型理论特征的点火条件细化中，操作的完成和数据模拟的提升的严格性的重要性。 类似于混沌范式中的数据精化分析（例如[13，15，12]），当允许非平凡一个特别有趣的启示是，在混沌和流产范式中，流产-提升-总体化语义可以作为正向模拟细化的标准概念的基础，其中实际范式仅取决于数据模拟提升的方式。15[15]大部分分析报告见[11]。84M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）676未来和相关工作：Miarka，Boiten和Derrick6.1意图、直觉和动机在[32]中，Miarka等人开发了一个框架，该框架结合了两个失败和混乱的范式进行改进。该框架允许在同一账户中同时表示拒绝和未充分指定。作者他们从一个简单的，但非常直观的例子来说明这一点。 这个例子是通过一个Z规范来建模一个简单的货币交易系统：银行是一个状态模式，它通过（唯一的）帐号和整数之间的部分函数来指定银行帐户的存储库，每个帐号代表它所致力于的帐户的余额Transfer是Bank上的一种操作模式，它具体地将给定帐户的余额增加给定值;transfer的前提条件包括两个谓词：一个保证给定帐户存在于存储库中，另一个保证给定值（将添加到余额中）不是负数，因此该操作的结果是不能提取资金。然后，他们证明，没有混乱和流产characterisations提供了一个足够的解决方案（操作）完善这个系统。混沌范式中的细化过于宽容：它允许一种明智的方法，即在给定的账号在存储库中不存在的情况下，用一个新的银行账户（其余额是给定的值）扩展存储库;然而，它也允许取款的危险情况（这两种情况都是削弱先决条件的自然结果）。相反，在流产范式中的细化限制性太强：它防止了取款的危险情况，但也防止了用新帐户扩展存储库的明智情况这些范式中没有一个范式提供了完善这个操作的令人满意的解决方案，原因在于，显然，在其前提条件中的两个谓词具有不同的作用：坚持附加值不是负数的谓词更像是一个守卫，而坚持给定帐户已经存在的谓词更像是一个前提。事实上，作者[16]事实上，我们在[18]中提出了精化的另一个特征（SC-精化），其中前提条件可能减弱，但后置条件保持固定。M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）6785不可能（警卫）未定义（Guard<$Pre）定义（前警卫）图三. 组合范式中操作行为的可能区域，以供细化。某些操作模式，从那些形成的先决条件。通过这种方式，它们在同一规范启用了守卫和先决条件。总的来说，在这个框架中，一个在其保护的操作表现得像在流产范式中一样：它被阻塞，不管它的前提条件是否成立;而在其保护之，操作表现得像在混沌范式中一样：结果取决于前提条件是否成立（像往常一样，任何事情都可能在前提条件之外发生他们实现这一思想的方式是将操作模式视为由一对模式组成：第一个是“使能”模式，表示守卫，而第二个重要的是要注意，这仅仅是将保护与操作模式的谓词显式分离的一种装饰性方式：自然地，“启用”模式的签名与“检查”模式的签名相同或包含在其中;因此，当在模式表达式中需要时，操作被简单地视为这两个这样，模式计算操作就不需要任何更改话虽如此，一个操作被赋予了一个非标准的解释，基于三值逻辑，它明确地给出了图中描绘的操作行为的三个区域的表现 3：当守卫和前提条件都成立时，操作被定义（这个区域由true表示）;操作是不可能的（即， blocked）当保护不成立时（这个区域用false表示）;当保护成立，但前提条件不成立时，操作被定义（这是一种“不关心”的情况，在这种情况下任何事情都可能发生，因此它由第三个逻辑值表示，它精确地体现了这种解释）。然后，作者根据这三个区域定义了操作-精炼的（充分条件）特征，由此，后条件可以加强，前提条件可以减弱，守卫可以加强。 尽管如此，重要的是要注意，“前提条件是加强防护的上限，防护是加强防护的下限，86M. Deutsch，M.C.Henson/Electronic Notes in Theoretical Computer Science 137（2005）67”[ 32 ]这是一种“以弱胜强”的说法换句话说：回到图3，定义区域可以被扩大，但不能超出不可能区域在我们的数学框架中捕捉这些想法将是非常有趣的。这样一种数学工具的扩展将强调三个突出的问题。我们将在其余的小节中详细讨论这些问题。6.2证明理论操作-细化首先，在我们基于经典逻辑的通常设置中，操作的三值逻辑解释对于以精炼的证明论表征的形式捕获[32]的意图似乎并不完全至关重要。当然，这里的关键问题是充分地捕捉先决条件和守卫之间的分离概念除了[32]中建议的方法之外一种方法是用两个谓词定义一个操作模式：一个构成守卫，另一个构成（通常的）Z后置条件;在某种意义上，这种方法让人想起[32]中的方法，只是这需要对模式calculus操作的定义进行一些修改。另一种方法是推广[26，27]中采用的方法，其中前置条件和后置条件在语法上是分开的，通过为守卫添加第三个无论哪种方式，研究这些方法的分支都是非常有趣的。6.3模型理论操作改进第二个问题（在[32]中没有涉及）涉及模型理论的精化。我们的推测（基于我们在过去四年中研究精化基础问题的整个项目中获得的经验）是W-精化，这是一个基于图1中描述的提升-总体化语义的第四，也是对[32]的理解。该组合提升累加语义基于附加语义元素“top ”T （
我的内容管理
展开
