文件比较算法fcomp在Isabelle/HOL中的验证

来源：软件学报杂志2017年第2期北京时间：

作者：宋丽华,王海涛,季晓君,张兴元

单位：宋丽华，解放军理工大学 指挥信息系统学院, 江苏 南京 21000711,王海涛，解放军理工大学 信息管理中心, 江苏 南京 21001402,季晓君，解放军理工大学 指挥信息系统学院, 江苏 南京 21000703,张兴元，解放军理工大学 指挥信息系统学院, 江苏 南京 21000704

摘要：基于机器定理证明的形式验证技术不受状态空间限制，是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.文件比较算法（file comparison algorithm）是一类成员众多，应用极为广泛，跨越生物信息学、情报检索、网络安全等多个应用领域的基础算法.在交互式定理证明器Isabelle/HOL中对Miller和Myers在1985年提出的基于行的文件比较算法fcomp做了形式化，改正了算法关于边界变量迭代的一个小错误，证明了改正后算法的可终止性和正确性；对算法时间复杂性做了完全形式化的分析，印证了算法的非形式化分析结论，为今后更多文件比较算法的形式验证提供了可供借鉴的经验.

关键词：文件比较算法;fcomp;交互式定理证明;Isabelle/HOL

基金资助：江苏省自然科学基金（BK20130070）