In strongly-typed languages, types are verified at compile time, while dynamically typed languages, such as Prolog, perform type consistency checks entirely at run-time. Extending dynamic languages with assertions allows expressing both classical types and more general properties, providing high expressiveness, but at the cost of run-time overhead. Abstract interpretation allows safely approximating such program properties at compile time, which has been used to reduce the number of properties that require run-time checks, while still reporting unverified properties that can guide further static analyses, testing, or domain refinement. In this work, we first study how to selectively integrate the run-time semantics of assertion properties into a multivariant, top-down, goal-directed abstract interpretation algorithm. We then show how multiple inferred calling patterns can be exploited to reduce the number of properties that must be checked at run-time, thus minimizing the overhead. Finally, we report on an implementation of our approach in the Ciao system and provide performance results supporting that better results can be obtained than with the previously reported techniques.

翻译：在强类型语言中，类型在编译时得到验证，而Prolog等动态类型语言则完全在运行时执行类型一致性检查。通过断言扩展动态语言，既能表达经典类型，也能表达更一般的属性，从而提供高表达能力，但代价是增加了运行时开销。抽象解释允许在编译时对这些程序属性进行安全近似，这已被用于减少需要运行时检查的属性数量，同时仍能报告未经验证的属性，从而指导进一步的静态分析、测试或领域细化。在本工作中，我们首先研究如何将断言属性的运行时语义有选择地集成到多变量、自顶向下、目标导向的抽象解释算法中。随后，我们展示了如何利用多个推断出的调用模式来减少必须在运行时检查的属性数量，从而最小化开销。最后，我们报告了该方法在Ciao系统中的实现，并提供了性能结果，证明该方法能获得优于先前报道技术的效果。