Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs

TL;DR

This paper introduces a novel static verification method for higher-order (C)LP programs using an abstract interpretation approach, enabling compile-time checking of higher-order assertions expressed via predicate properties.

Contribution

It presents a general approach for verifying higher-order assertions at compile time in (C)LP, including syntax, semantics, and an abstract interpretation-based analysis, with a prototype implementation.

Findings

Effective static verification of higher-order assertions demonstrated

Reduction of predicate properties to first-order properties for analysis

Prototype implementation shows practical applicability

Abstract

Higher-order constructs enable more expressive and concise code by allowing procedures to be parameterized by other procedures. Assertions allow expressing partial program specifications, which can be verified either at compile time (statically) or run time (dynamically). In higher-order programs, assertions can also describe higher-order arguments. While in the context of (constraint) logic programming ((C)LP), run-time verification of higher-order assertions has received some attention, compile-time verification remains relatively unexplored. We propose a novel approach for statically verifying higher-order (C)LP programs with higher-order assertions. Although we use the Ciao assertion language for illustration, our approach is quite general and we believe is applicable to similar contexts. Higher-order arguments are described using predicate properties -- a special kind of property which exploits the (Ciao) assertion language. We refine the syntax and semantics of these properties and introduce an abstract criterion to determine conformance to a predicate property at compile time, based on a semantic order relation comparing the predicate property with the predicate assertions. We then show how to handle these properties using an abstract interpretation-based static analyzer for programs with first-order assertions by reducing predicate properties to first-order properties. Finally, we report on a prototype implementation and evaluate it through various examples within the Ciao system.