基于属性抽象的多变量程序专业化
Polyvariant Program Specialisation with Property-based Abstraction
摘要：
在本文中，我们表明，基于属性的抽象，一个既定的技术起源于软件模型检验，是一个灵活的方法，在标准的在线专业化算法控制程序专业化的多变量。专业化是一种程序转换，它根据限制其行为的给定约束来转换程序。多变量专业化是指生成同一程序代码的两个或多个专业化版本。在计算过程中，同一个程序点可以不止一次地达到，每种情况下都有不同的约束条件，而多变量专业化允许实现不同的专业化。基于属性的抽象使用属性的有限集合来定义谓词的抽象版本的有限集合，确保仅生成有限数量的专用版本。属性的特定选择对于多元性至关重要;太少的版本可能导致专业化不足，而太多的版本可能导致代码大小的增加，而没有相应的效率增益。使用实例，我们展示了基于属性的抽象专业化的灵活性，并讨论了其在控制流细化，验证，终止分析和基于维度的专业化。
英文摘要：
In this paper we show that property-based abstraction, an established technique originating in software model checking, is a flexible method of controlling polyvariance in program specialisation in a standard online specialisation algorithm. Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Polyvariant specialisation refers to the generation of two or more specialised versions of the same program code. The same program point can be reached more than once during a computation, with different constraints applying in each case, and polyvariant specialisation allows different specialisations to be realised. A property-based abstraction uses a finite set of properties to define a finite set of abstract versions of predicates, ensuring that only a finite number of specialised versions is generated. The particular choice of properties is critical for polyvariance; too few versions can result in insufficient specialisation, while too many can result in an increase of code size with no corresponding efficiency gains. Using examples, we show the flexibility of specialisation with property-based abstraction and discuss its application in control flow refinement, verification, termination analysis and dimension-based specialisation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
