问认证计划的定义

EN

我看到了几个不同的研究小组，至少有一本书，他们谈到了使用Coq来设计认证的程序。对认证课程的定义有共识吗？据我所知，它真正的意思是程序被证明是完全正确的。现在，程序的类型可能是一些非常奇特的东西，比如一个列表，证明它是非空的，排序的，所有元素都是>= 5的，等等。然而，归根结底，一个经过认证的程序仅仅是一个Coq显示的完全和类型安全的程序，其中所有有趣的问题都归结为最终类型中包含了什么？

编辑1

基于wjedynak的回答，我看了Xavier Leroy的论文“Realistic Compiler的形式验证”，这篇论文在下面的答案中有链接。我认为这包含了一些很好的信息，但我认为在这一系列研究中更多的信息可以在桑德林·布拉齐和泽维尔·勒罗伊的论文Mechanized Semantics for the Clight Subset of the C Language中找到。这就是“正式验证”论文中添加优化的语言。在这篇文章中，Blazy和Leroy介绍了Clight语言的语法和语义，然后在第5节讨论了这些语义的验证。在第5节中，有一个用于验证编译器的不同策略的列表，在某种意义上，它概述了创建经过认证的程序的不同策略。它们是：

使用备用语义的semantics

• Verified translations

• Testing可执行文件semantics

• Equivalence的

1. 手册

属性

在任何情况下，可能还有一些要点可以添加，我当然希望听到更多。

回到我最初的问题，什么是认证计划的定义，对我来说仍然有点不清楚。Wjedynak在某种程度上提供了一个答案，但实际上Leroy的工作涉及在Coq中创建编译器，然后在某种意义上认证它。从理论上讲，这使得现在可以证明关于C程序的事情，因为我们现在可以进行C->Coq->证明。从这个意义上说，似乎有这样的工作流程，我们可以

在Coq或其他一些证明辅助工具中，根据步骤1中的程序模型，用X language

• Form编写一个

1. 程序。这可能涉及到在Coq中创建编程语言的模型，也可能涉及到直接创建程序的模型(即在Coq中重写程序本身)。
2. 证明了模型的一些性质。也许这是一个关于价值观的证据。也许这是语句等价性的证明(如3=1+2或f(x，y)=f(y，x)，whatever.)
3. Then，基于这些证明，称原始程序已通过认证。

或者，我们可以在证明辅助工具中创建程序的规范，然后验证规范的属性，而不是程序本身。

在任何情况下，我仍然有兴趣听到替代定义，如果有人有他们。