利用参数化集合约束定位 CLP 程序中的错误
编程语言
2007-05-23 v1
摘要
本文为约束逻辑编程（CLP）引入了一个参数化描述性方向类型框架。它提出了一种定位 CLP 程序中类型错误的方法，并展示了一个原型调试工具。主要技术是检查程序相对于类型规范的正确性。该方法基于将已知的逻辑程序正确性证明方法推广到参数化规范的情况。集合约束技术用于为（参数化）多态类型规范构建和检查验证条件。规范用项文法形式主义的参数化扩展来表达。证明了该方法的可靠性，并通过例子展示了支持所提方法的原型调试工具。本文是同一作者先前关于单态方向类型工作的实质性扩展。
引用
@article{arxiv.cs/0202010,
title = {Using parametric set constraints for locating errors in CLP programs},
author = {W. Drabent and J. Maluszynski and P. Pietrzak},
journal= {arXiv preprint arXiv:cs/0202010},
year = {2007}
}
备注
64 pages, To appear in Theory and Practice of Logic Programming