-
题名命令式动态规划类算法程序推导及机械化验证
- 1
-
-
作者
左正康
孙欢
王昌晶
游珍
黄箐
王唱唱
-
机构
江西师范大学数字产业学院
江西师范大学计算机信息工程学院
网络化支撑软件国家国际科技合作基地(江西师范大学)
-
出处
《软件学报》
EI
CSCD
北大核心
2024年第9期4218-4241,共24页
-
基金
国家自然科学基金(62262031)
江西省自然科学基金(20232BAB202010,20212BAB202018)
+1 种基金
江西省教育厅科技项目(GJJ210307,GJJ210333,GJJ2200302)
江西省主要学科学术与技术带头人培养项目(20232BCJ22013)。
-
文摘
动态规划是一种递归求解问题最优解的方法,主要通过求解子问题的解并组合这些解来求解原问题.由于其子问题之间存在大量依赖关系和约束条件,所以验证过程繁琐,尤其对命令式动态规划类算法程序正确性验证是一个难点.基于动态规划类算法Isabelle/HOL函数式建模与验证,通过证明命令式动态规划类算法程序与其的等价性,避免证明正确性时处理复杂的依赖关系和约束条件,提出命令式动态规划类算法程序设计框架及其机械化验证.首先,根据动态规划类算法的优化方法(备忘录方法)和性质(最优子结构性质和子问题重叠性质)描述问题规约、归纳递推关系式和形式化构造出循环不变式,并且基于递推关系式生成IMP(minimalistic imperative programming language)代码;其次,将问题规约、循环不变式和生成的IMP代码输入VCG(verification condition generator),自动生成正确性的验证条件;然后,在Isabelle/HOL定理证明器中对验证条件进行机械化验证.算法首先设计为命令式动态规划类算法的一般形式,并进一步实例化得到具体算法.最后,例证所提框架的有效性,为动态规划类算法的自动化推导和验证提供参考价值.
-
关键词
Isabelle/HOL
机械化验证
动态规划
命令式
VCG
-
Keywords
Isabelle/HOL
mechanized verification
dynamic programming
imperative
verification condition generator(VCG)
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-