Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)

TL;DR

This work addresses the challenge of specifying and verifying higher-order imperative programs by introducing Higher-Order Staged Specification Logic (HSSL), which extends Hoare-style reasoning to support multiple stages describing the behavior of unknown function-typed parameters and recursion. It presents formal semantics, a normalization/compaction procedure via biabduction, and a subsumption-based entailment framework with proven soundness, all integrated into an automated verifier named Heifer. The approach enables precise, modular specifications that avoid prematurely constraining higher-order arguments and supports automated proof via SMT, demonstrated on OCaml-like programs. The results indicate improved expressiveness and automation over state-of-the-art pre/post-based verifiers, with practical implications for verifying higher-order imperative code in real languages.

Abstract

Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification and reasoning, due to the use of yet-to-be-instantiated function parameters. One inherent limitation of existing specification mechanisms is its reliance on only two stages: an initial stage to denote the precondition at the start of the method and a final stage to capture the postcondition. Such two-stage specifications force abstract properties to be imposed on unknown function parameters, leading to less precise specifications for higher-order methods. To overcome this limitation, we introduce a novel extension to Hoare logic that supports multiple stages for a call-by-value higher-order language with ML-like local references. Multiple stages allow the behavior of unknown function-type parameters to be captured abstractly as uninterpreted relations; and can also model the repetitive behavior of each recursion as a separate stage. In this paper, we define our staged logic with its semantics, prove its soundness and develop a new automated higher-order verifier, called Heifer, for a core ML-like language.

Figures (13)

• Figure 1: A Simple Example
• Figure 2: Implementation of $\mathit{map\_incr}$ with a Summarized Specification from $\mathit{map}$
• Figure 3: Syntax of the Core Language and Staged Logics
• Figure 4: Semantics of Separation Logic Formulae
• Figure 5: Semantics of Staged Formulae

Theorems & Definitions (13)

• theorem thmcountertheorem: Soundness of Normalization
• proof
• Theorem 1: Soundness of Forward Rules
• proof
• theorem thmcountertheorem: Soundness of Entailment
• proof
• theorem thmcountertheorem: Soundness of Normalization
• proof
• Theorem 1: Soundness of Forward Rules
• proof