强类型函数式编程语言中模型检查的相关性？

Question

强类型函数式编程语言中模型检查的相关性？

10

我目前正在学习模型检查（模态逻辑、LTL、CTL、SAL模型检查器等），并在业余时间学习Idris，它是一种支持依赖类型的强类型函数式编程语言。由于我同时涉及模型检查和Idris，所以我开始好奇Idris与形式方法和模型检查的关系。

在学习模型检查时，感觉大多数举例都是关于验证用命令式方式编写的系统或硬件组件。因此，我对在强类型函数式编程语言，尤其是像Idris这样的依赖类型语言中进行模型检查的相关性感到困惑，因为在这些语言中，类型检查器似乎已经非常出色地验证了正确性。 然而，我的直觉告诉我，模型检查可能与不保证终止的部分函数有关。

在使用像Idris这样的强类型和依赖类型编程语言时，模型检查是否相关？

- user483036

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Pachelbel · Accepted Answer

您说得对，模型检查通常用于硬件验证和命令式（通常是并发）程序，因为它的起源也在这个领域。对于功能性程序，广泛使用精心设计的类型系统技术进行验证。但是，它们经常需要大量注释，或者可能产生“假阳性”，导致拒绝一个“正确”的程序。模型检查不需要这些注释，并且还可以回答更具体的问题。虽然我不是该领域的专家，但似乎类型系统和模型检查技术经常被结合用于功能性程序。如果您对当前的功能性程序模型检查研究和方法感兴趣，有一门在线材料丰富的优秀课程：

http://www.cs.ox.ac.uk/people/luke.ong/personal/EWSCS13

这门课程是由领域内的主要研究者之一Luke Ong准备的。