Mic*_*ahl 9 model-checking idris
我目前正在学习模型检查(模态逻辑,LTL,CTL,SAL模型检查器等).在我的业余时间,我正在学习Idris,这是一种支持依赖类型的强类型函数式编程语言.由于我正在研究模型检查和Idris,我开始对Idris如何与形式化方法和模型检查相关联感到好奇.
在了解模型检查时,感觉大多数示例都是关于验证以命令方式编写的系统或硬件组件.所以我对强类型函数式编程语言中的模型检查的相关性感到困惑,特别是在依赖类型的语言中,例如Idris,在我看来,类型检查器在验证正确性方面已经做了出色的工作. 然而,我的直觉告诉我,模型检查可能与不给予任何终止承诺的部分功能相关.
使用强大且依赖类型的编程语言(例如Idris)时,模型检查是否相关？
小智 4
你是对的，模型检查最常用于硬件验证和命令式（通常是并发）程序，因为它的起源也在这个领域。对于函数式程序，广泛使用复杂的类型系统技术进行验证。然而，它们通常需要大量注释，或者可能产生“误报”，从而导致反驳“正确”的程序。模型检查不需要这些注释，并且还可以允许回答更具体的问题。我不是该领域的专家，但似乎类型系统和模型检查的技术经常结合起来用于功能程序。如果您对功能程序模型检查的当前研究和方法感兴趣，可以阅读一门优秀的课程，其中包含大量在线材料：
http://www.cs.ox.ac.uk/people/luke.ong/personal/EWSCS13
该课程由该领域的领先研究人员之一 Luke Ong 编写。