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

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

Mechanized Verification and Program Derivation of Imperative Dynamic Programming Algorithms

Dynamic programming is a recursive method for finding the best solution to a problem by first solving the subproblems and then combining their solutions to solve the original problem. Because of the large number of dependencies and constraints between its subproblems, the validation procedure is laborious, especially for the imperative dynamic programming algorithms. We avoid dealing with complex dependencies and constraints when proving correctness by proving the equivalence of imperative dynamic programming algorithms and their programs, which is based on the functional modeling and verification of dynamic programming algorithms Isabelle/HOL. It is proposed a framework for the design of imperative dynamic programming algorithmic programs and their mechanized verification. We first describe the problem specification,inductively derive the recursive relations, and formally construct the loop invariants using the optimization method (memo method) and properties (optimal substructure property and subproblems overlapping property) of the dynamic programming of algorithms, and then generate the IMP (Minimalistic Imperative Programming Language) code based on the recursive relations. Second, the problem specification, loop invariants, and generated IMP code are fed into VCG (Verification Condition Generator), which generates the verification condition for correctness automatically; the verification condition is then mechanically verified in 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. At the end of the article, the effectiveness of the proposed framework is validated through case studies, providing valuable reference for the automated derivation and verification of dynamic programming algorithms.