testing - Haskell 関数は、正しさのプロパティで証明/モデルチェック/検証できますか?

Question

あなたのことはわかりませんが、保証できないコードを書くことにうんざりしています。

上記の質問をして驚異的な回答を得た後 (ありがとうございました!) Haskellへの証明可能で実用的なアプローチの検索を絞り込むことにしました。私が Haskell を選んだのは、それが実際に有用であり (Haskell用に書かれた多くの Web フレームワークがあり、これは良いベンチマークのようです) 、機能的に十分に厳密であり、証明可能であるか、少なくとも不変条件のテストが可能であると考えたからです。

これが私が欲しいものです（そして見つけることができませんでした）

psudocode で記述された Haskell 関数 add を参照できるフレームワークが必要です。

add(a, b):
    return a + b

- そして、特定の不変量がすべての実行状態を保持しているかどうかを確認します。正式な証明が欲しいのですが、モデルチェッカーのようなもので解決します。
この例では、値aとbを指定すると、戻り値は常に合計a+bになります。

これは簡単な例ですが、このようなフレームワークが存在することは不可能ではないと思います。テストできる関数の複雑さには確かに上限があります (関数への 10 個の文字列入力は確かに長い時間がかかります!) が、これは関数のより慎重な設計を促進し、他の形式を使用する場合と違いはありません。メソッド。Z または B を使用することを想像してみてください。変数/セットを定義するときは、変数に可能な限り小さい範囲を指定するようにしてください。INT が 100 を超えることがない場合は、そのように初期化してください。このような手法と適切な問題分解により、Haskell のような純粋関数型言語の十分なチェックが可能になるはずです。

私は正式なメソッドや Haskell の経験はまだありません。私のアイデアが正しいものなのか、それとも Haskell は適していないと思うのか教えてください別の言語を提案する場合は、「has-a-web-framework」テストに合格することを確認し、元の質問を読んでください:-)

score 63 · Accepted Answer

さて、あなたは Haskell ルートを取っているので、いくつかのことから始めましょう:

カリー・ハワード対応をご存知ですか？これに基づくマシンチェック証明に使用されるシステムがあり、多くの点で、非常に強力な型システムを備えた単純な関数型プログラミング言語です。
Haskell コードの分析に役立つ概念を提供する抽象数学の分野に精通していますか? さまざまな種類の代数といくつかの圏論がたくさん出てきます。
Haskell は、すべてのチューリング完全言語と同様に、常に非終了の可能性があることに注意してください。一般に、何かが常に真であることを証明することは、何かが真であること、または非終了値に依存することを証明することよりもはるかに困難です。

単にテストするだけでなく、証明を真剣に行う場合は、これらのことを念頭に置いておく必要があります。基本的なルールは次のとおりです。無効な状態を作成すると、コンパイラエラーが発生します。最初に無効なデータがエンコードされるのを防ぎ、型チェッカーに面倒な部分を任せてください。

さらに先に進みたい場合、メモリが役立つ場合は、証明アシスタントCoqに「Haskell への抽出」機能があり、重要な関数に関する任意のプロパティを証明してから、証明を Haskell コードに変換できます。

派手な型システムを Haskell で直接行うことについては、Oleg Kiselyov が Grand Masterです。彼のサイトで、配列境界チェックの静的証明をエンコードするための高ランクのポリモーフィック型などの巧妙なトリックの例を見つけることができます。

より軽量なものについては、タイプレベルの証明書を使用して、データの一部が正しいかどうかがチェックされていることをマークするなどのことができます。正確性チェック自体はまだ自分で行う必要がありますが、他のコードは少なくとも、一部のデータが実際にチェックされていることを知っていることに頼ることができます。

軽量な検証と派手な型システムのトリックから構築できるもう 1 つのステップは、ドメイン固有言語を埋め込むためのホスト言語として Haskell が適切に機能するという事実を利用することです。最初に、有用なプロパティをより簡単に証明できる慎重に制限されたサブ言語 (理想的にはチューリング完全ではないサブ言語) を構築し、次にその DSL でプログラムを使用して、プログラム全体のコア機能の重要な部分を提供します。たとえば、引数が 2 つの関数が連想的であることを証明して、その関数を使用して項目のコレクションを並列に縮小することを正当化できます (関数適用の順序は重要ではなく、引数の順序のみが重要であるため)。

あ、最後にひとこと。Haskell に含まれている落とし穴を回避するためのいくつかのアドバイス: さもなければ安全に構築できるコードを妨害する可能性があります: ここでのあなたの宿敵は、一般的な再帰、IOモナド、および部分関数です:

後者は比較的簡単に避けることができます: それらを書かず、使用しないでください。パターンマッチのすべてのセットが考えられるすべてのケースを処理することを確認し、errorまたはを使用しないでundefinedください。唯一のトリッキーな部分は、エラーを引き起こす可能性のある標準ライブラリ関数を回避することです。いくつかは明らかに安全ではfromJust :: Maybe a -> aありhead :: [a] -> aません。いくつかの入力値に対して本当に本当に何もできない関数を書いていることに気付いた場合は、無効な状態が入力タイプによってエンコードされることを許可しているため、最初にそれを修正する必要があります。
2 つ目は、式から使用されるさまざまな純粋な関数を介してデータを分散させることにより、表面的なレベルで簡単に回避できIOます。可能な限り、プログラム全体を純粋なコードに移動して、実際の I/O 以外のすべてを個別に評価できるようにすることをお勧めします。これは主に、外部入力によって駆動される再帰が必要な場合にのみ注意が必要です。これにより、最後の項目にたどり着きます。
賢明な言葉:十分に根拠のある再帰と生産的なコアカージョン. 再帰関数が、ある開始点から既知の基本ケースに進むか、要求に応じて一連の要素を生成していることを常に確認してください。純粋なコードでは、これを行う最も簡単な方法は、有限のデータ構造を再帰的に折りたたむことです (たとえば、カウンターを最大値までインクリメントしながら関数自体を直接呼び出す代わりに、カウンター値の範囲を保持するリストを作成して折りたたむことです)。）または遅延データ構造（たとえば、ある値の漸進的近似のリスト）を再帰的に生成しますが、2つを直接混合しないように注意してください（たとえば、「ストリーム内で特定の条件を満たす最初の要素を見つける」だけではありません。代わりに、ストリームから最大深度まで値を取得し、有限リストを検索して、見つからない場合を適切に処理します)。
最後の 2 つの項目を組み合わせて、一般的な再帰で本当に必要な部分についてはIO、プログラムをインクリメンタルコンポーネントとしてビルドしてから、扱いにくい部分をすべて単一の「ドライバー」関数に凝縮します。たとえば、のような純粋な関数mainLoop :: UIState -> Events -> UIState、のような終了テストquitMessage :: Events -> Bool、保留中のイベントを取得するgetEvents :: IO Events関数、および更新関数を使用して GUI イベントループを記述しupdateUI :: UIState -> IO ()、実際にのような一般化された関数を使用して実行することができますrunLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO ()。これにより、複雑な部分が真に純粋に保たれ、イベントスクリプトを使用してプログラム全体を実行し、結果の UI 状態を確認できます。一方で、厄介な再帰 I/O 部分を、理解しやすく、多くの場合必然的に正しい単一の抽象的な関数に分離できます。パラメトリック性による。

score 21 · Accepted Answer

おそらく、あなたが求めているものに最も近いのはHaskabelleです。これは、 Haskell ファイルを Isabelle 理論に変換し、それらに関するものを証明できる証明アシスタントIsabelleに付属するツールです。私の知る限り、このツールは HOL - ML - Haskell プロジェクト内で開発されており、ドキュメンテーションページには背後にある理論に関する情報が含まれています。

私はこのプロジェクトにあまり詳しくなく、それで何が行われたかについてあまり知りません。しかし、 Brian Huffmanがこれらのことをいじっていることは知っています。彼の論文や講演をチェックしてください。関連する内容が含まれているはずです。

score 19 · Accepted Answer

あなたが求めていることが本当にあなたを幸せにするものかどうかはわかりません。:-)

モデルが実用的であるためにはドメイン固有でなければならないため、汎用言語のモデルチェックはほぼ不可能です。ゲーデルの不完全性定理により、十分に表現力のある論理で自動的に証明を見つける方法はありません。

これは、自分で証明を書かなければならないことを意味し、その努力が費やした時間の価値があるかどうかという問題が生じます. もちろん、この努力は非常に価値のあるもの、つまりプログラムが正しいという保証を生み出します。問題は、これが必須かどうかではなく、費やされる時間が大きすぎるかどうかです。証明については、プログラムが正しいことを「直感的に」理解しているかもしれませんが、この理解を証明として形式化するのは非常に難しいことがよくあります。直感的な理解の問題は、偶発的なミス (タイプミスやその他のばかげたミス) を非常に起こしやすいことです。これは、正しいプログラムを作成する上での基本的なジレンマです。

したがって、プログラムの正しさに関する研究とは、証明を形式化し、その正しさを自動的にチェックすることを容易にすることです。プログラミングは、「形式化の容易さ」の不可欠な部分です。推論しやすいスタイルでプログラムを書くことは非常に重要です。現在、次のスペクトルがあります。

C、C++、Fortran、Python などの命令型言語: ここで何かを形式化するのは非常に困難です。単体テストと一般的な推論は、少なくともある程度の保証を得る唯一の方法です。静的型付けは些細なバグのみをキャッチします (バグをキャッチしないよりははるかに優れています)。
Haskell や ML などの純粋関数型言語: 表現力豊かな型システムは、重要なバグや間違いを見つけるのに役立ちます。手で正しいことを証明することは、200 行程度までのスニペットに対して実用的だと思います。(たとえば、運用パッケージの証明を行いました。)クイックチェックテストは、形式化された証明の安価な代替手段です。
Agda、Epigram、Coq などの依存型付き言語と証明アシスタント: 証明の形式化と発見の自動化されたヘルプのおかげで、プログラム全体が正しいことを証明できます。しかし、負担は依然として大きい。

私の意見では、正しいプログラムを作成するための現在のスイートスポットは、純粋に関数型プログラミングです。プログラムの正しさに命がかかっている場合は、レベルを上げて証明アシスタントを使用することをお勧めします。

score 5 · Accepted Answer

ESC/Haskell が必要なようですね: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm

ああ、Agda には Web フレームワークがあります (少なくとも概念実証): http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/

score 4 · Accepted Answer

クイックチェックはご覧になりましたか？それはあなたが必要とするもののいくつかを提供するかもしれません.

http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck

score 3 · Accepted Answer

一見単純な例であるadd（a、b）は、実際には検証が困難です。浮動小数点、オーバーフロー、アンダーフロー、割り込み、コンパイラ検証、ハードウェア検証などです。

HabitはHaskellの単純化された方言であり、プログラムのプロパティを証明することができます。

ヒュームは5つのレベルの言語であり、それぞれがより制限されているため、確認が容易です。

フルヒューム
  完全再帰
PR-ヒューム
  原始再帰関数
テンプレート-ヒューム
  事前定義された高階関数
  帰納的データ構造
  帰納的非再帰的一次関数
FSM-ヒューム
  非再帰的なデータ構造
HW-ヒューム
  機能なし
  非再帰的なデータ構造

もちろん、プログラムのプロパティを証明するための今日最も一般的な方法は、強力な定理を提供する単体テストですが、これらの定理は過度に具体的です。「有害と考えられるタイプ」、Pierce、スライド66

score 3 · Accepted Answer

ゼノを見てください。ウィキページを引用：

Zeno は、Haskell プログラムプロパティの自動証明システムです。インペリアルカレッジロンドンで、ウィリアムソネックス、ソフィアドロッソポウロウ、スーザンアイゼンバッハによって開発されました。任意の入力値に対して、2 つの Haskell 項が等しいという一般的な問題を解決することを目的としています。

現在利用可能な多くのプログラム検証ツールは、モデルチェックの種類のものです。非常に大きいが有限の検索空間を非常に迅速に横断することができます。これらは、記述が大きく、再帰的なデータ型がない問題に適しています。一方、Zeno は、無限の検索空間でプロパティを帰納的に証明するように設計されていますが、小さくて単純な仕様を持つもののみです。

score 2 · Accepted Answer

Haskell プログラムのいくつかの特性を正式に証明することは確かに可能です。私は FP 試験でそうしなければなりませんでした: 与えられた 2 つの式について、それらが同じ関数を表していることを証明します。Haskell はチューリング完全であるため、一般にこれを行うことはできません。そのため、機械的な証明者は、証明アシスタント (ユーザーガイダンス付きの半自動) またはモデルチェッカーのいずれかでなければなりません。

この方向への試みがありました。たとえば、P-logic: Haskell プログラムのプロパティ検証またはMizar を使用した関数型プログラムの正しさの証明を参照してください。どちらも、実装よりも方法を説明する学術論文です。

score 1 · Accepted Answer

MSR ケンブリッジによるごく最近の取り組み: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf

score 1 · Accepted Answer

ツールAProVEは、(少なくとも) Haskell プログラムの終了を証明することができます。これは、正当性の証明の一部です。詳細については、このペーパー(短いバージョン) を参照してください。

それとは別に、Dependent Typesに興味があるかもしれません。ここでは、型システムが拡張され、間違ったプログラムを不可能にするために使用されます。

score 1 · Accepted Answer

このツールhs-to-coqを使用して Haskell をほぼ自動で Coq に変換し、Coq 証明アシスタントの全機能を使用して Haskell コードを検証できます。詳細については、論文https://arxiv.org/abs/1803.06960およびhttps://arxiv.org/abs/1711.09286を参照してください。

testing - Haskell 関数は、正しさのプロパティで証明/モデルチェック/検証できますか?

11 に答える 11

Related

Reference