10

現在、モデル チェック (モーダル ロジック、LTL、CTL、SAL モデル チェッカーなど) について学んでおり、余暇には、依存型をサポートする強く型付けされた関数型プログラミング言語である Idris について学んでいます。私はモデル チェックと Idris の両方を見ているので、Idris が Formal Methods とモデル チェックにどのように関係しているかに興味を持ち始めました。

モデルチェックについて学ぶとき、持ち出されるほとんどの例は、命令型で書かれたシステムまたはハードウェアコンポーネントの検証に関するもののように感じます. そのため、強く型付けされた関数型プログラミング言語、特に Idris などの依存型型付け言語でのモデル チェックの関連性について当惑しています。タイプ チェッカーが既に正しさの検証において素晴らしい仕事をしているように思えます。 ただし、私の直感では、モデルのチェックは、終了の約束をしない部分関数に関連している可能性があります。

Idris などの強く依存する型付きプログラミング言語を使用する場合、モデル チェックは適切ですか?

4

1 に答える 1

4

モデル チェックは、ハードウェア検証と命令型 (多くの場合は並行) プログラムに最も頻繁に使用されます。その起源もこの分野にあるためです。関数型プログラムでは、精巧な型システム手法が検証に広く使用されています。ただし、多くの場合、多くの注釈が必要になったり、「誤検知」が発生したりして、「正しい」プログラムに反論することになります。モデル チェックでは、これらの注釈は必要なく、より具体的な質問に回答することもできます。私はこの分野の専門家ではありませんが、関数型プログラムでは、型システムとモデル チェックの手法が組み合わされることが多いようです。関数型プログラムのモデル チェックに関する現在の研究とアプローチに興味がある場合は、オンラインで多くの資料を含む優れたコースがあります。

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

このコースは、この分野の主要な研究者の 1 人である Luke Ong によって準備されました。

于 2016-04-09T21:59:57.840 に答える