Assertion-based debugging of higher-order (C)LP programs

Abstract

Higher-order constructs extend the expressiveness of firstorder
(Constraint) Logic Programming ((C)LP) both syntactically
and semantically. At the same time assertions have
been in use for some time in (C)LP systems helping programmers
detect errors and validate programs. However,
these assertion-based extensions to (C)LP have not been
integrated well with higher-order to date. This paper contributes
to filling this gap by extending the assertion-based
approach to error detection and program verification to the
higher-order context within (C)LP. We propose an extension
of properties and assertions as used in (C)LP in order
to be able to fully describe arguments that are predicates.
The extension makes the full power of the assertion language
available when describing higher-order arguments. We provide
syntax and semantics for (higher-order) properties and
assertions, as well as for programs which contain such assertions,
including the notions of error and partial correctness.
We also discuss several alternatives for performing run-time
checking of such programs.