软件学报

作者：左正康，孙欢，王昌晶，游珍，黄箐，王唱唱

单位：左正康，江西师范大学 数字产业学院, 江西 上饶 334006;江西师范大学 计算机信息工程学院, 江西 南昌 33002211,孙欢，江西师范大学 数字产业学院, 江西 上饶 33400602,王昌晶，江西师范大学 数字产业学院, 江西 上饶 334006;江西师范大学 计算机信息工程学院, 江西 南昌 33002203,游珍，江西师范大学 计算机信息工程学院, 江西 南昌 330022;网络化支撑软件国家国际科技合作基地 (江西师范大学), 江西 南昌 33002204,黄箐，江西师范大学 计算机信息工程学院, 江西 南昌 33002205,王唱唱，江西师范大学 数字产业学院, 江西 上饶 33400606

关键词：Isabelle/HOL;机械化验证;动态规划;命令式;VCG

基金：国家自然科学基金(62262031); 江西省自然科学基金(20232BAB202010, 20212BAB202018); 江西省教育厅科技项目(GJJ210307, GJJ210333, GJJ2200302); 江西省主要学科学术与技术带头人培养项目(20232BCJ22013)

动态规划是一种递归求解问题最优解的方法, 主要通过求解子问题的解并组合这些解来求解原问题. 由于其子问题之间存在大量依赖关系和约束条件, 所以验证过程繁琐, 尤其对命令式动态规划类算法程序正确性验证是一个难点. 基于动态规划类算法Isabelle/HOL函数式建模与验证, 通过证明命令式动态规划类算法程序与其的等价性, 避免证明正确性时处理复杂的依赖关系和约束条件, 提出命令式动态规划类算法程序设计框架及其机械化验证. 首先, 根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式, 并且基于递推关系式生成IMP (minimalistic imperative programming language)代码; 其次, 将问题规约、循环不变式和生成的IMP代码输入VCG (verification condition generator), 自动生成正确性的验证条件; 然后, 在Isabelle/HOL定理证明器中对验证条件进行机械化验证. 算法首先设计为命令式动态规划类算法的一般形式, 并进一步实例化得到具体算法. 最后, 例证所提框架的有效性, 为动态规划类算法的自动化推导和验证提供参考价值.

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期