基于集合约束的参数化正则类型推断
Towards Parameterized Regular Type Inference Using Set Constraints
摘要:
我们提出了一种方法来推断\emph{parameterized regular types}的逻辑程序的解决方案的限制系统的有限地面Herbrand条款(集约束系统)。这样的参数化正则类型通过扩展类型定义中的参数的范围来泛化\emph{parametric}正则类型,使得这样的参数可以关联不同谓词的类型。我们提出了一些增强的过程中解决的约束系统,提高推断的类型描述的精度。由此产生的算法,连同一个程序,以建立一套约束系统的逻辑程序,产生一个程序分析,推断更紧密的安全近似的成功类型的程序比以前的可比工作,提供了一个新的和有用的效率与精度的权衡。实验结果证明了分析的可行性。
英文摘要:
We propose a method for inferring \emph{parameterized regular types} for logic programs as solutions for systems of constraints over sets of finite ground Herbrand terms (set constraint systems). Such parameterized regular types generalize \emph{parametric} regular types by extending the scope of the parameters in the type definitions so that such parameters can relate the types of different predicates. We propose a number of enhancements to the procedure for solving the constraint systems that improve the precision of the type descriptions inferred. The resulting algorithm, together with a procedure to establish a set constraint system from a logic program, yields a program analysis that infers tighter safe approximations of the success types of the program than previous comparable work, offering a new and useful efficiency vs. precision trade-off. This is supported by experimental results, which show the feasibility of our analysis.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。