17.1. 概览🔗

mvcgen 的工作流程如下：

1. 按照谓词变换器语义重新解释单子程序。 WP 实例决定如何解释该单子。 每个程序都被解释为一个映射：它将任意后置条件映射为保证该后置条件成立的最弱前置条件。 大多数用户看不到这一步，但希望让自己的单子支持 mvcgen 的库作者需要理解它。

2. 由较小的程序组合成程序。 Lean.Parser.Term.do : termdo 块中的每条语句都与一个谓词变换器相关联，并有通用规则借助顺序执行和控制流运算符来组合这些语句。 带有前置条件和后置条件的语句称为霍尔三元组。 在程序中，每条语句的后置条件应足以证明下一条语句的前置条件；循环则要求指定循环不变式，即在循环开始时及每次迭代结束时都必须为真的命题。 指定的规约引理将函数与描述其行为的霍尔三元组关联起来。

3. 将单子程序的最弱前置条件语义应用于所需证明的目标，便得到为证明该目标而必须成立的前置条件。 任何缺失的步骤，例如循环不变式，或证明某条语句的前置条件蕴含其后置条件，都会成为新的子目标。 这些缺失的步骤称为验证条件。 mvcgen 策略执行这一变换，以验证条件替换原目标。 在此变换过程中，mvcgen 使用规约引理来解决关于各条语句的证明。

4. 给出循环不变式后，实践中许多验证条件都可以自动解决。 无法自动解决的验证条件，可根据其是用程序断言逻辑还是普通命题表示，使用专用证明模式或普通 Lean 策略来证明。