寻找一对一映射问题的Isabelle自动算法设计及验证

摘要

寻找一对一映射是通过归纳法解决问题的典型实例，在实例中涉及的映射可基于图结构进行分析，故对其进行研究有助于图结构算法的理解.该文结合Isabelle,基于Morgan求精的自动算法程序设计模型，通过形式化方法构造寻找一对一映射算法并进行验证.首先，利用Isabelle内置函数将寻找一对一映射问题的需求描述为规格；其次，根据Morgan求精规则对该规格进行求精，直至得到对应的IMP程序，在规则的使用中结合Isabelle引理库，提高程序求精的可靠度；最后，基于VCG自动生成寻找一对一映射IMP程序的验证条件，并通过Isabelle定理证明器进行机械验证，实现验证过程全自动且高可信.该算法的成功不仅有助于图算法的研究，而且对基于归纳法设计算法有借鉴意义.

关键词

寻找一对一映射 / Isabelle / Morgan求精 / 验证条件生成器

基金资助

国家自然科学基金(62462036); 江西省自然科学基金(20242BAB26017); 东华理工大学教育教学改革研究课题(DHJG-25-49)资助项目