17.1. 概述🔗

mvcgen 的工作流程包括以下内容：

1. Monadic 程序根据 谓词转换器语义 重新解释。 WP 的实例决定了 monad 的解释。 每个程序都被解释为从任意 后置条件 到 最弱前置条件 的映射，以确保后置条件。 此步骤对于大多数用户来说是不可见的，但是想要使其 monad 能够与 mvcgen 一起使用的库作者需要理解它。

2. 程序由较小的程序组成。 Lean.Parser.Term.do : termdo 块中的每个语句都与谓词转换器关联，并且存在将这些语句与排序和控制流运算符组合的通用规则。 带有前置条件和后置条件的语句称为 Hoare Triple。 在程序中，每个语句的后置条件应该足以证明下一个语句的前置条件，并且循环需要指定的 loop invariant，这是一个在循环开始和每次迭代结束时必须为 true 的语句。 指定的 specation lemmas 将函数与指定它们的 Hoare 三元组关联起来。

3. 将一元程序的最弱前提条件语义应用于所需的证明目标会导致证明目标必须成立的前提条件。 任何缺失的步骤，例如循环不变量或证明语句的前提条件暗示其后置条件都会成为新的子目标。 这些缺失的步骤称为 验证条件。 mvcgen策略执行此转换，用其验证条件替换目标。 在此转换期间，mvcgen 使用规范引理来释放有关各个语句的证明。

4. 在提供循环不变量之后，许多验证条件实际上可以自动解除。 那些不能用特殊证明模式或普通Lean策略来证明的，取决于它们是用程序断言的逻辑表达还是用普通命题表达。