文章详情

题名 · 作者 · 摘要 · 关键词 · DOI · 参考文献

背包问题求解的形式化验证

王旭，牟欣雨

（辽宁师范大学 数学学院，辽宁 大连 116029）

栏目：计算机技术 · 第 2026 年第 17 期 · 页码：41-46,52 · 2096-4706（2026）17-0041-07 · 中图分类号：TP311.1 · 文献标识码：A · DOI：10.19850/j.cnki.2096-4706.2026.17.008

摘要

背包问题是组合优化领域的经典NP难问题，其算法正确性对安全苛求系统具有关键意义。相较于难以覆盖所有输入场景的传统测试方法，形式化验证能够借助验证工具对程序正确性提供严格证明。针对背包问题的算法实现，文章基于ACSL（ANSI/ISO C规范语言）与Frama-C平台进行了形式化验证工作，重点围绕0-1背包和完全背包算法实现的可验证性展开，内容包括递归算法的逻辑函数建模、记忆化算法中状态缓存一致性的形式化规范、复杂循环不变式与帧条件的设计，以及算法功能等价性的严格证明。在Frama-C平台上的验证实践表明，0-1背包的28个验证条件，完全背包的41个验证条件全部验证通过，实现了这两种算法的正确性验证。

关键词

程序验证；ACSL；背包问题；递归算法；动态规划；Frama-C

参考文献

  1. [1] 李嘉鑫.带有冲突图的背包问题的精确算法的研究 [D].大连理工大学，2021.
  2. [2] Franken T T P，Neele T，Groote J F. The Autonomous Data Language-Concepts, Design and Formal Verification [J/OL].Theoretical Computer Science，2025：115560.https://www.sciencedirect.com/science/article/pii/S0304397525004980?via%3Dihub.
  3. [3] Frama-C. ANSI/ISO C Specification Language [EB/OL].[2025-03-20].http://frama-c.com/acsl.html.
  4. [4] Rocq. The Coq Proof Assistant [EB/OL].[2024-12-19].https://coq.inria.fr/.
  5. [5] Isabelle. The Isabelle/HOL Theorem Prover [EB/OL].[2024-12-19].https://isabelle.in.tum.de/.
  6. [6] 路红，王承毅，黄皓.基于数据分类的循环不变式自动生成 [J].计算机应用与软件，2023，40（1）：30-37.
  7. [7] 李薛剑，余韵.复杂内核数据结构程序形式化验证 [J].计算机系统应用，2023，32（11）：253-266.
  8. [8] Cassez F，Fuller J，Quiles H M A. Deductive Verification of Smart Contracts with Dafny [J].International Journal on Software Tools for Technology Transfer，2024，26（2）：131-145.
  9. [9] Lourenço C B，Pinto J S. Auto-active Verification of Distributed Systems and Specification Refinements with Why3-do [J/OL].Science of Computer Programming，2026，247：103352.https://www.sciencedirect.com/science/article/pii/S0167642325000917.
  10. [10] Meski A，Koutny M，Mikulski Ł，et al. Model Checking for Distributed Reaction Systems with Temporal-epistemic Properties [J].Natural Computing，2025，24（4）：1101-1117.
  11. [11] Schwarz M，Erhard J. The Digest Framework: Concurrency-sensitivity for Abstract Interpretation [J].International Journal on Software Tools for Technology Transfer，2024，26（6）：727-746.
  12. [12] Erwig M，Kumar P. Explainable Dynamic Programming [J/OL].Journal of Functional Programming，2021，31：e10.https://doi.org/10.1017/S0956796821000083.
  13. [13] Rai N，Grover J. Analysis of Crypto Module in RIOT OS Using Frama-C [J].The Journal of Supercomputing，2024，80（13）：18521-18543.
  14. [14] Frama-C. Frama-C WP Plugin [EB/OL].[2024-12-19].https://frama-c.com/wp.html.

作者简介

王旭（2002—），女，满族，辽宁宽甸人，硕士研究生在读，研究方向：自动推理、程序验证。