命令式动态规划类算法程序推导及机械化验证

作     者：左正康 孙欢 王昌晶 游珍 黄箐 王唱唱 ZUO Zheng-Kang;SUN Huan;WANG Chang-Jing;YOU Zhen;HUANG Qing;WANG Chang-Chang

作者机构：江西师范大学数字产业学院江西上饶334006 江西师范大学计算机信息工程学院江西南昌330022 网络化支撑软件国家国际科技合作基地(江西师范大学)江西南昌330022 

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

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2024年第35卷第9期

页      码：4218-4241页

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

主 题 词：Isabelle/HOL 机械化验证 动态规划 命令式 VCG 

学科分类：08[工学] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.13328/j.cnki.jos.007134

馆 藏 号：203134119...