正式验证算法的正确性

Question

首先,这只能在没有副作用的算法上实现吗？

其次,我在哪里可以了解这个过程,任何好书,文章等？

Answer 1

COQ是一种产生正确ocaml输出的证明助手.但这很复杂.我从来没有去看过它,但我的同事开始了,然后在两个月后停止使用它.这主要是因为他想要更快地完成任务,但如果你需要验证算法,这可能是一个好主意.

这是一个使用COQ 的课程,并讨论了证明算法.
以下是关于在COQ中撰写学术论文的教程.

Answer 2

1. 在不涉及副作用的情况下，验证/证明正确性通常要容易得多，但这不是绝对要求。
2. 您可能想查看一些有关Z等正式规范语言的文档。正式的规范本身并不是证明，但通常是证明的基础。