Computer Science

CLC number: TP311

Program Derivation and Mechanized Verification of Edit Distance Algorithm

编辑距离算法的程序推导与机械化验证

¹ School of Artificial Intelligence, Jiangxi Normal University, Nanchang 330022, Jiangxi, China
² National-Level International S&T Cooperation Base of Networked Supporting Software, Jiangxi Normal University, Nanchang 330022, Jiangxi, China
³ School of Information Engineering, Jiangxi University of Technology, Nanchang 330098, Jiangxi, China

^† Corresponding author. E-mail: This email address is being protected from spambots. You need JavaScript enabled to view it.

Received: 28 May 2025

Abstract

Edit distance is an algorithm to measure the difference between two strings, usually represented as the minimum number of editing operations required to transform one string into another. The edit distance algorithm involves complex dependencies and constraints, making state management and verification work tedious. This paper proposes a derivation and verification method that avoids directly handling dependencies and constraints by proving the equivalence between the edit distance algorithm and existing functional modeling. First, the derivation process of edit distance algorithm mainly includes 1) describing problem specifications, 2) inductively deducing recursive relations, 3) formally constructing loop invariants using the optimization theory (memorization technology and optimal decision table) and properties (optimal substructure property and subproblems overlapping property) of the edit distance algorithm, 4) generating the Minimalistic Imperative Programming Language (IMP) code based on the recursive relations. Second, the problem specification, loop invariants, and generated IMP code are input into Verification Condition Generator (VCG), which automatically generate five verification conditions, and then the correctness of edit distance algorithm is verified in the Isabelle/HOL theorem prover. The method utilizes formal technologies and theorem prover to complete the derivation and verification of the edit distance algorithm, and it can be applied to linear and nonlinear dynamic programming problems.

摘要

编辑距离是一种用于衡量两个字符串差异的算法，通常表示为将一个字符串变换为另一个字符串所需的最少编辑操作数。该算法涉及复杂的依赖关系与约束，导致状态管理和正确性验证过程繁琐。本文提出了一种程序推导与验证方法，通过与已有函数建模方法的等价性证明，避免了直接处理复杂依赖和约束的问题。首先，编辑距离算法的推导过程主要包括：(1)描述问题规约；(2)递归关系的归纳推导；(3)基于优化理论(记忆化技术与最优决策表)及编辑距离算法性质(最优子结构性质与子问题重叠性质)形式化构造循环不变量；(4)根据递归关系生成IMP(极简命令式编程语言)代码。其次，将问题规约、循环不变量以及生成的IMP代码输入到VCG(验证条件生成器)中，自动生成5个验证条件，并在Isabelle/HOL定理证明器中完成编辑距离算法的正确性验证。该方法综合运用了形式化技术与定理证明工具，实现了编辑距离算法的程序推导与验证工作，具备良好的可迁移性，可推广应用于线性和非线性的动态规划类问题。