|
|||||
|
|
| 算法的形式化推导与基于Isabelle的自动化验证 | |
| 作者姓名： | 齐蕾蕾 杨庆红 游颖 |
| 作者单位： | 江西师范大学计算机信息工程学院 |
| 摘 要： | 可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性. |
| 本文献已被 CNKI 等数据库收录！ | |