组件规格的缺陷对系统规范有重要影响

理论计算机科学电子笔记161（2006）91-107www.elsevier.com/locate/entcs软件构件和系统莎伦·弗林爱尔兰国立高威迪克·哈姆雷特1美国波特兰州立大学摘要关于使用组件开发的软件系统的推理从组件级规范开始，从组件级规范导出系统级规范。虽然合理的组合推理是正式规范方法的一个优势，但系统构建的实践经验使我们在组合两个从未打算组合的组件时会感到惊讶。 组件规格，就像任何其他人类工件一样，很可能是错误的。组合将一个组件中的错误与另一个组件中的错误相对立，导致意外的、通常是奇怪的行为。我们回顾了正式软件规范的理论，并将其应用于组件规范到系统级属性的组合，其中组件规范中的缺陷可能会被奇怪地反映出来。我们的结论是，系统规范的理想属性并不总是产生于组件级别的相同属性。保留字：形式规范、软件组件、组成1引言虽然程序语义、规范和它们之间正确性关系的基本形式化描述已经被长期使用，但是将这些描述应用于软件组件及其组合到系统中的探索很少。此外，软件中持久状态所扮演的角色还没有被挑出来进行形式化分析。状态在基于组件的系统开发（CBSD）中起着核心作用，因此CBSD是一个很好的理论处理环境1由NSF资助CCR-0112654和E.T.S.爱尔兰科学基金会的沃尔顿奖学金。这两个机构都不对本文中的陈述负责。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.02792S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）911.1基本定义软件组件被松散地定义为仅由其接口（语法）和黑盒行为（语义）描述的任何可执行单元。这个定义（Szyper-ski [12]）消除了关于特定编程语言和设计方法在CBSD中的作用的大量无利可图的争议。真正的组件通常是通过并发执行来组合的，在并发执行中，组件之间进行异步通信。时态逻辑最好地捕获并行执行[2]，模型检查可以用来推理组件和系统的错误[6]。与此相反，我们选择只讨论行为的顺序和功能方面。我们选择的理由是它的数学简单性和存在的一个机构的程序分析理论的基础上功能抽象。我们希望，较老的，非时间的形式主义将阐明基本问题。定义1.1组件代码通过它计算的两个映射来识别：f：D×H→R，从其输入域D和状态域H到其输出的函数映射范围R;以及g：D×H→H，国家映射。在本文中，符号D、H、R、f、g将保留其在定义1.1中的含义。在定义1.1中，D和H之间的直观区别是输入变量是一个程序被赋予一个任意的输入;相反，它自己设置了一个状态，这个状态后来又改变了它。程序语义映射通常是部分函数，因为可能发生代码不会终止于某个特定的输入x和状态h，因此f和g不定义在（x，h）。我们只是偶尔关心终止，所以除非另有明确说明，我们假设f和g是全的。在定义1.1中，一个持久状态集H和映射到它的程序行为g在符号上被挑选出来，这是不寻常的。通常的观点是将程序映射视为应用于更广泛集合的单个函数，该集合包括输入和状态值，以及程序使用的内部变量的值我们的论点是，状态是形式化软件描述中许多困难的来源，因此应该被强调。我们可以通过为程序定义一个单一的语义函数，然后投影到一个特殊的状态映射集合上来实现这一点然而，这样的形式主义使得更容易不注意到国家作为一个单独的实体，并补充说，一个额外的符号层（用于投影），每当考虑状态时。状态集被认为是一个程序的本地集，任何其他程序都无法访问。(This当我们在第3节中考虑组合组件时，这一点变得很重要。）这种私人国家有两个不同的方面。第一，混凝土S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）9193状态，由H本身表示，并由代码函数g直接操纵。第二个集合是抽象状态J，通常是一个数学定义的实体，它进入具体化。做出区分的原因是J可能是直观状态的高级描述，它可能不作为编程语言中的数据类型。然后，有必要用H中的程序实体来表示J的值。两者之间的联系是由抽象映射L：H→J。 这种表现和抽象是信息隐藏的基础，是最重要的实用设计技术。然而，区分抽象状态对我们希望讨论的情况几乎没有增加，所以L通常被认为是恒等函数。原则上，规范不需要关注软件状态。描述一个程序需要什么并不一定需要描述它将维护的持久存储器。实际上，如果决定使用持久存储以及它的形式（如果使用的话）留给实现者，就像选择临时存储（内部变量）一样，这将是理想的。如果规范确实提到了状态，它可能是在非约束性操作规范的意义对于非正式的规范，可以通过使用诸如“如果这个值在以前的运行中已经出现N次，那么打印N的值......”这样的迂回来避免明确地描述状态。然而，有时似乎不可能给出依赖于先前历史的所需动作的精确的、正式的描述，而不明确地因此，具体化语言和形式化方法确实包含了状态。本文考虑的问题之一将是国家应在多大程度上明确进入正式规范。我们从一个包含国家的定义开始。定义1.2码的规范S是D×H×H×R上的关系。在定义1.2中，叉积中的第一个H集直观上是一个输入状态，第二个H集是一个输出状态。规范可能无法在概念上区分“输入”和“输出”。然而，在定义1.2中得到的直觉是，叉积的最后两个集合中的值由S规定，而前两个集合中的值没有规定。“输入”状态是一个特别敏感的量，因为对“输出”状态的正是正确性的定义抓住了这些输入/输出的区别。最简单的定义是：定义1.3由函数映射f和状态映射描述的程序g是状态盲正确的，wrtS i <$x∈D，<$h∈H，或者3：（x，h，g（x，h），f（x，h））∈S，或者2.如果持久存储实际上是一个程序输出，供其他程序使用，它的形式当然需要规定。[3]如果状态被映射L：H→J抽象，则具体化将是D×J×J×R上的关系，定义将为：对于每个x∈D和每个h∈H，要么（x，L（h），L（g（x，h），f（x，h））∈S，要么不存在r∈R使得对于任何hJ，（x，L（h），hJ，r）∈S。94S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91<$r <$hJ，（x，h，hJ，r）/∈ S.在后一种情况下，x在状态h中被称为无关输入x的意图定义1.3没有赋予国家任何特殊的作用。为了做得更好，我们必须考虑输入序列和结果的状态值序列。 设h0∈ H是一个特殊的初始状态，考虑输入序列t =（x0，x1，.，xn），xi∈D，0 ≤i≤ n。德费恩hi= g（xi−1，hi−1），1 ≤i≤n.然后程序的连续函数输出是f（x0，h0），f（x1，h1），.，f（xn，hn）.序列t的正确性的定义抓住了我们对状态的直觉：定义1.4f和g对序列twrtS i ∈t的所有成员都是正确的要么（xi，hi，g（xi，hi），f（xi，hi））∈S或者xi是状态hi中的该程序是序列正确的wrtS i，它是正确的所有这样的序列。定理1.5状态盲序列的正确性，但不是相反。证据 显然，状态盲正确性意味着序列正确性，因为后者所需的每个特定关系元素都包含在前者中。为了证明反向蕴涵不成立，考虑一个程序P0，其描述如下：其中，g（x，h）=h0，f（x，h0）= 0，f（x，h）= 1，hh0;和一个规格：<$x，<$h，（x，h，h，0）∈ S.P0是序列正确的wrtS，但不是状态盲正确的。Q显然，状态盲正确性要求的不仅仅是直观上的必要性;序列正确性足以保证程序直观上的良好行为定义可以被构建为序列正确性的变体，将状态完全留给实现。S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）9195定义1.6设D+是Dn中的所有有限序列，对任意整数n≥1。把定义1.2中的一个具体化S改变为D+×R上的一个关系，即只关心输入序列的输出。 S必须包括特殊的定义条件，被重置，使得人们可以说在该条件下接收的输入程序从输入端序列t∈Dn如定义1.4所示，我们可以说程序对所有t都是正确的，我们有（t，f（xn，hn））∈S，其中S在序列的开始被重置把定义1.6中的概念称为状态隐藏的，相反，把定义1.2、1.3和1.4中的概念称为状态显式的。基于行为序列的状态隐藏思想也可以用时态逻辑来描述这个应用程序与捕获并发行为不同，但我们在这里并不追求它 假设S是一个状态，显式指定，SJ是状态隐藏指定。不可能存在S和SJ“等价”的意义，因为与为前者规定的状态不同的状态（事实上但我们可以定义一个方向的关系定义1.7SJ覆盖Si，所有对S序列正确的程序对SJ状态隐藏正确。在续集中，当然而，大多数直观的解释对于不同的定义都具有同样的意义。例如，序列正确性仅仅将关于“所有状态”的直观陈述1.2‘Wrong’对某些人来说，一个规范S可能是错误的，因为：(i) S不符合那个人的愿望，即，存在感兴趣的某个（x，h）和作为输出不可接受的某个E和/或作为状态h中的输入x上的结果状态不可接受的E，然而（x，h，e，E）∈S。我们说S是不正确的，或者S在（x，h）是错误的。(ii) S在（x，h）处是不完整的，这意味着在状态h中输入x的输出是人所期望的，然而x是(iii) S在（x，h）处是过度规定的，这意味着输出r和结果状态hJ在输入x上的状态h是人可以接受的，但（x，h，hJ，r）/∈S。(iv) （序列与状态盲正确性）S在（x，q）处是错误的或不完整的或过度预写的，但是根据S，q不应该出现在以重置开始的任何输入这种情况是由于人们不清楚哪种正确性是适当的。(v) （状态隐藏与状态显式的正确性）状态显式的S在（x，q）处是错误的或不完整的或过度规定的，但存在一个覆盖S的状态隐藏规范SJ，这些错误对它没有意义。同样，这个人96S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91混乱的定义。在使用这些术语时，省略关键人物是一种惯例（尽管可能不明智）。过度处方和不完全性之间的关系有些特殊。一方面，最好不要过度指定，也就是说，对于给定的输入x，指定关系应该尽可能宽。但不完全性是未指定的极端：如果输入x上的任何结果是可接受的，那么指定在x上是不完整的，这也是不可取的。2形式化方法我们研究了几种形式的数学规范，并讨论了状态进入正确性概念的方式。考虑一个简单的原型程序，它的状态记录了以前输入的数据，供子程序使用，这是很有启发性的。这样的程序模拟了永久数据库的使用。它有“存储”输入，修改状态，没有显着的输出值，以及“查找”输入，检索先前存储的值并输出它们。例如，在一个类似通讯录的应用程序中，状态可能是名称-地址对。如果输入是find John Smith，则如果状态包含该对，则输出应该是sm137255@aol.com，或者如果状态没有任何与这 样 的 第 一 个 元 素 的 对 ， 则 输 出 未 找 到 。 如 果 输 入 是 store John Smith ：smith27@ucg.ie，如果没有状态对具有该人的第一个元素，则输出应该是OK，或者重复-如果有则忽略。这种草率的指定可以使用如上所述的显式状态发展成精确的关系Sa或者，状态隐藏的规范SaJ可能类似于以下内容设t∈Dn是输入序列t =（x1，x2，.，xn），其在复位条件下开始。有两个例子：(i) xn是商店John Smith：smith27@ucg.ie。然后，如果名称没有与store一起出现在序列t的任何较早成员中，则输出是OK的，或者重复--如果它出现了，则忽略;(ii) 找到约翰·史密斯。然后，如果涉及名称“John Smith”和“store”的最早成员xi∈t 是 （ 比 如 ） store John Smith ： sm137255@aol.com ， 则 输 出 为sm137255@aol.com在下面的小节中，对每种形式主义的描述都是简短而深刻的，只是为了提醒读者它们的属性。2.1MillsHarlan Mills在20世纪80年代提出了一种在其最完整的形式[9]中，他的思想被应用于Pascal的一个子集。一个指称意义M被分配给一个程序P，该程序P从它的基本语句开始并归纳地进行到复合语句。最终的结果是S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）9197P给P赋值一个函数语句，可以表示为并发赋值（X1，X2，.， Xn）：= M（X1，X2，...， Xn），其中Xi是P中出现的变量，并发赋值反映了程序如何改变它们的值。Mills将规格化为函数S，将程序变量的值映射到相同的值，并定义了正确性如S。 因此，程序可以在选择和扩展S域时操纵不在S中的变量，但是在S所覆盖的变量和域上受到约束。对于我们的目的，米尔斯形式主义中的程序P 函数f和g分别是P在Xr和Xh的值集上的投影有趣的规范是从输入和状态值集到输出值和输出状态值集的映射。例如，由于第2节的原型规范Sa是一个函数，它可以作为米尔斯规范。如果一个程序P是用显而易见的方式来实现Sa的，设置Xh作为状态以程序提供的状态变量约束的形式输入Mills正确性证明。在试图证明定义的功能包容性时，将需要考虑的情况减少到程序实际允许发生的那些状态值是非常有帮助的。 尽管这样做是完美的，正确性证明将有效地只处理对应于序列正确性的情况;另一方面，如果忽略实际在实践中，任何证明都是在证明涉及状态的额外情况的困难程度和表达状态约束的困难程度之间的妥协，从而简化了证明。2.2Hoare逻辑遵循弗洛伊德[3]的思想，霍尔设计了一个一阶程序逻辑[5]来指定程序应该做什么或做什么。这个逻辑的谓词的范围是程序中使用的变量的值集。假设这些是（x1，x2，...，xn），并将这个n元组表示为X. 声明：(1)P（X）{C}Q（X）断言如果语句P在程序C执行之前持有变量值，那么语句Q将在之后持有它们。P是前置条件，Q是后置条件。在Q中，变量被在输入和输出变量的约定下，方程（1）构成了一个未知程序C的一个特例。另一方面，如果给定了一个特定的C，断言（1）要么成立要么不成立，并且C对于P98S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91我H具体来说，如果有。霍尔为命令式程序提供了一种证明方法，其中确定了各个语句的前置条件和后置条件，推理规则允许将这些条件组合起来，直到整个程序达到所需的P和Q（如果程序不正确，则不达到同样，假设断言中只有六个变量，xi表示输入，xr表示输出，xh表示状态，并在后置条件中为xJ赋值一般来说，霍尔证明方法不需要对任意程序C精确地约束函数f和g。霍尔推理规则的某些程序语句，如循环和递归程序调用，包括任意不变的谓词，不需要完全捕捉这些语句的结果。 的因此，规则确定谓词R（X），使得真{C}R（X）。观察时作为正确性关系，R约束C的语义映射f和g，但可能而不是决定他们。也就是说，例如，f（xi，xh）=xr<$R（xJ，xJ，xr），但是Ih相反的含义不一定成立。同样，前置条件和后置条件构成关系规范S（X）=P（xi，xh）<$Q（xJ，xi，xJ，xh，xr）。I hState通过不变量的概念进入Floyd/Hoare证明不变量是一个陈述I（X），通过加强前提条件来简化正确性的证明。 如果P（X）{C}Q（X）的证明不能完成（也许只是因为人类或机械证明者不能胜任这项任务），那么可能是P（X）<$I（X）{C}Q（X）<$I（X）更容易证明，并且如果I（X）可以被证明最初成立，则是等价的。不变量通常描述特定变量价值观，特别是国家的价值观，都在发挥作用。引入不变量是正确性证明的创造性部分，因为除了简化证明的需要之外，没有什么约束它们的形式。强不变量引入了一个状态限制，使其余的证明更容易，但随后建立了自己的困难证明义务。对于指定Sa，后置条件是一个简单的断言确认。例如：如果xJ是一个包含名称，xr包含I h地址和xh=xJ;或者，如果xJ是一个不包含名称，则喜喜姓名和地址被添加到xh，并且xr是不变可能有助于证明xh没有重名。2.3Z规格由牛津大学编程研究小组基于Jean-Raymond Abrial的开创性工作开发的Z规范语言是面向模型的规范语言的一个例子，它在2002年成为国际标准。它是一种基于集合论和一阶谓词演算4的形式符号。Z中的规范描述了一个抽象的状态空间，通常使用状态空间上的谓词（不变量）来描述有效的状态。 的操作在状态空间上使用谓词Pop在输入变量X？上给出，输出变量X！以及“之前”状态X h和“之后”状态X j的变量谓词描述了输入和状态之前的条件、可能的输出以及[4]严格来说，很容易把数学符号错误地称为S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）9199AddressBookaBook：PERSON→›地址商店OKΔAddressBookp？：一个人？：地址r！：报告p？∈/domaBookaBookJ=aBook{p？›→a？r！=OK存储错误你的地址簿p？：一个人？：地址r！：报告p？∈domaBookr！=重复忽略状态从之前变为之后。例如，规范Sa的状态空间可以建模为从名称到地址的部分函数。请 注 意 ， 在 本 例 中 ， 省 略 了 不 变 量 （ True ） ， 这 意 味 着 从 PERSON 到ADDRESS的任何部分函数都是有效的地址簿。存储操作应该检查名称是否在状态函数的域中，如果不在，则添加新的maplet并输出OK，如果是，则返回错误。Find操作应该检查名称是否在状态函数的域中，如果是，则输出结果，或者返回错误，在两种情况下都保持状态不变。省略了形式模式虽然Z规范准确地描述了给定输入的状态和输出，但它没有说明可能发生的操作序列（以及状态）。然而，规范通常会指定一个初始状态，以及证明它是一个有效状态，即满足状态不变量。地址簿Sa的初始状态将是空函数，即包含没有地图。由于函数是所需类型的部分函数，因此默认情况下它满足不变量100S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91初始化地址簿地址簿Ja BookJ=该系统被认为是建模的初始状态，然后由一个任意序列的操作。此外，在每个操作上都有一个证明要求，即状态的改变将总是导致有效状态，给定有效状态作为输入。Z规范的实现将包括状态空间的具体表示，对于规范中的每个操作，具体状态上的相应因此，正确性是一个证明每个抽象操作都由其相应的具体操作来细化的问题，操作A±操作C。如果我们考虑OpA和OpC作为（D×H×H×R）上的关系，这意味着证明：∈D，Xh∈H，（<$XJ∈H，X！∈R，（X？，Xh，XJ，X！）∈OpA）H Hn（nXJ∈H，X！∈R，（X？，Xh，XJ，X！）∈OpC）H H和<$XJ∈H，X！∈R，（X？，Xh，XJ，X！）∈OpC<$（X？，Xh，XJ，X！） ∈OpA。h h h这种Z概念的正确性介于状态盲正确性和序列正确性之间。它不像状态盲正确性那么强，因为可以假设输入状态是有效的，因此输出状态也是有效的。它与序列正确性不同，因为所有有效的输入状态都需要证明，即使是那些可能永远不会从任何输入序列中产生的3组件组成在考虑由我们的一般形式描述的组件构建软件系统我们区分这些下标映射，关系等机制的系统建设将被限制为这一机制并不能涵盖制度建设的所有案例，但它显然是一个重要的案例，其中出现了重要的理论问题。3.1形式上定义组合对于具有状态的组件组合在一起的系统，持久状态的正确直观含义并不明显。一方面，系统状态可以被认为是5系列调用不是一个程序“调用”另一个程序的子程序机制S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91101UA BfUgUfBgBfAgAbe使用信息隐藏设计的面向对象类的模型建议后一种选择。如图1所示，将两个部件A和B串联起来形成系统U。1.一、我们希望根据系统代码的行为来定义系统代码的行为，Fig. 1.将两个组件串联组合成一个系统件.定义3.1URB，其状态集为HU=HA×HB，其两个映射为：（二）以及（3）fU（x，（h1，h2））=fB（fA（x，h1），h2），gU（x，（h1，h2））=（gA（x，h1），gB（fA（x，h1），h2）），对任意x∈DU，h1∈HA，h2∈HB.在定义3.1中，方程（2）的函数映射fU方程（3）中的状态映射gU将A和B的一个输入和一对状态值带入一对，第一个元素是A对其状态的作用，第二个元素是B对其状态的作用，但在后者中，B看到的输入是A的输出。定义3.1反映了功能组件形式主义的将A和B串联的自然意图是RADB;然而，如果不是这种情况，并且对于某些v∈DA，fA（v，h）/∈DB，则fU在（v，h）处未定义，并且为了使U正确，v必须是我们选择每个组件的私有状态而不是系统的全局状态的原因在等式（2）和（3）中显而易见。对于私人国家，国家职能g不相互作用，甚至不通过合成相互作用，这大大简化了理论。将状态保存在每个组件中还允许组件开发人员在不引用任何其他组件的情况下分析g更难的是找到一个直观正确的定义，说明组件规范应该如何组合成一个系统规范。一种可能性是取关系的组成定义3.2（直接构成）102S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91SU=SASB={（x，（h，hJ），（k，k J），r）|<$y，（x，h，k，y）∈ SA<$（y，hJ，k J，r）∈ SB}.不幸的是，简单的组合不能正确地处理例3.3假设组分A和组分B串联形成系统U。让他们的规格包括四元组：（x0，e1）∈SA和（x0，e2）∈SA.（e1，z）∈SB但e2是SB中的无关输入对于代码，fA（x0，）= e2和fB（e2，）= ZJZ.当A在输入x0上产生一个错误消息，其特定形式可能是e1或e2时，就会发生这种情况的具体版本。然而，e2是如此不寻常，以至于它是B的一个例3.3中的四元数说明与A和B对于SA和SB是正确的并不矛盾。然而，用直接合成定义SU，（x0，（，），（，），z）∈SU，但（x0，（，），（，），ZJ）/∈SU，而fU（x0，（，））=ZJ，则级数组合是不正确的。组合的定义可以通过从组合中删除任何存在未定义替代的四元组来调整以处理示例定义3.4（严格组成）SU=（SA<$SB）\{（x，（h，hJ），（k，k J），r）|（x，h，hJ，y）∈ SA<$t，（y，hJ，k J，t）/∈ SB}在例3.3中，x0是严格合成规范SU中的一个然而，直觉上x0不太可能是创建空洞的情况表明系统规范中的信息丢失。对例3.3最直观的描述似乎是A不应该与B串联，因为输入x0上的系统行为是意外的。只有严格的复合定义是可以接受的，我们不能让两个正确的成分组成一个不正确的系统。然而，直接的构图是直觉的更好基础。定义困境6由于state在示例中不起作用，因此state值仅显示为占位符。S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91103PU可能是对提议的组件组合进行评估，以查看定义是否不一致。如果他们这样做，这种组合可能被认为是危险的。然而，这种自然的观念有着令人不安的分支，因为它对形式规范的“可组合性”提出了质疑。组合中的危险完全是一个3.2现有形式中的复合Mills、Floyd/Hoare和Z形式主义被设计用来描述完整的系统。每一个都有一个系统内的“组成”的概念，但没有一个与系列组合的组件思想相匹配。困难的一部分是，形式因此，米尔斯串联的组件直观地3.2.1米尔斯考虑两个程序和它们的规格，在米尔斯的形式主义中被捕获为（具体化函数SA）正确性）和（规格SB），并将它们组合成系统U。 通过正确地重命名输入，输出，以及PA和PB的状态变量，可以用下式描述：组件描述。（将PA的输出变量与PB的输入变量区分开来，并保持它们的状态变量不同。） 由于规范是函数式的，所以简单的组合SU=SA<$SB并不显示例3.3中的非确定性的困难。3.2.2弗洛伊德/霍尔逻辑就像米尔斯演算一样，通过重新命名串联系统U的两个分量A和B的输入、输出和状态变量，A的前置条件和B的后置条件可以作为U的前置条件和后置条件，从而定义一个自然的SU。不幸的是，SU的性质不太理想。首先，尽管很自然地期望B的前提条件应该是A的后置条件的逻辑结果，但是这个条件对于U的正确性不是必需的。例如，可能发生系统后置条件太弱，以至于不需要B第二，例3.3中显示的非确定性很容易使组件正确，而系统不正确。把构成前置条件和后置条件看作关系，它们根据定义3.4的严格复合可以消除这种困难，但是在前置条件和后置条件形式中似乎没有严格复合的自然表达PBPAPA104S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91面向对象编程使用Hoare规范（它称之为面向对象的类作为组件的重用[8]是基于传统的编程语言过程调用，而不是调用，因此与我们的理论并不匹配。3.2.3Z中的模式组合Z规范表示法包括模式组合的概念，表示一个操作的结果后面跟着另一个操作。然而，在Z模式组合和规范组合之间存在一些重要的区别。本文给定两个Z操作Op和Op，组合OpoOp被定义为A B A9B只有当操作都定义在相同的状态空间上时，状态才是全局的。该组合是顺序的，因为OpA的输出状态变成OpB的输入状态，但是输入和输出是共享的。更正式地说，如果OpA是DA×H×H×RA中的关系，并且OpB是DA中的关系，D×H×H×R，则OpoOp是（D<$D）×H×H×（R<$R）中的关系B B A9B A B A B在定义Z中的模式组合时所做的选择来自于一个更早的时代，在那个时代，现代的组件观是没有预料到的。4不完善的规范使用形式化数学方法的软件开发通常设想如下进行：(i) 设计一个规格。也就是说，产生一个要写的程序必须满足的关系S，或者一个特定的形式主义提供的关于S的任何变化。(ii) 写一个程序P来满足S。 有时，形式主义提供了一种操纵S以获得必然正确的代码的方法;在另一个极端，代码可以被编写以满足与S仅松散联系的直观理解。(iii) 证明P相对于S是正确的。如果P在构造上不正确，这一步可能非常困难。这种范式的经验表明，S几乎总是亏的[4]。正式的具体化是一项要求很高的复杂活动，大多数人都不适合。如果P是由S构造的，那么在P被测试或使用之前，这些缺陷可能会被隐藏起来;如果P是单独手工构造的，那么证明就会失败，有时是因为P不是我们想要的那样，但更多的时候是因为S是错误的。尽管这几乎是普遍的经验，但很少有明确的研究规范错误。在基于组件的软件开发中，组件规范和代码是给定的，通常不需要调整。 因此，这种设置是研究的理想选择。具体的错误和它们进入组成的方式。通过考虑可能出现的问题，我们希望了解CBSD的特殊规格需求S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）911054.1例3.3再访重申3.1节中的问题示例：组件A和B串联放置，A在输入x0上产生错误消息，其特定形式可能是e1或e2;e2是有许多可能性，其中规格SA或SB不足：• 可能是SA在x0处是错误的-可能不应该有错误消息，或者e2对于x0不是可接受的错误消息。解决方案可能是从SA中移除将x0与e2相关的元组，从而需要相应地改变组件代码A• 在SB真的不完整并且e2不应该是无关输入的情况下，那么一个好的解决方案可能是像对待e1一样在这种情况下，规格SB和组件代码B• 或者，也许SB在e1处是错误的，并且要求特定的结果是过度规定的。在这种情况下，我们可以使e1成为• 另一种情况是SA在x0处是错误的，并且e1不是可接受的错误消息。现在，组件A是好的，即使它的规格是错误的。这些可能性表明，组件的不完美规格组合是多么脆弱，以及当系统级别出现意外时，找出原因和所需更改的困难4.2组件的替换和修改如果基于组件的开发要实现它的承诺，它必须能够从组件的规范中合成组件组合的规范。这对组件规格化形式主义提出了新的要求开发人员希望他们能够独立地修改组件（包括代码和规范），独立地对修改后的组件进行推理，然后将更改替换到系统中。以下是对这一过程的最低期望：(i) 如果组件代码被更改，但对于未更改的组件规范仍然是正确的（所谓的(ii) 如果一个组件规范被扩展，所有的原始元组仍然属于它，但其他的元组被添加，使用扩展的规范不应该做更多的扩展系统规范。(iii) 组件中的错误不应隐藏在系统级别。例3.3将违反期望（ii），如果它被视为扩展第一个组件规范以允许消息e2。很容易构造其他病态的例子，这些例子是实际开发人员所熟悉的情况，例如：106S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91• 两个规范中的每一个都是错误的，它们的代码都是正确的，但它们的组成并没有错，违反了上面的期望（iii）。(This如果第一个组件的错误输出值被第二个组件校正，并且如果第二个组件的错误值从未出现，因为第一个组件具有不激励它们的受限范围，则可能发生。）在这种情况下的危险是，系统的直观属性不是来自组件，而是偶然出现的。• 一个组合是正确的，尽管它的第一个组件是错误的（也许是因为错误的输出被纠正）。 当第一个组件被纠正时，合成失败（可能是因为第二个组件无法处理正确的第一个组件输出）。从这些例子中，我们了解到，组件级的看似无害的指定错误会引入不确定性，使系统级推理变得可疑。形式规范开发模型所要求的完美是罪魁祸首。5结论我们重新研究了函数和关系形式规范，明确考虑了持久状态，并将其应用于软件组件。这个练习表明，正式的规范在很大程度上是作为一个单一程序的思想来构思和发展的。它设想程序和规范被纳入正确性的关系中，这就是它的结束。相反，在软件开发的组件视图中，组件级的正确性只是将组件组合成系统的推理过程的开始人们常说数学规范方法具有这一见解基于功能性构图的明显概念，但当我们考虑到人们在构图时所犯的错误时，它就受到了质疑。这些错误以奇怪而奇妙（或可怕）的方式结合在一起，事后再解决这些问题也无济于事。如果要有一个正式的理论的组成部分组合成系统，理想的系统性质必须得到的性质的组成部分，我们已经表明，这是有问题的。为独立系统建立良好的正规理论的属性对于基于组件的系统可能适得其反非决定论就是一个很好的例子。对于一个单一的程序来说，没有必要的通过允许非确定性的选择（也就是说，指定是一个关系，而不是一个函数），实现者被赋予了有用的自由，正确性证明被简化了。但是，非决定论在组件规范中是一件坏事，因为它强迫对组成进行非自然的定义，当人们犯规范错误时，它会表现得很糟糕米尔斯的形式主义是完全功能性的，而弗洛伊德/霍尔的形式主义是首选，因为它允许非决定论。对于成分理论来说，选择可能是相反的。S. Flynn，D.Hamlet/Electronic Notes in Theoretical Computer Science 161（2006）91107Parnas和Madey在[11]中认识到，组件的需求文档不会完全描述该组件的行为可能有许多明显不同的组件满足相同的要求。他们建议可能需要软件行为规范，该规范描述了组件的实际（功能）行为。这与我们的观察一致，即非确定性可能有利于系统规范，但可能不适合描述组件的行为。如果状态指定是不确定的，或者在隐藏状态的情况下，如果状态根本没有指定，错误指定的组件的组合可能特别不可预测。只有当特定的状态出现时，才会出现意想不到的结果，而且很难确定这种情况是否真的发生过。组件级别的证明可能是状态盲的，因此它们永远不会掌握实际发生的考虑到人类能力的变幻莫测，不可避免的具体化错误是不正确的-一个人想要的东西与正式的数学定义不同。形式方法的批评者说，形式主义只是将不正确的实现问题转移到错误的具体化。相反的论点是，这种转变是值得的，因为错误的规范比错误的代码更容易检测和理解在组件设置中，这场辩论的批评者一方得到了加强。由于组件开发人员不知道他的组件将被放置到哪个应用程序中，也不知道其他组件将与之一起使用，因此他无法识别可能的规范错误-它们只会在系统级别上对一些无法想象的系统变得重要。引用[1] 13568：2002，I.，信息技术。Z形式规范表示法。语法、类型系统和语义学。国际标准。[2] Abadi，M.和L. Lamport，联合规范，ACM TOPLAS（1995），pp. 507-534[3] 弗洛伊德河W.，应用数学专题讨论会论文集（1967），pp. 十九比三十二[4] Gerhart，S.，D. Creigen和T.罗尔斯顿，使用正式方法对工业实践的观察，在：第15届ICSE，1993年，pp. 24比33[5] 霍尔角A. R.，计算机程序设计的公理基础，Comm. of the ACM（1969），pp. 576- 585[6] Li，H.，S. Krishnamurthi和K. Fisler，《将交叉特征视为开放系统》，载于：《SIGSOFT FSE学报》，2002年，第100页。八九比九十八[7] 迈耶湾，[8] 迈耶湾，The grand challenge of trusted components，in：Proc. ICSE 25，2003，pp.660-667.[9] 米尔斯，H.，诉Basili，J.Gannon和D.哈姆雷特，[10] Parnas，D.， On a“Buzzword”：Hierarchical structure，in：Proc. IFIP Congress（1974），pp. 336-339[11] Parnas，D. Madey，Functional documentation for computer systems engineering，Science ofComputer Programming（1995），pp. 41-61.[12] Szyperski，C.，