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

Program Derivation and Mechanized Verification of Imperative Dynamic Programming Algorithms

作　　者：左正康[1,2] 孙欢[1] 王昌晶[1,2] 游珍 黄箐[2] 王唱唱 ZUO Zheng-Kang;SUN Huan;WANG Chang-Jing;YOU Zhen;HUANG Qing;WANG Chang-Chang(School of Digital Industry,Jiangxi Normal University,Shangrao 334006,China;School of Computer Information Engineering,Jiangxi Normal University,Nanchang 330022,China;National-level International S&T Cooperation Base of Networked Supporting Software(Jiangxi Normal University),Nanchang 330022,China)

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

出　　处：《软件学报》2024年第9期4218-4241,共24页Journal of Software

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

摘　　要：动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP(minimalistic imperative programming language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG(verification condition generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.As a recursive method for finding the optimal solution to a problem,dynamic programming mainly solves the original problem by first solving the subproblems and then combining their solutions.Due to a large number of dependencies and constraints among its subproblems,the validation procedure is laborious,and especially the correctness verification of imperative dynamic programming algorithms is a challenge.Based on the functional modeling and verification of dynamic programming algorithms Isabelle/HOL,this study avoids dealing with complex dependencies and constraints in proving correctness by verifying the equivalence of imperative dynamic programming algorithms and their programs.Meanwhile,a framework for the design of imperative dynamic programming algorithmic programs and their mechanized verification are proposed.First,according to the optimization method(memo method)and properties(optimal substructure property and subproblems overlapping property)of dynamic programming algorithms,the problem specification is described,the recursive relations are inductively derived,and the loop invariants are formally constructed.Then,the IMP(minimalistic imperative programming language)code is generated based on the recursive relations.Second,the problem specification,loop invariants,and generated IMP code are fed into VCG(verification condition generator)to generate the verification condition for correctness automatically.Additionally,the verification condition is then mechanically verified in the Isabelle/HOL theorem prover.The algorithm is initially designed in the general form of an imperative dynamic programming algorithm and further instantiated to obtain specific algorithms.Finally,the effectiveness of the proposed framework is validated by case studies to provide references for automated derivation and verification of dynamic programming algorithms.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]