基于行的文件比較算法fcomp改正
大小：1.99 MB 人氣： 2018-01-03 需要積分：2
標簽：
基于機器定理證明的形式驗證技術不受狀態空間限制，是保證軟件正確性、避免因潛在軟件缺陷帶來嚴重損失的重要方法．文件比較算法（file comparison algorithm）是一類成員眾多，應用極為廣泛，跨越生物信息學、情報檢索、網絡安全等多個應用領域的基礎算法在交互式定理證明器Isabelle/HOL中對Miller和Myers在1985年提出的基于行的文件比較算法fcomp做了形式化，改正了算法關于邊界變量迭代的一個小錯誤，證明了改正后算法的可終止性和正確性：對算法時間復雜性做了完全形式化的分析，印證了算法的非形式化分析結論，為今后更多文件比較算法的形式驗證提供了可供借鑒的經驗．
?
非常好我支持^.^
(0) 0%
不好我反對
(0) 0%