形式化组件搜索策略

理论计算机科学电子笔记187（2007）173-188www.elsevier.com/locate/entcs形式验证软件大卫·赫默1阿德莱德大学计算机科学学院，阿德莱德，南澳大利亚，5005，澳大利亚摘要基于使用形式规范作为检索基础的思想，已经提出了许多基于组件的软件开发的形式化方法。这些方法在搜索组件时提供了良好的查全率和查准率。 最近，组件适配的问题已经开始要解决的问题，在认识到这一事实，即图书馆的组成部分将很少满足用户的需要完全。然而，目前的方法的主要弱点是它们只满足单一的适应步骤。实际上，我们通常需要应用一些适应步骤的组合。在本文中，我们提出了一个搜索策略的集合，它允许我们将一系列的匹配和适应命令组合成一个单一的步骤。这些策略是以一种通用的方式提出的，目的是它们可以应用于各种不同的基于形式的CBSD方法。我们用一个简单的例子来说明搜索策略的使用。保留字：组件;适应;形式方法1引言对于安全关键软件，基于组件的软件开发（CBSD）方法使用预先验证的库组件，可以节省成本，特别是与验证相关的成本。然而，基于组件的方法只有在重用组件的总体工作量明显小于从头开始开发（和验证）软件的工作量时才是可行的[13]。与其他CBSD方法一样，在实现任何真正的节省之前，需要解决许多挑战[3]。这些挑战包括找到合适的组件并对其进行调整以满足软件工程师的特定需求。传统的构件检索方法是基于文本或关键词的匹配.然而，由于相关的模糊性和不精确性，1 电子邮件：david. adelaide.edu.au1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.08.051174D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173对于自然语言规范，这种检索方法的精确度和召回率都很差为了解决这些问题，已经开发了基于匹配的正式组件规范在库中定位组件的方法[12，8，15]。最近，已经提出了适应正式指定的方法[10，9]。为了在匹配和适配之间产生紧密的协同作用，我们使用通用库组件实现适配策略[5]。为用户需求寻找合适的解决方案涉及一系列匹配步骤。在每个步骤中，库组件都被组合和调整，直到完全符合用户要求。在实践中，这种方法通常涉及许多平凡而繁琐的步骤。在本文中，我们定义了搜索策略，它可以用于将多个匹配和自适应步骤合并为一个步骤。这个想法类似于在交互式定理证明器中使用策略，事实上，我们从这项工作中得到了很多启发。通过这些搜索策略，我们的目标是自动化通用组件自适应步骤，使软件工程专注于更重要的设计决策。在本文中，我们定义了一组用于半自动化组件适配和检索的搜索策略。 我们的意图是，该策略应该适用于任何使用基于形式的匹配和适应技术的方法。因此，我们从第2节开始，定义一个通用模型，用于匹配和适应正式指定的组件。我们分别考虑单个单元和模块化组件。在第3节中，我们定义了搜索策略的一般形式。我们还定义了一系列基本的搜索策略，从中可以构建更复杂的策略。在第4节中，我们定义了一组战术，用于组合基本战术以构建更复杂的战术。在第5节中，我们通过一个使用CARE语言和工具的简单示例来说明搜索策略的使用。第6节包含我们的方法与其他相关工作的比较。2基于逻辑的组件在本节中，我们将介绍一个通用框架，用于匹配和适配正式指定的组件。该框架概括了现有的具体匹配方法，捕捉了关于组件适配的组件匹配的一般概念。这里使用的框架是基于早期论文[6]中提出的通用框架;然而，在下文中注意到了一些变化我们使用Z规范语言[14]对框架进行建模。通用框架在两个独立的粒度级别上考虑组件。在第一个层次上，我们考虑与函数、类型、定理等相对应的各个单位。在第二层，我们考虑模块化组件，D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173175匹配策略条件精确匹配（Qpre惠Spre）（Qpost惠Spost）插件匹配（QpreSpre）（SpostQpost）保护插件匹配（QpreSpre）（（S前S后）Q后）满意度匹配（QpreSpre）（（QpreSpost）Qpost）表1基于语义的规范匹配策略由多个单元组成。这种分离使我们能够专注于与特定粒度级别相关的匹配和自适应技术。在为单个单元开发匹配方法时，我们不需要考虑如何匹配单元集合。类似地，当开发匹配模块的方法时，我们可以假设存在匹配单个单元的方法2.1单元匹配我们首先考虑包含在模块库组件和程序中的基本单元。单位的例子包括函数、类型、定理等。我们使用泛型类型对这些单元进行建模，表示一组没有进一步定义的值。【单位名称】我们对单元的内部结构不作任何假设，但在本节的其余部分，我们描述了必须为每种单元定义的一些函数和关系我们假设一对单位之间存在关系，定义第一个单位满足第二个单位意味着什么。一般而言，满意度关系将适用于单位的指定部分。满意度：单位参与单位表1显示了一些更常用的规范匹配技术的满意度关系示例，这些规范匹配技术用于使用前置和后置条件规范的类函数单元。Zaremski和Wing [15]给出了一个更全面的匹配关系集合。在表中，库单元规范由S表示，查询规范由Q表示。下标前置和后置分别指前置条件和后置条件176D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173当Q和S的前置条件等价，且Q和S的后置条件等价时，精确匹配成功。当库组件的前置条件弱于查询的前置条件，而库组件的后置条件强于查询的后置条件时，插件匹配成功。保护插件匹配是在插件匹配的基础上，在后置条件关系中增加了库组件的前置条件。满意匹配类似于受保护的插件匹配[11]，但使用查询组件的前提条件，而不是库组件来保护后置条件关系。请注意，随着我们沿着表往下走，匹配关系变得越来越弱，因此，例如，插件匹配也将是精确匹配通过使单元具有适应性，组件库可以以不同的方式应用于解决各种问题。我们定义了一个泛型类型来表示单元可以调整的方式：【适应】在这一点上，我们通常只对支持相对简单的适应感兴趣。通过简单，我们的意思是可以使用自动化技术（如单位规格的统一）这种技术的示例包括标识符重命名（例如，对于变量和类型名），以及高阶变量实例化。在可以应用不同类型的适配的情况下，我们将Adapt建模为元组。我们定义函数adapt，它将适应应用于一个单元，以产生一个新的单位我们还定义了平凡的自适应，trivAdapt，当应用于adapt函数时，它保持单位不变，以及合并两个自适应的函数mergeadapt：Unit×Adapt→UnittrivAdapt：Adapt合并：Adapt×Adapt→Adaptu：Unit·adapt（u，trivAdapt）=uu：单位;a1，a2：适应·adapt（u，merge（a1，a2））=adapt（adapt（u，a1），a2）我们将合并建模为部分函数，反映了合并两个适配并不总是可能的事实。最后，定义一种匹配单位的方法（如果有不同种类的单位，则为一种或多种方法）。匹配方法必须符合下面的matches谓词，它是根据满足关系和自适应函数定义的。对于本文来说，抽象地定义两个单位匹配意味着什么就足够了。当且仅当存在适配时，才说单元u1匹配第二单元u2a1和a2，使得相对于a1的u1满足相对于a2的u2。D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173177这是由谓词匹配捕获的：匹配：P（Unit×Unit×Adapt×Adapt）u1，u2：单位;a1，a2：适应·（u1，u2，a1，a2）∈matches惠adapt（u1，a1）满意度adapt（u2，a2）一般来说，我们包括两个单位的适应。这与我们早期的模型[6]不同，其中只有一个单元（库单元）被调整。该通用模型反映了以下事实：在某些情况下，程序单元还可以包括自适应元素，例如参数。这种可适应的元素最常在匹配过程中引入，其中部分模块适应被重新翻转。2.2模块匹配匹配单元的框架被扩展以处理粗粒度的组件，这里称为模块。为了保持一般性，我们在这里不对模块进行正式建模;特别是不对模块的结构进行假设。[模块]我们将假设模块接口在模块提供的单元和模块需要的单元之间是不同的。 所需的单位在定义算法或数据细化的模块中以及定义自适应方案的模块中为了访问模块中的单元集，我们假设提供和要求的函数，它们返回模块提供和要求的单元集，已经定义：提供：模块→ F单元所需：模块→ F单元这些功能的确切性质将取决于特定模块的问题。对于一个mountat模块，它们将只返回模块中包含的单元集。然而，对于分层结构的模块，它们可以表示返回嵌套模块中包含的单元集的类似地，在面向对象编程中，函数可能需要遍历继承结构。我们在本文中模型支持两种模块自适应：适应个别单位和模块子集。Subseting返回一个子模块，它本身也是一个模块，遵守与其父模块相同的语法和语义约束[6]。我们将模块适配定义为由单个单元适配和一组模块单元组成。单元自适应描述了模块内的各个单元是如何自适应的;单个自适应用于确保自适应178D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173在整个模块中一致地应用-例如，它确保参数在整个模块中被实例化为相同的值。为了模块子集化的目的，模块单元的集合描述要包括什么模块单元。ModAdapt==Adapt× F单位我们假设有一个函数adapt将模块适配应用于模块，返回一个新模块。adapt：Module×ModAdapt→Module3搜索战术到目前为止，现有的检索工具的基础上规格匹配已被限制到执行一个单一的匹配步骤。 一般来说，这种检索工具需要单元查询的集合，并返回一组候选模块匹配（一些方法简单地返回匹配的模块，而其他方法也返回相应的模块适配）。我们将其概括为一系列模块匹配，其中来自一个匹配步骤的结果形成下一个匹配步骤的输入的一部分。 为此，我们定义了搜索策略的概念，它概括了模块匹配步骤的任何组合。搜索策略类似于交互式定理证明器中使用的证明策略[4]。证明策略旨在将多个简单的证明步骤组合成一个更复杂的步骤，从而使更平凡的步骤自动化。类似地，我们的目标是将多个单独的搜索步骤组合成单个复杂的搜索步骤。我们将搜索策略建模为一个函数，它接受一个仅指定的程序单元（查询）列表为了与交互式定理证明器的术语保持一致，我们将指定的程序单元列表每个解决方案包括一系列模块调整，一个单一的本地程序调整和一个新的子目标列表searchtac=^seqUnit→F（seqModAdapt×Adapt×seqUnit）搜索策略表示输入查询的一组解决方案每个解决方案都包括搜索历史，由一系列模块适配表示。每个解决方案还确定了必须应用于初始子目标的任何局部适应，以及引入新的子目标列表我们首先定义两种特殊策略，ID和FAIL。ID：searchtacFAIL：searchtacD. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173179应用ID策略总是成功的，返回一个平凡的结果，这使得子目标列表保持不变。平凡的结果由一个空的模块自适应列表（modulationadaptation）和一个平凡的局部自适应表示。x：seqUnit·ID x ={（相比之下，FAIL策略总是失败，对于任何初始子目标列表，返回一个空的结果集（）。x：seqUnit·FAIL x =我们描述的第一组策略对应于目前在基于特定匹配的检索工具中使用的简单一步策略[6]。这些策略中的每一个都需要一个库模块作为匹配过程的输入MATCHALL：Module→searchtacMATCHSOME：Module→searchtacMATCHONE：Module→searchtacMATCHALL搜索策略在用户需要具有一个或多个共享需求的多个单元（例如，用于操作基于相同底层类型的抽象数据类型的多个函数通过将各个需求指定为单独的单元子目标，并使用MATCHALL策略搜索库，只返回满足所有需求的模块。对于一个模块m，MATCHALL m定义了一个策略，给定一个子目标列表us，返回一组形式为（mas，a，usJ）的三元组对于每个三元组：• 序列mas包含单个模块适配ma，使得us中的每个单元（在它们已经相对于a适配之后）匹配由模块m提供的单元（相对于ma适配）;• 适配a对应于用户中的单位的适配;• 单元列表usJ对应于包含在m在它已经相对于ma被改编之后。MATCHALL策略具体如下：MATCHALL：Module→searchtac模块：模块;mas：序列ModAdapt;a：Adapt;us，usJ：序列单元·（mas，a，usJ）∈MATCHALL m us惠us/=模块适配器模块：ModAdapt·mas=模块适配器模块q：us·matches（u，q，π1ma，a）<$u∈π2ma<$usJ=required（unitsOf（adapt（m，ma）180D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173请注意，当子目标列表us为空（us=0）时，MATCHALL策略失败（返回空答案集）。这是必要的，以确保递归策略将终止一旦所有单位规格已实施。MATCHSOME策略是对严格的MATCHALL策略的放松。当指定的模块匹配某些（至少一个）子目标时，这种策略就成功了。这将包括由MATCHALL策略形成的比赛集MATCHONE策略使用户能够包括多个备选子目标，以找到单个所需的单元。当有许多等效的方式来指定一个单位时，这是很有用的;例如，用户可能需要一个用于操作列表s的单位，前提条件是该列表是非空的;这样的前提条件可以给定为#s= 0或s/=0。 （详情载于早期的论文[6];然而，像MATCHALL一样，我们添加了额外的条件，即当单元指定列表为空时，这些策略失败）。以下策略在组合多个搜索步骤时非常有用每个搜索步骤都可以引入新的子目标，这些子目标被附加到子目标列表的末尾。下面的策略为我们提供了一种方法，在为新添加的子目标寻找匹配之前，首先搜索最旧的子目标的匹配。因此，它们使广度优先搜索策略得以实施。MATCHFIRST：Module→searchtacMATCHFIRST：Module→searchtac如果子目标列表中存在某个前缀，使得该子序列中的所有单元都可以与库模块中的单元匹配，则MATCHFIRST搜索策略成功MATCHFIRST：模块→searchtac模块：模块;mas：序列ModAdapt;a：Adapt;us，usJ：序列单元·（mas，a，usJ）∈MATCHFIRm us惠我们1，我们2，我们3·us=我们1-我们2，我们1，我们3（mas，a，us3）∈MATCHALL m us1usJ=us2-us3我们计算得出的结论是，该预处理器必须满足无元素（us1=/n）的要求。这确保了如果初始子目标列表为空，则策略失败MATCHFIRST策略可以被定义为MATCHFIRST策略的一个特例，前缀us1包含一个等于子目标列表us的头部的元素，其余单元us2等于子目标列表的尾部。4战术到目前为止，我们已经重新定义了现有的单步模块匹配技术，其方式与一般搜索策略形式一致在本节中，我们将展示D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173181如何使用战术来构建更复杂的搜索策略。战术是一种机制，允许个人战术相结合。本节中定义的策略是基于最初提出用于交互式定理证明器的策略[4]。然而，它们的定义是非常不同的，因为我们不仅返回最终的子目标集，而且在搜索策略完成时返回搜索历史。战术总结如下，每个战术的更多细节如下：THEN：searchtac×searchtac→searchtac操 作 ： searchtac×searchtac→searchtac 附录：searchtac×searchtac→searchtac尝试：searchtac→searchtac完成：searchtac→searchtac重复：searchtac→searchtacTHEN策略实现搜索步骤的顺序组合。它结合了两个搜索步骤，第一个搜索步骤的结果，如果成功，则用作第二个搜索步骤的输入THEN：searchtac×searchtac→searchtac数据库1，t2：searchtac;x：seqUnit;mas：seqModAdapt;a：Adapt;us：seqUnit·（mas，a，us）∈（t1THEN t2）（x）惠Mass1，mas2：seqModAdapt;a1，a2：Adapt;us1：seqUnit·（mas1，a1，us1）∈t1（x）<$（（us1=mas=mas1a=a1）（（mas2，a2，us）∈t2（us1））n=mas1-mas2n（a1，a2）∈dommerge（a =merge（a1，a2）此战术计算第一个战术的结果。如果此策略返回子目标的空列表（即，所有规范都已实现），然后策略停止，返回第一个策略的答案否则，第一个策略返回的子目标列表解决方案中的子目标列表是第二个策略返回的列表。由THEN策略返回的模块调整序列对应于由第一策略返回的模块调整，该模块调整被附加到由第二策略返回的序列的前面。返回的局部自适应对应于两种策略的局部自适应的合并。这两个本地适配必须是可合并的，才能返回结果。OccupSE战术依次应用两种备选搜索战术。第二个策略仅在第一个策略没有返回任何解决方案时才应用。如果第一个搜索策略成功（返回一个非空的解集），则182D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173tactical返回其结果;否则执行第二搜索步骤并返回其结果集操作说明：searchtac×searchtac→searchtac数据库1，t2：searchtac;x：seqUnit;mas：seqModAdapt;a：Adapt;us：seqUnit·（mas，a，us）∈（t1Occupse t2）（x）惠（mas，a，us）∈t1（x）（mas，a，us）∈t2（x））APPEND策略类似于OSPINSE策略，但它执行更详尽的搜索。无论第一步是否成功，它都会返回第二步搜索的结果附录：searchtac×searchtac→searchtac数据库1，t2：searchtac;x：seqUnit;mas：seqModAdapt;a：Adapt;us：seqUnit·（mas，a，us）∈（t1APPEND t2）（x）惠（mas，a，us）∈t1（x）<$（mas，a，us）∈t2（x）使用APPEND策略，我们将上一节中应用于单个模块的基本策略推广到搜索库模块列表的策略。MATCHALL匹配：seq模块→searchtacMATCHSOME匹配：seq模块→searchtacMATCHONE匹配：seq模块→searchtacMATCHFIRST匹配：seq模块→searchtacMATCHFIRST匹配：seq模块→searchtac对于模块列表m1，.、.、mn，MATCHALLn定义为：MATCHALL（m1， . . ，mn）=^MATCHALL（m1）APPENDIX.. 附录匹配（mn）上面的其他一般策略也以类似的方式定义。TRY策略将尝试应用一个策略，但如果失败，它将保持子目标列表不变。t：searchtac·TRY t=t OASHSE ID只 有 当 策 略 匹 配 所 有 初 始 子 目 标 并 且 不 返 回 任 何 新 的 子 目 标 时 ，COMPRESSION搜索引擎：searchtac→searchtact：searchtac;x：seqUnit·（mas，a，us）∈COMPUTER（mas，a，us）∈txus=D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173183重复策略使我们能够重复地应用一种策略，在每个阶段将该策略应用于前一次应用的结果。它只返回最后一次重复的结果。重复t：searchtac·REPEAT t=（t THEN REPEAT t）重复IDREPEAT策略是递归定义的。它重复地将t应用于当前的子目标列表，当策略t失败或t返回一个空的子目标列表时终止。5例如作为概念验证，战术和战术已作为检索工具的扩展实施，该检索工具已用于支持CARE方法[7]。这些策略已经被应用到几个简单的例子中，包括一个对两个列表的长度求和的例子，我们将在本节中描述图1包含一个CARE程序，用于对两个列表的长度求和。 主片段sumlengths接受两个列表作为输入，并返回一个等于两个列表长度之和的自然数输出。 它是通过将片段长度应用于两个输入列表，然后将片段添加应用于结果来实现的。该程序包括片段长度和加法的规范，以及列表（自然数）和自然数的类型声明。类型Nat ==NtypeList==seqN和长度（在x，y：列表，在z：自然）postz=len（x）+len（y）：：= length（x）：：u：Nat; length（y）：：v：Nat; add（u，v）：：z：Nat;z.length（inx：List， outn：Nat）n = len（x）.add（inx，y：Nat， outz：Nat）后z = x + y。Fig. 1. 求两个列表在早期的论文[5]中，我们展示了如何仅使用库组件来实现长度和这是通过组合图1所示的两个库模块中的原语来完成的。二、NAT模块（图2（a）中显示的部分列表）定义了表示和操作自然数的原语。该模块包括两个自然数的加法和乘法操作，以及返回常量0和1的片段这些运算符使用标准算术运算符指定。184D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173模块 LIST[X]是模块N为typeList==seq X.nil（out y：X）post y= 1000。类型Nat==Nadd（inx，y：Nat， outz：Nat）后z = x + y。mult（inx，y：Nat，outz：Nat）postz = xy。head（inx：List，outy：X）前x/=0柱y =头x。tail（inx：List， outy：List）前x后zero（outz：Nat）postz = 0.一个（输出z：Nat）后z = 1。结束模块。(a) 自然数模后y=尾x。cons（inx：X， iny：List，outz：List）postz = x-y。append（inx，y：List， outz：List）后z = x-y。length（inx：List， outn：Nat）n = len（x）.结束模块。(b) 列表模块图二. 护理模块LIST模块（图2（b）中显示的部分列表）提供了创建和操作列表的原语。模块被参数化为单个列表元素可以采用的值集（X）。原语操作被提供用于：创建空列表;访问列表的头部;访问列表的尾部;将元素添加到列表的头部;连接两个列表;以及计算列表的长度。这种开发还需要两个适应模板。其中第一个是图3所示的模板FUN DECOMP，它让我们通过将问题分解为可以顺序解决的子问题来解决问题。主片段通过将函数g和h应用于输入参数来计算答案，然后通过应用第三个函数f来连接结果。该模板在这三个函数上进行了参数化，因此它可以适用于解决各种问题。图4中所示的第二个库模板DROP IINPUT允许通过调用具有少一个输入参数的辅助片段（frag1）来实现片段（main当要删除的输入参数不在主片段中时，可以应用此模板。这是有用的，因为规范匹配只匹配具有完全相同数量参数的片段，即使前置条件和后置条件相同。基于（手动）库的和长度开发从匹配与来自FUN DECOMP的主要片段的长度和（见图11）。（3）与以下--D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173185模板FUN DECOMP[X;Y;U;V;W;f：U→V→W;g：X→Y→U;h：X→Y→V]是main（inx：X，iny：Y，outw：W）前P（x，y）f（g（x，y），h（x，y））：：= gfrag（x，y）：：u：U;hfrag（x，y）：：v：V;ffrag（u，v）.ffrag（inu：U， inv：V，outw：W）f（u，v）= 0.gfrag（inx：X， iny：Y， outu：U）前P（x，y）postu = g（x，y）.hfrag（inx：X， iny：Y， outv：V）前P（x，y）postv = h（x，y）.结束模板。模板图三.顺序分解模板DROP I输入[X;Y;Z;P：X-B;f：X-Z]为fragmentmain（ inx：X， iny：Y， outz：Z）前P（x）f（x）=0：：= frag1（x）。fragmentfrag1（ inx：X， outz：Z）前P（x）f（x）= 0.结束模板。见图4。用于删除未使用的输入降低参数实例化：f<$→λu，v·u+v，g<$→λu，v·len（u）h<$→λu，v·len（v），P<$→λu，v·true在将这些实例化应用到模板之后，我们得到以下子目标（我们省略了琐碎的先决条件）：ffrag（inu：Nat， inv：Nat， outw：Nat）后w = u + v。gfrag（inx：List， iny：List， outu：Nat）186D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173postu = len（x）.hfrag（inx：List， iny：List， outv：Nat）D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173187postv = len（y）.通过为这三个片段寻找实现，开发工作继续进行。这些片段中的第一个可以使用精确匹配与来自NAT模块的片段添加进行然而，其他两个片段还不能尽管它们的后置条件与来自LIST模块的长度片段的后置条件相同，但gfrag和hfrag有一个额外的（未使用的）参数。这些片段可以通过应用DROP_INPUT模板来适配。对于gfrag，可以通过实例化参数来应用DROP I输入模板，如下所示：P<$→true，f<$→λu·len（u）返回以下仅指定的片段：frag1（inx：List， outu：Nat）postu = len（x）.片段frag1可以与来自LIST模板的片段长度匹配。为了完成示例，以类似的方式匹配片段hfrag。上述开发可以通过应用以下策略来自动化：COMPUTER（MATCHFIRST（FunDecomp）THEN REPEAT（MATCHFIRST）COMPUTER（MATCHFIRST（FunDecomp）THEN REPEAT（MATCHFIRST）COMPUTER（MATCHFIRST（FunDecomp））MATCHFIRST（DropInput）我们使用COMPUTER策略，以便只返回总匹配，即，其中返回子目标。这适用于使用THEN战术的子战术。这种策略的第一部分调用顺序分解模板将问题分解为更小的部分。然后我们反复尝试匹配第一个从数据结构模块中的一个单元得到子目标;或者如果失败，则从列表中的第一个子目标中删除输入。一般来说，当重复战术中的战术失败时，这个战术就终止了。当没有剩余的子目标时（即，所有要求都已满足），或者在子目标列表的头部存在与来自数据结构模块的单元不匹配的单元，并且不能移除任何输入参数。6相关工作有许多基于形式规范匹配的组件检索方法[12，8，15]。这些方法都符合我们的总体框架。对正式规定的成分的适应问题的关注较少然而，Penix和Alexander [10]以及SPARTACAS项目[9]的方法与CARE的组件适应方法相似。主要188D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173差异是在我们的方法中使用分支片段，用于定义通过对输入进行案例分析来组合组件的适配模板[5]。在我们的方法中，分支条件被明确定义，并且通常可以通过匹配过程来推导。这与相关的方法不同，其中分支条件是隐含的，并且通常需要人工交互来推导。Bracciali [2]描述了一种适应不匹配行为的方法。他们的方法有三个主要特征：组件接口;适配器规范;和适配器派生。组件接口包括指定的和需要的功能（通过签名），以及指定的行为（交互协议）。适配器规范指定了两个组件之间的互操作。适配器派生自动生成一个具体的适配器。适配器派生基于匹配函数签名;从这个意义上说，我们的方法更复杂。然而，他们的方法考虑了非功能行为，并且使用π演算来建模更复杂的连接器（架构）。Bosch [1]提出了一种与已经讨论过的方法略有不同的方法。博世没有定义可应用于任何组件的通用自适应技术，而是将自适应技术与特定组件相关联。这种方法使博世不仅可以定义类似于本文所讨论的适应性（所谓的黑盒适应性），还可以定义需要了解组件内部结构的白盒适应性。然而，目前还不清楚，这种方法可以与基于形式的检索。7结论在本文中，我们定义了一些通用的搜索策略，这些策略可用于使用正式指定的组件库来找到问题的解决方案。我们已经定义了基本战术，它使我们能够找到直接匹配，以及战术，使我们能够组合匹配步骤，从而使我们能够应用适应步骤的组合。这些策略是通用的，应该适用于各种正式的CBSD方法。通过定义策略，我们可以消除许多繁琐的适应步骤，让用户专注于开发中的创造性步骤。像交互式定理证明一样，搜索策略的使用允许用户在搜索过程中进行尽可能少或尽可能多的交互。按照他们的意愿或要求发展。本文中提出的工作代表了以前工作的重大进展这些策略已经通过扩展CARE工具进行了原型化，并在几个小例子上进行了测试。D. Hemer/Electronic Notes in Theoretical Computer Science 187（2007）173189确认这项工作由澳大利亚研究委员会发现资助DP0208046，规范汇编。感谢ColinFidge，他对本文的早期草稿提供了有用的反馈引用[1] Bosch，J.，叠加：一种组件适配技术，信息与软件技术4（1999），pp. 249-305[2] Bracciali，A.，A. Bragi和C. Canal，Adapting components with mismatching behaviors，in：J.Bishop，editor，Proceedings of CD185-199.[3] Brereton，P.和D.Budgen，基于事件的系统：问题的分类，IEEE计算机33（2000），pp. 54比62[4] 戈登，M。J.，A. J. Milner和C. P. Wadsworth，[5] Hemer，D.，构件自适应和组合的一种形式化方法，在：V。埃斯蒂维尔-卡斯特罗，编辑，ACSC'2005的会议记录259-266。[6] Hemer，D.和p.Lindsay，Specification-based retrieval strategies for module reuse，in：D.格兰特和L. Stirling，editors，Proc. of Australian Software Engineering Conference（ASWEC235-243.[7] Hemer，D. Lindsay，Template-based construction of verified software，IEE Proceedings SoftwareEngineering152（2005），pp. 2[8] Jeng，J.- J.和B. Cheng，Specification Matching for Software Reuse：A Foundation，in：Proceedingsof ACM Symposium on Software Reuse，1995，pp. 97比105[9] 莫雷尔湾和P. Alexander，SPARTACAS：Automating component reuse and adaptation，IEEETransactions on Software Engineering30（2004），pp. 587-600[10] Penix，J.和P. Alexander，Toward automated component adaptation，第九届软件工程和知识工程国际会议，1997年，pp.535-542[11]Penix，J.和P. Alexander，E.基于规范的构件检索，Automated Software Engineering6（1999），pp.139-170。[12] 佩里，D。和S.Popovich，Inquire：基于谓词的使用和重用，在：第八届基于知识的软件工程会议论文集，1993年，pp.144-151。[13] 普里托-迪亚斯河和F.P，Classifying software for reusability，IEEE Software4（1987），pp.6比16[14] Spivey，J.，“The Z Notation: a Reference Manual,” Prentice-Hall, New York,[15] Zaremski，A. M. J. Wing，Specification matching of software components，ACM Transactions onSoftware Engineering6（1997），pp. 333-369