Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation

Abstract

Mechanical theorem proving is especially advantageous on formal verification of algorithms manipulating complicated data structures. Some proof assistants such as Isabelle/HOL also enable users to extract executable code from verified specification, pushing the correctness assurance from algorithm level forward to code level. As a long-standing active research area, file comparison algorithms have extensive applications involving molecular biology, information processing, data retrieval and network security. In this paper, the formalization of fcomp, an efficient line oriented file comparison algorithm suggested by Miller and Myers, is modeled in the interactive theorem prover Isabelle/HOL. A small bug in fcomp's bound variable iteration is identified and the fixed algorithm's termination and correctness is established. Formal analysis of time complexity is also performed which coincides with the algorithm designers' own results. Using Isabelle's code generation tool a credible OCaml program is extracted further. This program's efficiency is compared to another hand-written OCaml program as well as to a C program through a set of experiments. Analysis results show that the generated program's efficiency still needs much improvement to be practically usable. Our work lays foundation for subsequent rigorous check of more file comparison algorithms.