functional-programming - Coq 通过两种实现对阶乘程序进行验证

Question

我是 coq 的新手，我正在尝试验证 factorial 程序的功能。

根据我的理解，我应该做的是遵循标准的霍尔逻辑范例，从前置条件开始，计算循环不变式，并推理后置条件。像这样的事情:

{{ X = m }} 
{{  FOL 1 }}
Y ::= 1;;
{{  FOL 2   }}
WHILE !(X = 0) DO  
    {{ FOL 3    }}
    Y ::= Y * X;;
    {{ FOL 4   }}
    X ::= X - 1
   {{ FOL 5  }}
END
{{ FOL 6 }}
{{ Y = m! }}

这里是来自“一阶逻辑”的FOL标准。

然而，令我惊讶的是，似乎在用coq验证factorial程序时，常见的做法是定义以下两个函数fact 和 fact_tr:

Fixpoint fact (n:nat) :=
match n with
| 0 => 1
| S k => n * (fact k)
end.

Fixpoint fact_tr_acc (n:nat) (acc:nat) :=
match n with
| 0 => acc
| S k => fact_tr_acc k (n * acc)
end.

Definition fact_tr (n:nat) :=
fact_tr_acc n 1.

并证明这两个函数的等价性:

Theorem fact_tr_correct : forall n:nat,
fact_tr n = fact n.

我从here学到了这样的方法和 here .

这是我的问题:

1. 有人可以说明这种“基于平等”的验证方法背后的动机吗？它们在概念上仍然类似于基于标准霍尔逻辑的推理吗？

2. 不过，我可以使用 coq 遵循基于“标准”霍尔逻辑 的方法来验证 factorial 程序的正确性吗？通过指定前置条件、后置条件并归纳推理整个程序来表示。

Answer 1

请注意，Coq 程序的底层语言属于(依赖类型)函数式语言家族，而不是命令式语言。粗略地说，没有状态和语句，只有表达式。

“基于平等”方法背后的动机是，简单功能程序可以充当规范。 事实当然很简单——Coq 代表 definition of factorial通过其基本的递推关系。换句话说，事实是一个引用实现，即在本例中它是一个明显正确的实现。虽然 fact_tr_acc 是一种优化的，其正确性符合我们希望建立的规范。

是的，您仍然可以验证命令式factorial程序的正确性。例如。 Software Foundations series展示如何在 Coq 中编码命令式程序并使用 Hoare 逻辑验证其正确性。特别参见factorial exercise .