中图分类号：TP311.1 文献标志码：A 文章编号：1001-3695（2026）03-001-0641-10doi：10.19734/j. issn.1001-3695.2025.08.0277

0 引言

程序验证1是一个确保程序行为符合预期的过程，通过形式化方法来证明程序符合其（试读）...