基于行的文件比較算法fcomp改正

　　 基于機(jī)器定理證明的形式驗(yàn)證技術(shù)不受狀態(tài)空間限制，是保證軟件正確性、避免因潛在軟件缺陷帶來(lái)嚴(yán)重?fù)p失的重要方法．文件比較算法（file comparison algorithm）是一類成員眾多，應(yīng)用極為廣泛，跨越生物信息學(xué)、情報(bào)檢索、網(wǎng)絡(luò)安全等多個(gè)應(yīng)用領(lǐng)域的基礎(chǔ)算法在交互式定理證明器Isabelle/HOL中對(duì)Miller和Myers在1985年提出的基于行的文件比較算法fcomp做了形式化，改正了算法關(guān)于邊界變量迭代的一個(gè)小錯(cuò)誤，證明了改正后算法的可終止性和正確性：對(duì)算法時(shí)間復(fù)雜性做了完全形式化的分析，印證了算法的非形式化分析結(jié)論，為今后更多文件比較算法的形式驗(yàn)證提供了可供借鑒的經(jīng)驗(yàn)．
?