Hiord#: 用于 Higher-Order (C)LP 程序的规范与验证方法
编程语言
2025-09-11 v2
摘要
Higher-order 构造通过允许程序参数化其他程序来实现更具表达性和简洁性的代码。断言允许表达部分程序规范，可在编译时（静态）或运行时（动态）进行验证。在 higher-order 程序中，断言也可以描述 higher-order 参数。尽管在 (constraint) 逻辑编程 ((C)LP) 中，对 higher-order 断言的运行时验证已有一些研究，但编译时验证仍相对未探索。在本文中，我们提出了一种用于静态验证具有 higher-order 断言的 higher-order (C)LP 程序的新方法。虽然我们使用 Ciao 断言语言进行示例，但我们的 метод是相当通用的，我们认为适用于类似的上下文。通过 predicate properties——一种特殊类型的属性，它们利用 (Ciao) 断言语言——来描述 higher-order 参数。我们细化了这些属性的语法和语义，并引入一种抽象准则来确定在编译时是否符合 predicate property，基于一种比较 predicate property 与 predicate 断言的语义顺序关系。随后，我们展示了如何使用基于抽象解释的静态分析器来处理这些属性，将 predicate properties 简化为 first-order properties。最后，我们报告了一个原型实现并通过 Ciao 系统中的各种示例进行评估。
引用
@article{arxiv.2507.17233,
title = {Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs},
author = {Marco Ciccalè and Daniel Jurjo-Rivas and Jose F. Morales and Pedro López-García and Manuel V. Hermenegildo},
journal= {arXiv preprint arXiv:2507.17233},
year = {2025}
}
备注
Accepted for publication in Theory and Practice of Logic Programming (TPLP)