Z轴提升：控制理论和实时规范中的一种特殊规范风格的研究与应用

197理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html23页Z轴提升安德鲁·马丁a和科林·菲奇b牛津大学软件工程中心，沃尔夫森大楼，公园路，Oxford，OX1 3QD，英国b软件验证研究中心，昆士兰大学，昆士兰4072，澳大利亚摘要像Z这样的形式符号为编写清晰的规范以及对这些规范的性质进行证明提供了强大的支持在本文中，我们将探索一种特殊的规范风格，并将其应用于控制理论和实时规范。 我们定义的符号允许准确的描述这些领域的概念，没有显着的开销或符号混乱。这个符号长期以来一直被这些领域的从业者使用;我们证明它可以在标准草案Z中定义，并且由此产生的规范可以证明。1介绍诸如Z之类的形式符号为编写清晰的规范以及对这些规范的性质进行证明提供了强大的支持。这种好处很大程度上来自于拥有丰富的预先定义的概念和类型的语言，以便规范既简洁又精确，而且易于访问。我们用Z写的所有东西也可以用经典的一阶谓词逻辑来写，但结果远不那么容易接近。在本文中，我们将探索一种特殊的规范风格，并将其应用于（至少）控制理论和实时规范。我们定义的提升运算符和符号长期以来一直被这些领域的我们证明，这些符号可以在标准草案Z [19]（以下简称“标准Z”）中进行正式定义，并且这样做是有用的将定义保持在Z范围内的价值在于，它使规范易于使用现有的Z工具进行分析。在这些和其他应用程序中，我们感兴趣的是将我们的描述从涉及简单数据类型的描述提升到使用这些数据类型的函数的描述。提升允许为简单类型定义的代数，例如2001年由ElsevierS cienceB. V. 操作访问和C CB Y-NC-ND许可证。马丁和菲奇198整数，应用于更复杂的类型，例如从实数到整数的函数。具体地说，在实时系统的规范[21]中，我们想写这样的表达式：速度20<这并不是说一个称为速度的恒定值不超过20，而是说在不同的时间t，可变速度所取的值永远不会超过20。也就是说，速度（t）<20.在本文中，T是时间值的集合，通常是实数R。提升的另一个例子出现在各种应用中使用多项式虽然多项式通常是在实域上开发的，但它们可以有效地在各种各样的基础系统上使用多项式的这种处理在控制理论中很流行，其中传递函数用于差分方程的解[4]。第4.2节给出了此类用途的示例2以前的举重方法在这一节中，我们回顾了前面描述的两种在Z中提升的方法，一种是显式提升函数，另一种是重载现有的Z运算符。2.1显式提升Duddy等人报道了许多与Z中的定时特性的具体化相关的工作。在关于提升的部分，他们强调，在描述连续时间历史的性质时，适当的函数算子集合对于编写可理解的规范是必不可少的因此，将实数的加法推广到实值（历史）函数的加法是合适的（f+Jg）（t）==f（t）+g（t），允许表达简洁的条件，例如h=f+Jg，而不是更冗长的t= f（t）+g（t）。它们继续描述代数（S，O）上的同态（即提升函数），对于S是数据对象的集合，O是马丁和菲奇199↑（maxSpeed−speed）↑↑↑→S上的运算符。对于任何定义域类型A，同态是代数（S↑A，O↑A），其中S被提升为定义域A的函数，对于O也是类似的：S↑A==A→SO↑A=={o：O·o↑A}o↑A==λf1， . ，fn：（A →S）·（λa：A·o（f1（a）， . ，fn（a）。因此，（+）T正是上面定义的运算符（+J）。将提升算子推广到表达式，可以证明在（S，O）的原始项代数中成立的定律也在（SA，OA）的项代数中成立（因此它是一个协变的hom-functor[15]）。这个运算符可以用来“提升”各种Z表达式和谓词。（后者是通过使用布尔值函数代替谓词来实现的为了处理未定义谓词的可能性，使用了部分函数逻辑。因为在Z中，操作符和值（分别是O和S的元素）之间没有语法上的区别，所以开发了一个精心设计的特殊情况集合来覆盖每一种可能性，并且实现并测试了由此产生的提升算法。因此，通过以下时变值和时不变常数的声明speed：T R最大速度：R表达式不不=（−）↑（maxSpeed，speed）=λt：T·（−）（maxSpeed，speed（t））=λ t：T·maxSpeed − speed（t）。请注意，标识符的声明类型决定了它们是否被索引。由于应用需要同时完成关于两个值的提升，提升算法进一步复杂化。在描述时间间隔时，我们不妨这样写：速度（α）≤速度以指定在整个间隔中速度的值永远不小于其初始值。这里α是一个区间函数，它返回区间开始时的时间（区间的最小因此，右边的表达随时间而变化，左边的表达随时间的间隔而变化。对于时间间隔的集合（即，T的连续子集的集合）写入TI，并且↑T，TI用于同时提升两次马丁和菲奇200的|−→不和间隔，我们有（speed（α）≤speed）↑T，TI= λ π：TI; t：T·speed（α（π））≤speed（t）。在这个例子中，我们还看到了一个变量如何以多种方式使用。在左边，速度在一个子表达式中被显式地解引用同样，提升算法在确定如何提升变量时必须考虑类型2.2无点Brien等人描述了一种算法较少的方法[6]，通过定义一族提升函数、算子和关系来实现类似的结果的定义类似于上面的（+J），但要注意尽可能避免在定义中使用点这一选择是由观察到量化器和lambda抽象倾向于使证明复杂化，并且引用函数而不提及其应用点的定义通常更容易使用。在这种方法中，大多数操作符都是重载的，如图1所示，改编自Brien等人的论文。请注意，与前面的方法一样，使用了布尔类型，因此关系是布尔值函数。该图说明了如何将实数上的关系（重新转换为布尔值函数）重新解释为实数时间函数上的关系（给出布尔值时间函数例如，可以在时域上提升变量v：R以创建跟踪变量v：T→R。当用一个表达式来解释时，如4≤vT，提升关系产生T→B型结果。这些函数可以通过考虑它们在开始和结束点的值（对于函数f，这些是'b'）而进一步提升为时间间隔的实值函数。F和E。f此外，常数可以比较任何一种功能，通过将它们转换成常数功能。类似地，谓词（布尔值函数）可以使用"“运算符提升到时间间隔在这种方法中，上面描述的同态定义如下[6]。给定一个集合S和一个函数或关系h，则hom-functor（S h）接受一个从S到h的定义域的函数，并返回一个从S到h的值域的函数。由于下面的模式中的量化函数f可能不是全的，定义要求集合S是f的定义域。[X，Y，Z]−→：PX×（Y→Z）→（X→Y）→（X→Z）f：X→<$Y;h：Y→<$Z·（domf−→h）f=h马丁和菲奇201→ × → →→[X，Y，Z]X→（Y×Z）：（X→Y）×（X→Z）→X→Y;g：X→Z;x：X·f（x）=（f（x），g（x））[X，Y，Z，W]（X×Z）→（Y×W）×：（X→Y）×（Z→W）→f：X→Y;g：Z→W;x：X;y：Z·（f×g）（x，y）=（f（x），g（y））TI →RTI→R≤，=≤，=TI →B的|T →BRB≤，=Fig. 1. 超载起重注意缺少点。 例如，假设运算符（+）是 对于（R×R）→R型的函数f，若给定T→（R×R）型的函数f，则（T−→（+））f是（T→（R×R））→（T→R）型的函数就其本身而言，这个定义并没有以我们想要的形式提供提升为了克服这个问题，定义了两个乘积函子（第一个在这里使用;第二个将在下面出现）：通过这种方式，可以在不参考点的情况下定义提升操作员（+J）[X] ==（X−→（+））。例如，函数（+J）[T]的类型是（（T R）（T R））（T R），这给了我们在时域上的实加法的期望提升。在使用布尔值函数时，这种整体方法开始从Z中删除下一节中的定义将∫∫e.B.不不马丁和菲奇202在很大程度上马丁和菲奇203+：X×X→X[在增补][在乘法运算]-：X→XX：X×X→X0：Xx：X·0+x=x[添加的标识][加法的逆]x，y：X·（−x）+x=0x+y=y+x[加法的交换性]x，y，z：X·x+（y+z）=（x+y）+zx（yz）=（xy）z[加法的结合性][乘法的结合性]x（y+z）=（ xy）+（ xz）[乘法分布]遵循这种风格，但将纯粹停留在标准Z中，使用松散的3使用松散泛型进行提升在本节中，我们在Z中构造一般提升的必要装置我们结合了上述两种方法的特点，但主要是受2.2节中重载方法的（另一种选择，在形式上而不是结构上不同，将遵循函数式编程文献，例如Backus的工作[2]，或者实际上，在现代风格中，使用monads的表示[20]。3.1环与场一个环是一个数学结构与两个运营商，通常表示为加法和乘法[3，p。238]。这两个算子满足一些性质和代数定律。我们使用一个模式来总结这些。环[X]当乘法运算是可交换的，并且有一个恒等式和逆时，得到的结构是一个场[3，p。245]。马丁和菲奇204⟨⟩字段[X]环[X]1：X−1：X→›X0/=1dom（−1）=X\{0}[identity and zerodistinct][无零因子]x：X|x/= 0·x=1x1=x[乘法的逆]x：X·【乘法恒等式】x，y：X·xy=yx[乘法的交换性]注意，这些Z定义稍微偏离了数学传统，因为我们通常认为环是结构X，+，。在这些定义中，我们已经说明了在某个类型X上形成一个环或场的某些运算的绑定意味着什么。4.1节的例子使用了实值函数环，在下面的例子中描述在第4.2节中，实值函数被不同地使用，在一个结构中（几乎！）形成一个场。显然，如果我们的应用需要它，我们可以定义其他结构，例如交换环[3，p。239]。如果我们在任何可能的地方追求没有要点的定义，我们可能会把这些定义写得有些不同。例如，场的最后一个公理可以表示为：（）=（）（第二，第一）。3.1.1示例最著名的环是实数和复数，具有通常的算术运算。假设实数和实数运算符的工具箱定义，实数形成环的事实可以表述为：► ⟨|0== 0，−==−，+==+，==| n ∈环[R].一个更有趣的环是将运算符逐点提升为从实数到实数的函数上的运算符马丁和菲奇205∗► ⟨|0==（λr：R ·0），−==（λf：R→R·（λr：R· −（fr），+==（λg，f：R→R·（λr：R·（fr）+（gr），λ==（λg，f：R→R·（λr：R·（fr）<$（gr） |⟩ ∈ ring [R → R].这个定理的证明需要证明这里定义的函数满足环中给出的公理。例如，我们可以证明f，g：R →R ·（λg，f：R→R·（λr：R·（fr）<$（gr）（f，g）=（λg，f：R→R·（λr：R·（fr）<$（gr）））（g，f）.大量使用lambda抽象是很麻烦的，这就是为什么Brien等人[6]使用范畴概念来提出一系列无意义的定义，如上所述。我们在这里使用类似的定义来重申猜想，也推广到从任意集合X到R的函数：[X]电子邮件|0 == 0 X，−==（X−→−），+==（X−→（+）），= =（X−→（|n ∈环[X→R].上述举证责任现在可以重新表述为（X −→（））=（X −→（））（第二，第一）。使用分布律和分布律的性质允许直接（等式）证明该性质，而无需求助于量化器，lambda抽象，或点数。3.2提升关系也可以定义一个提升版本的infix关系运算符首先，我们可以考虑一个具有偏序和等价关系的集合的定义，以无点的方式，使用Z代数工具箱中的熟悉符号。(So到目前为止，在模式定义中使用诸如“+”和“”之类的运算符但是，不允许将“=”定义这里出现的符号相应地比正常的Z相等更大更粗这种区别是微妙的，但在通常的文献中，并没有试图区分这些符号。马丁和菲奇206orderedRing[X，Y]环[X→Y]=：（X→Y）×（X→Y）→PX<：（X→Y）×（X→Y）→PX不相交的X→Y（fg），（gf），（f=g）<<.x，g，h：X→Y·（fg）（f+hg+h）<<（0h）（fg）（fh）（gh）<<

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