认证计划的定义

我看到了几个不同的研究小组,至少有一本关于使用Coq设计认证程序的书.关于认证计划的定义是什么,是否有共识？从我所知道的,它真正意味着该程序被证明是完整的并且类型正确.现在,程序的类型可能是非常奇特的东西,例如列表,其中包含非空的证明,排序,所有元素> = 5等等.但是,最终,是一个经过认证的程序,Coq显示的是总计和类型安全的程序,所有有趣的问题归结为最终类型中包含的内容？

根据wjedynak的回答,我看了Xavier Leroy的论文"现实编译器的形式验证",它在下面的答案中有所联系.我认为这包含一些很好的信息,但我认为这个研究序列中的信息量更多的信息可以在Sandrine Blazy和Xavier Leroy 的C语言的Clight子集的机械化语义学中找到.这是"形式验证"论文添加优化的语言.在其中,Blazy和Leroy介绍了Clight语言的语法和语义,然后在第5节讨论了这些语义的验证.在第5节中,列出了用于验证编译器的不同策略,这在某种意义上提供了概述创建认证计划的不同策略.这些是:

手动评论

证明语义的属性

验证翻译

测试可执行语义

与备用语义的等价性

在任何情况下,可能会添加一些点,我当然希望听到更多.

回到我关于认证程序定义的原始问题,对我来说仍然有点不清楚.Wjedynak提供了一个答案,但Leroy的工作实际上涉及在Coq中创建编译器,然后在某种意义上证明它.从理论上讲,它现在可以证明C程序的内容,因为我们现在可以进行C-> Coq->证明.从这个意义上讲,似乎就是我们可以做到这一点

用X语言编写程序

Coq中的步骤1或其他证明助手工具的程序模型的形式.这可能涉及在Coq中创建编程语言的模型,或者它可能涉及直接创建程序模型(即在Coq中重写程序本身).

证明一些关于模型的属性.也许这是关于价值观的证明.也许它是语句等价性的证明(例如3 = 1 + 2或f(x,y)= f(y,x)之类的东西.)

然后,根据这些证明,调用原始程序认证.

或者,我们可以在校对助手工具中创建程序规范,然后证明规范的属性,而不是程序本身.

无论如何,如果有人有这些定义,我仍然有兴趣听取其他定义.