基于公理的转换与测试：编译器优化的新思路

理论计算机科学电子笔记238（2009）17-33www.elsevier.com/locate/entcs基于公理的转换：优化和测试Anya Helene Bagge1 Magne Haveraaen2挪威卑尔根大学信息学系摘要程序员通常了解他们的程序的属性，这些属性没有在代码中显式表达-这些属性可能非常有用，例如，编译器优化和自动化测试。虽然这些信息有时会以正式或非正式的规范形式记录下来，但编译器和其他工具通常无法访问这些信息。然而，使用即将到来的C++标准中的概念和公理的思想，我们可以将公理嵌入程序代码。在本文中，我们勾勒出这些公理可以被解释为重写规则和测试神谕。重写规则与用户定义的转换策略一起使我们能够实现程序或特定于库的优化。关键词：重写规则，公理，优化，测试，C++，概念1介绍在即将到来的C++0x标准3[10]中，提出公理是新概念的构建。concepts的思想是让程序员对模板参数进行限制。例如，通用排序函数可以指定其参数应该是具有LessThanComparable元素的Indexable对象。如果没有概念，就只能继续使用索引和小于运算符，然后是编译器第1http://www.ii.uib.no/~anya/2http://www.ii.uib.no/~magne/3当我们在本文中提到1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.03818A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）17如果有人试图使用不合适的数据结构的排序功能，概念也可以组织在一个层次结构中-允许众所周知的代数概念以结构化的使用概念图，人们可以指定一个类或一组类满足给定的概念，也可以在概念的名称和签名与类的名称和签名之间进行映射例如，“我的（x >=y）'作为小于运算符”。拟议标准中的公理概念还处于早期阶段。它有一个定义的语法和一些例子，但行为的规范相当有限。编译器被允许，但不是必需的，根据公理用等价的表达式替换表达式在此之前，编译器几乎没有机会对用户代码进行假设，例如，它不能将内置运算符的许多简化这样的规则现在可以被描述为概念，但是仍然没有办法给编译器提示哪些公理可能是有用的，等式的哪一边是优选的，重写规则应该如何应用，等等。公理在软件系统中可以有多种用途(i) 记录有关泛型类和方法的模板参数的知识(ii) 证明一组公理意味着另一组公理-例如，属于概念C1的类可以用于需要概念C2（具有相同或更小的签名）的地方-以及程序验证-证明类满足其声明的(iii) 代码的语义保留重写，例如，为了优化的目的。(iv) 测试一个类是否满足它所声明的属性。第（i）项或多或少是今天提出的标准的立场;公理作为概念要求的结构化文档的形式第（ii）项可能不适用于C++，部分原因是C++的语法和语义很难分析，部分原因是许多需求不能表达为公理。 基于我们之前在C++用户定义重写规则[1]和基于公理的测试[12]方面的经验，我们将重点关注本文中的第（iii）和（iv）项。本文的其余部分组织如下。我们首先介绍公理，然后讨论公理在重写（第3节）和测试（第4节）中的应用。然后，我们将概述一些实施问题（第5节），并以讨论和结论结束（第5节）。（六）。A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）1719什么？“axiom”Identifier“（“ ParamDecls“）” AxiomBody-> AxiomDef“{”Axiom*“}”-> AxiomBodyExpressionStmt->公理“if”“（“Condition“）”ExpressionStmt->公理图1.一、建议的C++0x公理标准语法（SDF 2表示法）。第二条允许在公理参数上附加概念约束什么？“axiom”Identifier“（“ParamDecls“）”GroupClause？AxiomBody-> Declaration“：“{GroupName“，"}+-> GroupClause“{”（公理|语句）*“}”->公理体“assert”“（“表达式“）””;”->公理图二、我们的公理语法（SDF2表示法）。2概念和公理提出的C++公理标准语法如图1所示。每个公理定义可以包含多个公理，公理本身是带有“==”运算符的表达式语句例如，这里概念Monoid typical_Op，typical_T>：半群Op，T>{ Tidentity_element（Op）;public int findDuplicate（int findDuplicate）{op（x，identity_element（op））== x; op（identity_element（op），x）== x;} }个文件夹然后，我们可以指定一个类Vector满足Monoid概念，Vector：：plus4作为操作，Vector：：zero作为单位元素：concept_map Monoid Vector：：plus，Vector>{Vector identity_element（Vector：：plus）{return Vector：：zero;} }个文件夹对于我们的工作，我们选择了一个稍微不同的语法（见图2）。我们的语法扩展了原来的语法，允许公理群（见2.1节），4Vector：：plus是一个围绕加号操作的类包装器，这是方便地将其用作模板参数所必需的Vector：：plus（）是该类的一个对象，可用作函数，因为它有一个重载的（）-操作符。这是在C++中做事情的常用方法，我们将避免评论它的直观性。20A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）17GroupDef->声明“axiom_group”GroupName（GroupBody|“;”）->GroupDef“{”GroupDecl*“}”-> GroupBody“using”Name“;”-> GroupDeclAxiomDef-> GroupDeclTemplateSpec GroupDecl-> GroupDecl图三. Axiom Group的缩写。GroupDef定义或扩展一个命名的公理群。GroupName是一个标识符或限定（嵌套）名称。GroupBody列出了构成组的公理或公理组。 名称应该是公理、组或概念的名称通过允许在公理体中使用任何语句（用于测试，见Sect.4），并通过使用关键字assert标记实际公理。此外，我们允许在概念之外声明公理，以便可以将简单的公理直接附加到类，而不必为其声明概念和概念图。一个标准的C++概念映射只有当映射的类被用作一个模板参数，并被约束到一个概念时才是“活动的”。例如，在一个示例中，Vector只有在泛型代码中用作Monoid时才被认为是这限制了公理的使用，我们将假设概念图的存在意味着我们可以对图中的类和操作使用assert关键字可以更容易地在公理体中允许更广泛的它还简化了使公理可执行为测试代码（节。4）。在我们的语法中，上面的monoid概念变为：概念Monoid typical_Op，typical_T>：半群Op，T>{ Tidentity_element（Op）;公理Identity（Op op，T x）：简化{ assert（op（x，identity_element（op））==x）; assert（op（identity_element（op），x）== x）;} }个文件夹公理群“simplify”将恒等式公理识别为可用于简化规则，其中假设右侧比左侧更简单（资源密集度2.1公理群公理组用于识别哪些公理可用作重写规则，并区分不同类型的规则简化规则，重新排序规则，如结合性/交换性，或规则，应该是ap.A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）1721在转化过程的早期或晚期公理群可以使用公理群构造来定义（图3），或者在公理定义的group子句中列出群名。公理群定义是开放式的，可以在以后扩展下面axiom_group simplify {templatetype_0 p，type_0 T>使用Monoid Op，T>：：Identity;}模板声明具有通用量化monoid的操作符和类型的效果6using指令允许我们添加一个公理，来自给定概念的所有公理（例如，使用Monoid），或者来自另一个公理组的所有公理（使用我的simplify;）。公理也可以直接在公理群中定义。在群定义中列出公理等价于在公理定义中我们允许这两种可能性，以减少需要为一个简单的公理编写的代码量。我们建议对直接遵循公理的相当标准的分组使用公理定义-例如交换性-并对转换系统相关的分组使用单独的公理组定义一些建议的公理组是：ac- associative-commutative-一个表达式的简化- 右手侧优于左手侧;应终止重复propagate-跨表达式引入和传播属性3用公理从拥有公理到使用它们进行优化的跳跃并不遥远。建议的C++标准已经建议编译器可以使用公理来简化代码，并且已经存在基于ConceptGCC的基于公理的优化的概念证明[18类似的想法已经在TAMPR [3]和CodeBoost [1]等系统[5]这种标记在CASL [16]这样的规范和证明系统中也很重要[6]这在C++中运行得很好，但会导致额外的冗长。也许允许Monoid：：Identityas a shortcut.22A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）173.1基本重写让条件重写规则由匹配模式、替换模式和条件组成。如果条件总是为真，则可以省略。模式可以有变量（有时称为Meta变量，以区别于C++变量）。例如，考虑以下重写规则：g（f（x））→h（x）g（f（x））是匹配模式，h（x）是替换模式，x是变量。如果将该规则应用于表达式g（f（42）），则结果将是h（42）。替换模式中的变量应该是匹配模式和条件中变量的子集我们可以从由条件方程形成的任何公理导出重写规则，只需选择方程的一侧作为匹配模式，另一侧作为替换模式。如果我们选择相反的方式在简化规则的情况下，最好是单向的，但在交换规则的情况下，任何一个重写方向都可能有用。公理规则应用于表达式。如果我们希望将一个规则应用于整个程序（即，程序中的所有表达式），我们必须使用重写策略（下面讨论）。如果规则匹配且其条件为真，则规则可能成功，也可能失败。如果成功，则执行重写，我们完成。如果它失败了，如果我们应用一组规则，我们可以尝试其他规则，直到我们找到一个成功的规则。典型的重写策略会访问程序中的所有表达式，并重复应用规则，直到没有规则成功为止。重要的是要注意重写不仅仅是语法上的，它还考虑到表达式的类型和签名例如，从这个公理导出的int a，intb，int c，int d，int e，intf，int e，int e，int f，int e，intf，int f}将适用于表达式5 + 4，但不适用于4。2+6。9，它使用了浮动点加运算符。重写规则通常都有名字，在我们的系统中，这个名字来自公理的名字。规则名称与公理组名称共享相同的名称空间允许规则具有相同的名称-在这种情况下，它们形成一个组并将一起应用（即，以任意顺序进行审判，直到A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）1723成功或全部失败）。我们可以期望基于C++公理的重写系统是非一致的（即，以不同的顺序应用规则会产生不同的结果）和非终止性。重写策略与公理组一起提供了一个实用的解决方案，并允许我们仔细控制规则的应用3.2重写策略我们可以把优化工具建立在一个或几个固定的重写策略的基础上，并把每个策略与一个特定的公理组联系起来。例如，一个可能的默认优化策略是对程序树进行自下而上的简化（使用简化组），模ac规则。基于公理的优化可以通过编译器选项打开，-frewrite-rules.当然，我们可以做得用户定义的策略允许详细控制何时以及如何应用各种重写Boyle在TAMPR系统[3]中表明，需要这种控制来从重写规则中获得程序优化的许多目标基于现有的程序转换语言（如Replego [4]），我们可以在类似C++的语法中使用其策略构建结构（见图4），然后将我们的重写规则和策略编译为Replego代码，或者使用Replego解释器执行它们上述默认策略可以这样编码strategy（）{自下而上（重复）（简化||（ac&&simplify）;}其中，bottomup对程序树进行自底向上的遍历，repeat应用参数直到失败。 选择组合子||尝试它的左参数，如果左参数失败，则尝试它的右参数（对应于BIGGO中的<+），并且序列组合子&&按顺序应用其参数，并且仅当两者都成功时才执行（对应于BIGGO中的;）。这两个组应用程序简化，ac将在程序树中的当前位置应用实际重写规则见图图5是策略组合器的概述像简单的opt这样的策略可以作为编译器或转换工具选项提供给用户，例如。-frewrite-using=simple opt.24A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）17“策略”标识符“（“ParamDecls“）””;”-> StrategyDecl“策略”标识符“（“ParamDecls“）” StrategyBody->策略定义“{”Statement*“}”-> StrategyBody见图4。 策略定义的定义-这可以被解析为函数返回的定义类型为“策略”的值。StrategyBody中可用的策略语言的语句和操作符的有限集合（在图5中详细描述）。什么都不做假的什么都不做all（s）将s应用于当前节点的所有子节点S1||s2应用s1或s2，先尝试s1s1&&s2应用s1 然后s2a应用重写规则名称a应用公理群GG[a]应用公理群G中的任何规则arepeat（s）反复应用s直到失败。图五. 一些人建议使用策略组合子和内置策略。3.3与其他优化整合通常，优化规则可能仅应用于特定的抽象级别。例如，内联通常会暴露规则应用的一些机会，而隐藏其他机会。例如，在表达式a+f（b）中，我们可以内联或部分求值f，并计算出它返回一个零但是如果我们内联加号（例如，在向量加法的情况下），我们的规则将不再匹配。向策略语言公开一个内联接口将是非常有用的。在我们早期关于C++中用户定义规则的工作中，我们为简单函数添加了内联规则，以打开可能会失去的优化机会。例如，我们可能有一个规则，axiom GetElement（T a，T：：index_typei）：inline { assert（a[i] ==a.data[int（i）]）;}内联用户定义的[]-操作符的代码。由于这只是对[]实现的简单复制，因此让编译器表达式赋值的替换也可能有帮助。例如，考虑一个规则a*x+y== axpy（a，x，y），它将一个乘法和一个A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）1725添加到一个单一的操作。如果操作发生在不同的语句中（可能在代码中相距很远），我们可能无法判断该规则是否适用：向量a，b; a= 5 * a;b = a + b;但是如果在最后一个语句中替换了赋值给a的表达式，b = 5* a + b;我们也许能转变成一个更有效的b = axpy（5，a，b）;当处理向量和矩阵等大型数据结构时，像axpy这样的组合运算在像BLAS这样的数值库中很常见将这些规则与库一起提供，可以使程序员不必记住所有优化的特殊情况形式3.4属性和传播某些公理可能依赖于某些属性的满足。比如说，公理SortSort（T a）：简化{ if（sorted（a））sort（a）;}这个公理可以用来消除对已经排序的数据结构的不必要的排序程序员不太可能在数组刚排序后就要求再次排序，但是通过使用数据流分析，我们可以在整个程序中跟踪这类信息。要做到这一点，我们需要弄清楚数组何时排序（我们将简单地称之为“数组”，即使它也可以是任何有序的一个刚排序的数组被排序：公理Sorted（T a）：propagate{ assert（sorted（a）））;}此外，从数组中删除一个元素会导致数组仍然是排序的（好吧，至少对于我们的数组来说是这样公理SortedRemove（T a，T：：index_typei）：propagate{ if（sorted（a））26A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）17sort（a.remove（i））;}传播组用于识别可能适合于属性的数据流传播的公理任何像上面sorted这样的布尔谓词都可以用作传播属性。请注意，没有传播公理，我们就不能假设对象的任何修改（例如，调用一个非常量函数）都能保持它的属性。属性可以用作选择更有效算法的基础例如，公理公理SortedSearch（T a，T：：value_type e）：加速{ if（sorted（a））return（a，e）; return（a，e）}允许我们选择二进制搜索而不是线性搜索排序数组。我们为这个公理选择了公理群加速，因为它是一个与表达式简化略有不同的概念。可以想象，我们的优化策略可能会投入更多的工作来证明加速规则可以应用，而不是简化规则。跟踪对象的属性在数值编程中通常很有用，如果知道操作数具有特殊属性，例如矩阵中的对称性，某些操作可以大大加快4测试公理一旦我们有了公理并基于它们重写规则，我们就需要检查我们的实现是否满足公理。特别是，在我们将优化规则应用于程序之前，最好检查这些规则虽然公理可以用于形式化的程序验证，但这在通用语言中很难实现然而，我们可以采取更务实的方法，并使用公理作为测试的基础。使用公理作为测试预言机7是直接的遗憾的是，这种基于规范的测试为测试提供基本支持非常简单7测试预言是告诉你想要测试的操作的正确结果的东西。A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）1727实例化的（在概念映射之后）公理代码可用作可调用函数。然后，测试代码可以从测试程序或测试框架（如Java的JUnit [15]例如，参考Monoid的恒等公理，我们可以通过使用几个不同的整数值来调用它来测试它对整数是否成立for（inti = -2;i= 2; i++）{Monoid：：Identity（std：：multiplies int>（），i）;Monoid：：Identity（std：：plusint>（），i）;}在这里，std：：multiplies和std：：plus指的是内置运算符的预定义类包装器。它们是必要的，因为幺半群概念是如何定义的（以运算作为模板参数）4.1具有复杂测试码的公理用于测试的公理可以用任何（可计算）逻辑来编写因此，出于测试目的，在公理定义例如，我们可以声明两个数组相等，如果它们具有相同数量的元素，并且元素相等axiom ArrayEqual（Array a，Arrayb）{ bool eq = a.size（）== b.size（）; if（eq）for（int i=0; i a.size;++i）eq =a[i]== b[i];return（a ==b）;}第一行需要遍历数据集并积累有关其组成部分的信息。assert关键字有助于识别这个语句序列的哪一部分实际上是定义公理的测试。它可以被赋予它的C库含义-–允许assert具有附加参数甚至可能是有用的，例如，用于添加关于测试的额外信息。虽然在公理中只允许简单的表达式是很好的，但是能够为公理编写支持代码为我们提供了更多的表达能力。也有可能没有“helper”代码-28A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）17帮助器代码作为布尔函数，可能使简单的公理更加复杂。请注意，虽然上面的公理可能看起来微不足道，但正确地测试等式的实现是很重要的，以确保依赖于它的其他公理测试正确地工作。4.2测试异常行为同样有用的是将方法在特定条件下应该抛出异常作为公理public int findDuplicate（T x，T y）{ if（y.try { div（x，y）; assert（false）;}catch（DivisionByZero）{assert（true）;}}第一个断言测试没有抛出异常。第二个确认异常的预期捕获。如果不允许使用helper语句，则也需要封装此公理4.3测试限制以这种方式导出的测试显然只和它们所基于的公理一样好，如果公理是错误的，测试也会是错误的（尽管如果测试的实现是正确的，人们很可能会发现这一点基于等式和其他比较的测试依赖于正确执行的此外，如果一个等式的两边都是错误的，但给出了相等的结果，这将被忽视。然而，在实践中，使用不同的测试数据和多个公理的综合测试很可能会发现某些地方出错，即使环境与某些公理测试相违背。有效的测试需要良好的测试数据。这是我们在这里没有考虑到的这里的危险是程序员对什么构成好的测试数据的假设通常是错误的我们将在以后重新讨论这个问题（第二节）。（六）。5执行问题任何C++扩展实现所面临的最大障碍是实现对基础语言的支持现有的C++前端是A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）1729远远不能支持完整的C++，或者很难扩展，这使得对新语言特性进行原型设计的成本很高。对概念和公理的支持已经在实验性的ConceptGCC编译器中实现[9]。至少有一次尝试实现基于公理的重写（基于ConceptGCC和C++0x提案）[18]（他们注意到内部GCC表示上的规则应用和模式匹配确实非常具有挑战性）。我们还没有实现本文中描述的功能，但我们有以前的经验，实现基于公理的重写C++[1]和从公理导出C++测试[13]。在本节中，我们将简要地概述如何为C++实现原型5.1将公理转换为规则公理中使用的语法与实际的C++代码不同-人们写的这意味着要将规则应用于用户代码，我们必须首先根据概念图映射来翻译规则，内联任何概念图函数（如标识元素）。例如，恒等公理int x = x，int x = 0;为Vector：：plus实例化，Vector变为，Vector：：plus（）（x，identity_element（Vector：：plus（）== x;然后如果我们内联Vector：：plus（）和identity element（），我们得到x + Vector：：zero == x;这是我们希望在用户代码中看到的。C++前端的重载解析可用于确定规则中操作的签名（例如，整数加法，与浮点加法相对公理参数成为匹配模式中的变量。我们在之前的用户定义规则实现中使用了这个想法。请注意，当模板参数受到概念约束时，重写规则可以应用于通用模板代码。如果没有概念，在应用重写之前，您使用概念的模板代码已经用与公理相同的术语编写（例如，使用OP和Identity元素），因此必须做较少的工作来适应规则。30A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）175.2整体转型过程公理作为规则的整个处理过程可以如下进行。首先，我们需要对程序进行解析和语义分析，给出一个注释了类型和签名信息的抽象语法树（AST）前端然后从程序树中挑选出公理和策略定义然后，公理可以被编译为应用于概念级别的规则，并且在应用概念图之后，被编译为应用于类/用户级别的规则应用概念图后生成测试一旦规则可用，我们将根据内置或用户定义的优化策略应用它们。规则应用应该与内联和数据流分析相结合，以获得最大的收益。6讨论在程序中嵌入优化规则并不是一个新想法。CodeBoost [1]中的用户定义规则受到Glasgow Haskell编译器[14]中重写规则的启发然而，CodeBoost实现更高级条件重写规则在转换语言中是众所周知的，如Replego [4]和ELAN[2]，这两种语言也支持策略，并且通常来自术语重写。CodeBoost用户定义的规则仅限于重写，尽管我们从正式的代数规范中导出了优化规则，但规则的实际编码是手工完成的，并且直接与C++类相关。C++中的概念让我们弥合了规范之间的差距（用代数思想写的，如幺半群，场，环等）。并具体实现为C++类。用概念语法编写我们规范的相关部分，并使用公理，将使公理自动可供工具使用然而，这个难题中仍然缺少一块毫无疑问，已经有人在研究这个问题了。ConceptGCC [18]对基于公理的重写的支持比我们在这里做的更接近C++标准提案。[18]中的规则应用目前仅限于明确受概念约束的上下文（见第二节）。2），和转换被限制到一个单一的策略（最左最外还原）。我们的目标是建立一个基于概念的优化框架，A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）1731可能最终会取代编译器中特定类型的内置简化。我们并不打算与这一实现竞争，尽管我们希望我们的一些想法将对他们的工作有用这里描述的基于公理的规则限于对表达式进行操作，并且如果转换系统不能组合来自多个尽可能多地使用嵌套表达式在基于规则的优化和公共子表达式消除这样的优化之间存在权衡-复制一些公共子表达式可能会为规则应用程序打开，但也可能导致重复的我们最初的规则实验有相当有希望的结果。使用了Sophus数值库规范中的少量规则（以及一般简化规则）来优化Sophus的C++实现，提供了5一些加速是由于系统中的其他优化-将基于公理的规则应用于现有的程序代码可能不会给出很好的结果，因为程序员通常已经手工完成了许多相同的优化。我们预计，对于以前以高级风格编写的未优化程序，以及与性能敏感的库一起交付时，例如对于数值软件，使用公理作为测试的基础是从DAISTS [7]这样的系统中得知的与JUnit[15]等单元测试框架以及其他语言的xUnit系列框架相比这意味着人们可以很容易地用许多不同的数据值来测试一个公理全面的测试可以通过建立公理库和测试数据库，并针对所有合适的数据测试所有公理来完成。JUnit 4.4中提供的理论允许通用量化[17]，并且可以从本文中的测试代码中调用公理。JUnit 4.4还允许将可用的测试数据自动应用于测试。QuickCheck [5]是Haskell的一个测试系统，程序员可以将定律（如C++公理）作为Haskell函数来陈述。quickcheck测试函数生成随机测试值，并测试定律是否成立。条件定律也是允许的-在这种情况下，更多的测试值将根据需要生成，以有效地测试定律。Haskell中的代数数据类型使得生成随机数据结构变得相当简单，程序员可以提供生成器函数来微调数据生成。没有32A.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）17在Glasgow Haskell编译器中快速检查和重写规则之间的链接（如上所述）。分区测试是另一种测试方法，其中尝试将输入域划分为区域，并且仅测试来自每个区域的一个值（以及一些边界值）。但这并不一定比随机测试得到更好的结果[11]。分区和随机数据生成都可能需要C++程序员的帮助。这是一个应该进一步探索的领域，以便充分利用基于公理的测试。6.1结论即将到来的C++0x标准中引入的概念和公理是可能被证明对文档编制、自动测试和程序优化非常有用的语言特性为了充分利用公理，我们引入了一些额外的语言特性：• 公理组：根据公理的使用方式对公理进行• 用于指定如何以及何时使用基于公理的规则的策略• 可调用公理/公理组，使公理可用于测试• 可以根据公理传播并在公理条件下使用的属性在公理体中允许更广泛的陈述，并允许公理出现在概念之外，这给我们提供了一些额外的可用性好处。我们对自己和其他人以前在这一领域的工作的主要贡献确认感谢Valentin David对C++和语法的复杂性提供了有用的评论和帮助，并感谢裁判提供了许多有用的评论和提示。引用[1] 巴格岛S.和M. Haveraaen，在CodeBoost中使用用户定义的规则进行特定于域的优化，在：J.- L.Giavitto和P. - E. Moreau，editors，Proceedings of the 4th International Workshop on Rule-Based Programming（RULEA.H. Bagge，M.Haveraaen/电子笔记理论计算机科学238（2009）1733[2] Bor ov ansk y'，P.，C. Kir c hner，H. Kir c hner，P. E. Moreau和C. Ringeissen，ELAN概述，在：C.和H. Kirchner，editors，Proceedings of the 2nd International Workshop on RewritingLogic and its Applications（1998）.[3] Boyle，J.M.，T. Harmer和V. Winter，TAMPR程序转换系统：简化数值软件的开发，在：E。Arge ， A. M. Bruaset 和 H. P.Langtangen ， editors ， ModernSoftwarereToolsforScientificComputingg，Birkhauser，Boston，1997 pp.353-372.[4] Bravenboer，M.，K. T.卡勒贝格河Vermaas和E. Visser，Pungo/XT 0.16：转换系统，in：F.Tip和J.Hatterykirk，editors，PEPM[5] Claessen ， K. J. Hughes ， QuickCheck ： a lightweight tool for random testing of Haskellprograms，in：ICFP268-279。[6] Czarne cki，K.， 联合W. 阿 塞内茨克尔河 Gluüc k，D. Vande voorde和T. L. Verdhuizen，GeneRativeProgramming and Active Libraries，in：Selected Papers from the InternationalSeminar on Generic Programming（2000），pp.25比39[7] Gannon，J.，P. McMullin和R. Hamlet，数据抽象、实现、规范和测试，ACM Trans.Program。Lang.Syst.3（1981），pp. 211-223[8] Gottschling ， P. ， Fundamental algebraic concepts in concept-enabled C++ ， TechnicalReport TR639，Department of Computer Science，Indiana University（2006）.[9] Gregor，D.， J.Jüarvi，J. 西克湾Stroustrup，G. D.Reis和A. Lumsdaine，Concepts：LanguageSupport for Generic Programming in C++，in：OOPSLA291-310.[10] Gregor ， D. ， B. Stroustrup ， J.Siek 和 J.Widman ， Proposed words for concepts（ revision3 ） ， TechnicalReportN2421=07-0281 ， JTC1/SC22/WG21http://www.open-std.org/jtc1/sc22/wg21/.[11] Hamlet，D.和R. Taylor，Partition testing does not inspire confidence，IEEE Trans. Softw.Eng.16（1990），pp. 1402-1411.[12] Haveraaen，M.，机构，属性感知编程和测试，在：ACM SIGPLAN研讨会上图书馆为中心的软件设计（LCSD23[13] Haveraaen，M.和E.Brkic，Structured testing in Sophus，in：Norsk InformatikkonferanseNIK 2005（2005），pp.43比54[14] 琼 斯 ， S 。 P. ， A. Tolmach 和 T. Hoare ， Playing by the rules ： Rewriting as a practicaloptimization technique in GHC，in：R. Hinze，editor，2001 Haskell Workshop，Firenze，Italy.[15] Louridas，P.，JUnit：Unit testing and coding in tandem，IEEE Softw.22（2005），pp.12比15[16] Mosses，P.D、编辑，[17] Sa ， D. ， Theory-Infected ： Or How I Learned to Stop Worrying and Love UniversalQuantification，in：OOPSLA846-847[18] Tang，X. 和J. Jüarvi，Concept-basedoptimization， in：ACMSIGPLANSymposium on Library-Centric Software Design（LCSD'07）的出版物