约束逻辑程序的反向分析

程序开发中一个反复出现的难题是理解如何复用第三方开发的代码。在约束逻辑编程的语境下，这一问题部分归结为弄清如何查询该程序。如果逻辑程序没有提供任何文档，那么程序员只能通过一种非正式的方式进行查询实验，或跟踪程序的控制流（反向）来推断断言在何种调用模式下才能避免实例化错误。本文提出了一种抽象解释方案，用于自动化后者技术。本文所描述的分析能够推断出的模态属性，如果这些属性在初始查询中被满足，则保证该程序和查询永远不会产生任何模态或实例化错误。讨论了该分析的其他应用。本文解释了如何使用具有某些计算属性（即浓缩）的抽象域来反向（从右到左）追踪控制流，以推断初始查询的有用属性。给出了正确性论证并报告了实现情况。