Lean 4.22：验证命令式程序的全新基础设施
2025-07-07
Lean 4.22 版本即将推出一个令人兴奋的新特性：用于证明命令式程序属性的全新验证基础设施。文章以一个简单的例子——判断列表中是否存在两个整数之和为零——展示了该特性的使用方法，并将其与 Dafny 和 Verus 等类似工具进行了比较。新框架 Std.Do 基于 Hoare 三元组，并结合了 mvcgen 和 grind 策略，极大地简化了命令式程序的验证过程，即使对于包含循环和提前返回的复杂情况，也能轻松应对。相比于依赖外部 SMT 求解器的自动化系统，Lean 的交互式证明方式更可靠、更易于调试和维护，这使得 Lean 在实际的程序验证任务中具有显著优势。
开发
命令式编程