Program Derivation and Mechanized Verification of Edit Distance Algorithm

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.