通过两种实现对阶乘程序的Coq验证
通过两种实现对阶乘程序的Coq验证
提问于 2018-03-25 21:39:21
我是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标准。
然而，令我惊讶的是，在用factorial验证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.所以我的问题是：
- 有人能说明这种“基于平等”的验证方法背后的动机吗？它们在概念上是否仍然与基于
Hoare Logic的标准推理相似？ - 不过，我是否可以使用
coq来验证基于“标准”Hoare logic方法的factorial程序的正确性？通过指定前提条件、后置条件和归纳推理等方法对整个程序进行推理。
回答 1
Stack Overflow用户
回答已采纳
发布于 2018-03-25 22:19:58
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/49481213
复制相关文章
相似问题
腾讯云开发者
