Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Inferring Non-Failure Conditions for Declarative Programs

Michael Hanus

TL;DR

The paper tackles internal programming failures in declarative languages by automatically inferring non-failure conditions for partially defined operations. It introduces call types $CT(f)$ and in/out types $IO(f)$ within an abstract domain framework (e.g., depth-$k$ abstractions on $A$ with $oldsymbol{ abla}$), and then performs a fixpoint-based checking and refinement process to ensure that calls satisfy their inferred conditions. The method, implemented for Curry and FlatCurry, can handle literals, external operations, higher-order constructs, encapsulated failures, and configurable treatment of errors, demonstrating practical scalability across standard libraries with only modest iteration counts. The results show that most non-trivial non-fail conditions arise from a small subset of operations, enabling automatic verification without requiring extensive annotations, while still allowing programmer intervention to adapt code when necessary. This work advances automatic safety checks for declarative programs, with potential extensions to richer domains and integration with SMT-based reasoning for more expressive conditions.

Abstract

Unintended failures during a computation are painful but frequent during software development. Failures due to external reasons (e.g., missing files, no permissions) can be caught by exception handlers. Programming failures, such as calling a partially defined operation with unintended arguments, are often not caught due to the assumption that the software is correct. This paper presents an approach to verify such assumptions. For this purpose, non-failure conditions for operations are inferred and then checked in all uses of partially defined operations. In the positive case, the absence of such failures is ensured. In the negative case, the programmer could adapt the program to handle possibly failing situations and check the program again. Our method is fully automatic and can be applied to larger declarative programs. The results of an implementation for functional logic Curry programs are presented.

Inferring Non-Failure Conditions for Declarative Programs

TL;DR

The paper tackles internal programming failures in declarative languages by automatically inferring non-failure conditions for partially defined operations. It introduces call types and in/out types within an abstract domain framework (e.g., depth- abstractions on with ), and then performs a fixpoint-based checking and refinement process to ensure that calls satisfy their inferred conditions. The method, implemented for Curry and FlatCurry, can handle literals, external operations, higher-order constructs, encapsulated failures, and configurable treatment of errors, demonstrating practical scalability across standard libraries with only modest iteration counts. The results show that most non-trivial non-fail conditions arise from a small subset of operations, enabling automatic verification without requiring extensive annotations, while still allowing programmer intervention to adapt code when necessary. This work advances automatic safety checks for declarative programs, with potential extensions to richer domains and integration with SMT-based reasoning for more expressive conditions.

Abstract

Unintended failures during a computation are painful but frequent during software development. Failures due to external reasons (e.g., missing files, no permissions) can be caught by exception handlers. Programming failures, such as calling a partially defined operation with unintended arguments, are often not caught due to the assumption that the software is correct. This paper presents an approach to verify such assumptions. For this purpose, non-failure conditions for operations are inferred and then checked in all uses of partially defined operations. In the positive case, the absence of such failures is ensured. In the negative case, the programmer could adapt the program to handle possibly failing situations and check the program again. Our method is fully automatic and can be applied to larger declarative programs. The results of an implementation for functional logic Curry programs are presented.
Paper Structure (24 sections, 6 theorems, 18 equations, 3 figures, 1 table)

This paper contains 24 sections, 6 theorems, 18 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Functional Logic Programming and Curry
  3. Call Types and Abstract Types
  4. In/Out Types
  5. Inference and Checking of Call Types
  6. Initial Call Types
  7. Call Type Checking
  8. Iterated Call Type Checking
  9. Extensions
  10. Literals
  11. External operations
  12. Higher-order operations
  13. Encapsulation
  14. Errors as Failures
  15. Evaluation
  16. ...and 9 more sections

Key Result

theorem thmcountertheorem

Let $\mathit{Var}(e) \subseteq \mathit{dom}(\Gamma)$, $\Gamma \vdash e : \{ \overline{\Gamma_k \hookrightarrow a_k} \}$ be derivable by the inference rules in Fig. fig:inouttypes, and $\sigma$ be a substitution with $\sigma(x) \in \gamma(\Gamma(x))$ for all $x \in \mathit{Var}(e)$. If $\sigma(e)$ is

Figures (3)

  • Figure 1: Syntax of the intermediate language FlatCurry
  • Figure 2: Approximation of in/out types
  • Figure 3: Call type checking

Theorems & Definitions (11)

  • theorem thmcountertheorem
  • proof
  • corollary thmcountercorollary: Correctness of inferred in/out types
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • theorem thmcountertheorem
  • proof
  • corollary thmcountercorollary: Correctness of call type checking
  • ...and 1 more