代码之家 › 专栏 › 技术社区 › lllllllllllll

通过两个实现对阶乘程序进行Coq验证

verification coq functional-programming

2

lllllllllllll · 技术社区 · 7 年前

我是新手 coq 我正在验证 factorial 程序

根据我的理解,我应该做的是遵循标准 Hoare Logic 范例,从前置条件开始,描绘循环不变量,并推理后置条件。类似这样:

{{ 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公司 ,常用的方法是定义以下两个函数 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 。

所以我的问题是:

有人能说明这种“基于平等”的验证方法背后的动机吗?它们在概念上是否仍然与标准相似 霍尔逻辑 基于推理?
还有,我可以用 coq公司 验证 阶乘的 遵循“标准”的程序 Hoare logic 基于的方法?也就是说,通过指定前置条件、后置条件和归纳推理来完成整个程序。

1 回复 | 直到 7 年前

1

2

Anton Trunov 7 年前

请注意,Coq程序的基础语言属于(依赖类型的)系列 功能的 语言,而不是命令式语言。大致上,没有状态和语句,只有表达式。

“基于平等”方法背后的动机是 易于理解的 功能程序可以用作 规格说明 。和 fact 当然很简单——这是Coq代表 definition of factorial 通过其基本递推关系。换句话说, 事实 是参考实现,即在这种情况下,它显然是正确的实现。虽然 fact_tr_acc 是一个优化的,其正确性与我们希望建立的规范有关。

是的,您仍然可以验证命令的正确性 factorial 程序E、 g.该 Software Foundations series 演示如何在Coq中编码命令式程序,并使用霍尔逻辑验证其正确性。具体参见 factorial exercise 。