Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms

Chengxi Yang, Shushu Wu, Qinxiang Cao

TL;DR

This work introduces a formal framework in Coq for naturally specifying and verifying sequential algorithms using a state relation monad defined over $\Sigma \times A \times \Sigma$, enabling imperative control with nondeterminism and customizable program states. It develops a Hoare logic tailored to this monad and a novel two-stage proof approach that separates natural reasoning from mechanical proof composition, improving modularity and readability. The framework is demonstrated by formalizing Depth-First Search and verifying Knuth–Morris–Pratt, illustrating the applicability to stateful, imperative algorithms and complex control flows. By unifying expressive type systems with flexible operational semantics, the approach offers a practical, modular path toward verified imperative algorithms with clearer alignment to natural proof structure, with artifacts available at the provided GitHub link.

Abstract

Current approaches for formal verification of algorithms face important limitations. For specification, they cannot express algorithms naturally and concisely, especially for algorithms with states and flexible control flow. For verification, formal proof based on Hoare logic cannot reflect the logical structure of natural proof. To address these challenges, we introduce a formal framework for naturally specifying and verifying sequential algorithms in Coq. We use the state relation monad to integrate Coq's expressive type system with the flexible control flow of imperative languages. It supports nondeterministic operations and customizable program states, enabling specifying algorithms at an appropriate level of abstraction. For verification, we build a Hoare logic for the monad and propose a novel two-stage proof approach that separates natural logical reasoning from mechanical composition. It reflects the logical structure of natural proof, enhancing modularity and readability. We evaluate the framework by formalizing the Depth-First Search (DFS) algorithm and verifying the Knuth-Morris-Pratt (KMP) algorithm.

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms

TL;DR

This work introduces a formal framework in Coq for naturally specifying and verifying sequential algorithms using a state relation monad defined over , enabling imperative control with nondeterminism and customizable program states. It develops a Hoare logic tailored to this monad and a novel two-stage proof approach that separates natural reasoning from mechanical proof composition, improving modularity and readability. The framework is demonstrated by formalizing Depth-First Search and verifying Knuth–Morris–Pratt, illustrating the applicability to stateful, imperative algorithms and complex control flows. By unifying expressive type systems with flexible operational semantics, the approach offers a practical, modular path toward verified imperative algorithms with clearer alignment to natural proof structure, with artifacts available at the provided GitHub link.

Abstract

Current approaches for formal verification of algorithms face important limitations. For specification, they cannot express algorithms naturally and concisely, especially for algorithms with states and flexible control flow. For verification, formal proof based on Hoare logic cannot reflect the logical structure of natural proof. To address these challenges, we introduce a formal framework for naturally specifying and verifying sequential algorithms in Coq. We use the state relation monad to integrate Coq's expressive type system with the flexible control flow of imperative languages. It supports nondeterministic operations and customizable program states, enabling specifying algorithms at an appropriate level of abstraction. For verification, we build a Hoare logic for the monad and propose a novel two-stage proof approach that separates natural logical reasoning from mechanical composition. It reflects the logical structure of natural proof, enhancing modularity and readability. We evaluate the framework by formalizing the Depth-First Search (DFS) algorithm and verifying the Knuth-Morris-Pratt (KMP) algorithm.
Paper Structure (21 sections, 27 equations, 1 algorithm)

This paper contains 21 sections, 27 equations, 1 algorithm.

Table of Contents

  1. Introduction
  2. Outline.
  3. State Relation Monad
  4. Monad Design
  5. Case Study: Formulating the DFS Algorithm
  6. Proof Framework
  7. Hoare Logic
  8. The Two-Stage Proof Approach
  9. Group 1: range.
  10. Group 2: partial match.
  11. Group 3: partial bound.
  12. Group 4: post loop.
  13. Related Work
  14. Conclusion
  15. Acknowledgments.
  16. ...and 6 more sections