Haskell関数を証明/モデルチェック/正確性特性で検証できますか？

StackOverflow https://stackoverflow.com/questions/4077970

質問

アイデアから続く： 実証可能な現実世界の言語はありますか？

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

上記の質問をして驚異的な応答を受け取った後（ありがとう！） ハスケル. 。 Haskellを選んだのは、実際に有用だからです（ある たくさんの ウェブ フレームワーク それのために書かれた、これは良いベンチマークのようです） と 私はそれが十分に厳しいと思います、 機能的に, 、それが証明可能であるか、少なくとも不変剤のテストを許可する可能性があること。

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

haskell関数を調べることができるフレームワークが必要です。

add(a, b):
    return a + b

- そして、特定の不変性がすべての実行状態を保持しているかどうかを確認します。私は正式な証拠を望んでいますが、モデルチェッカーのようなものに落ち着くでしょう。
この例では、不快感は与えられた値です a と b, 、返品値は常に合計です a+b.

これは簡単な例ですが、このようなフレームワークが存在することは不可能だとは思いません。確かにテストできる関数の複雑さに上限があります（関数への10文字列入力には確かに長い時間がかかります！）が、これは機能のより慎重な設計を促進し、他のフォーマルを使用することと違いはありません方法。 zまたはbを使用することを想像してください。変数/セットを定義するとき、変数に可能な限り小さな範囲を与えることを確認します。 INTが100を超えない場合は、そのように初期化してください！このような技術、および適切な問題の分解は、Haskellのような純粋な機能的言語の満足のいくチェックを可能にする必要があります。

私はそうではありません - まだ - 正式な方法やHaskellを非常に経験しています。私のアイデアが健全なものであるかどうか、またはHaskellが適していないと思うかもしれません。別の言語を提案する場合は、「has-a-web-framework」テストに合格し、オリジナルを読んでください 質問 :-)

役に立ちましたか？

解決

Haskellルートを取っているので、まず最初から始めましょう。

  • あなたはに精通していますか カレー - ハワード通信？これに基づいた機械チェックされた証明に使用されるシステムがあり、多くの点で非常に強力なタイプシステムを備えた単純な機能的なプログラミング言語です。

  • Haskellコードを分析するための有用な概念を提供する抽象的な数学の分野に精通していますか？代数のさまざまなフレーバーといくつかのカテゴリ理論のいくつかのビットがたくさん登場します。

  • Haskellは、すべてのチューリング複雑な言語と同様に、常に非終了の可能性があることに留意してください。一般的に、何かがそうなることを証明するのははるかに難しいです いつも 何かが真実であるか、禁止されていない価値に依存することを証明するよりも真実である。

あなたが真剣に行くなら 証拠, 、単にではありません テスト, 、これらは心に留めておくべきものです。基本的なルールは次のとおりです。無効な状態になるとコンパイラエラーを引き起こします。無効なデータがそもそもエンコードされるのを防ぎ、タイプチェッカーに退屈な部分を実行させます。

さらに進みたい場合、メモリが私に証明アシスタントに役立つなら coq 重要な関数に関する任意の特性を証明できる「Haskellへの抽出」機能があり、証明をHaskellコードに変えます。

Haskellで派手なタイプのシステムを直接行うために、 オレグ・キシエリョフはグランドマスターです. 。あなたは彼のサイトできれいなトリックのサイトで例を見つけることができます 高位の多型タイプをエンコードする配列境界の静的証明をエンコードする.

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

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

ああ、最後のこと。 Haskellに含まれている落とし穴を避けるためのいくつかのアドバイス。これは、他の方法では構成ごとに安全なコードを妨害する可能性があります。 一般的な再帰, 、 IO モナド, 、 と 部分関数:

  • 最後は比較的簡単に避けることができます：それらを書かないで、それらを使用しないでください。パターンのすべてのセットが、可能なすべてのケースを処理し、使用しないことを確認してください error また undefined. 。唯一のトリッキーな部分は、エラーを引き起こす可能性のある標準的なライブラリ関数を回避することです。いくつかは明らかに安全ではありません fromJust :: Maybe a -> a また head :: [a] -> a しかし、他の人はもっと微妙かもしれません。いくつかの入力値で本当に何もできない関数を書いていることに気付いた場合、最初にそれを修正する必要があるという無効な状態をエンコードすることができます。

  • 2番目は、さまざまな純粋な機能を介して物を散乱させることにより、表面的なレベルでは簡単に回避できます。 IO 表現。可能な限り、プログラム全体を純粋なコードに移動して、実際のI/O以外のすべてで独立して評価できるようにすることです。これは、外部入力によって駆動される再帰が必要な場合にのみトリッキーになり、最終的なアイテムになります。

  • 賢者への言葉： 根拠のある再帰 と 生産的なcorecursion. 。再帰関数が出発点から既知の基本ケースに移動するか、一連の要素をオンデマンドで生成していることを常に確認してください。純粋なコードでは、これを行う最も簡単な方法は、有限のデータ構造を再帰的に崩壊させることです（たとえば、最大までカウンターを増やしながら直接呼び出す関数の代わりに、カウンター値の範囲を保持するリストを作成して折ります）または怠zyなデータ構造を再帰的に生成します（例：何らかの値の進行性近似のリスト）。存在します。代わりに、ストリームから最大の深さまで値を取得し、有限リストを検索して、発見されていないケースを適切に処理します）。

  • あなたが本当に必要とする部品のために、最後の2つのアイテムを組み合わせる IO 一般的な再帰で、プログラムを増分コンポーネントとして構築してから、すべての厄介なビットを単一の「ドライバー」関数に凝縮してください。たとえば、次のように純粋な関数を持つGUIイベントループを書くことができます mainLoop :: UIState -> Events -> UIState, 、次のような出口テスト quitMessage :: Events -> Bool, 、保留中のイベントを取得する機能 getEvents :: IO Events, 、および更新関数 updateUI :: UIState -> IO (), 、それから実際には、次のように一般化された関数で物を実行します runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO (). 。これにより、複雑な部分が本当に純粋に保たれ、イベントスクリプトでプログラム全体を実行し、結果のUI状態を確認できますが、厄介な再帰的なI/O部品を理解しやすく、しばしば正しい単一の抽象関数に分離します。に パラメトリック.

他のヒント

おそらくあなたが求めているものに最も近いものは ハスカベル, 、プルーフアシスタントに付属するツール イザベル HaskellファイルをIsabelleの理論に翻訳し、それらについてのことを証明できます。私が理解している限り、このツールはhol -ml -haskellプロジェクト内で開発されています ドキュメントページ 背後にある理論に関する情報が含まれています。

私はこのプロジェクトにひどく慣れていませんし、それで何が行われたかについてあまり知りません。でも私は知ってる ブライアン・ハフマン これらのことで遊んでいて、彼の論文と講演をチェックしています、それらには関連するものが含まれるべきです。

あなたが求めるものが実際にあなたを幸せにするものであるかどうかはわかりません。 :-)

モデルをチェックすることは、モデルが実用的になるように固有のドメインでなければならないため、隣接するものです。ゲーデルの不完全性の定理のために、単にあります 自動的に証明を見つける方法はありません 十分に表現力豊かな論理で。

これは、あなたがしなければならないことを意味します 自分で証明を書いてください, 、努力が時間を費やす価値があるかどうかという問題を提起します。もちろん、この努力は非常に貴重なもの、つまりあなたのプログラムが正しいという保証を生み出します。問題は、これが必需品であるかどうかではなく、費やす時間が大きすぎるかどうかです。証拠についてのことは、あなたが持っているかもしれないが あなたのプログラムが正しいことを理解する「直感的」, 、それはしばしば非常にです この理解を正式にするのは難しい 証拠として。直感的な理解の問題は、偶発的な間違い（タイプミスやその他の愚かな間違い）の影響を非常に受けやすいことです。これは、正しいプログラムを書くことの基本的なジレンマです。

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

  • C、C ++、Fortran、Pythonなどの命令的な言語：ここでは何でも形式化するのは非常に困難です。ユニットテストと一般的な推論は、少なくともある程度の保証を取得する唯一の方法です。静的タイピングは、些細なバグのみをキャッチします（それらを捕まえないよりもはるかに優れています！）。

  • Haskell、MLのような純粋に機能的な言語：表現型タイプシステムは、自明でないバグや間違いをキャッチするのに役立ちます。手で正しさを証明することは、約200行のどこかのどこかのスニペットにとって実用的です、と私は言います。 （私は自分のために証拠をしました 運用パッケージ, 、 例えば。） クイックチェック テストは、正式な証明の安価な代替品です。

  • Agda、Epigram、Coqなどの依存型の言語と校正アシスタント：プログラム全体を正しいことを証明することは、自動化されたヘルプの証明の正式化と発見のおかげで可能です。しかし、負担はまだ高いです。

私の意見では、正しいプログラムを書くための現在のスイートスポットは 純粋に機能的なプログラミング. 。生活がプログラムの正確さに依存している場合は、レベルを上げて証明アシスタントを使用する方が良いでしょう。

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/

QuickCheckを見たことがありますか？それはあなたが必要とするもののいくつかを提供するかもしれません。

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

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

癖 プログラムの特性を証明できるHaskellの単純化された方言です。

ヒューム 5つのレベルの言語で、それぞれがより限定され、したがって、検証しやすい言語です。

Full Hume
  Full recursion
PR−Hume
  Primitive Recursive functions
Template−Hume
  Predefined higher−order functions
  Inductive data structures
  Inductive  Non−recursive first−order functions
FSM−Hume
  Non−recursive data structures
HW−Hume
  No functions
  Non−recursive data structures

もちろん、プログラムの特性を証明するための今日の最も人気のある方法は、強力な定理を提供するユニットテストですが、これらの定理は非常に具体的です。 「有害と見なされるタイプ」、ピアス、スライド66

見て ゼノ. 。 Wikiページを引用：

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

今日入手可能なプログラム検証ツールの多くは、多様性をチェックするモデルのものです。非常に大きいが有限の検索スペースを非常に迅速に通過できます。これらは、大きな説明がある問題に適していますが、再帰的なデータ型はありません。一方、Zenoは、無限の検索スペースを介して特性を誘導的に証明するように設計されていますが、小さくてシンプルな仕様のみがあります。

確かに証明することは可能です いくつかの Haskellプログラムのプロパティは正式に。 FP試験でそうしなければなりませんでした。2つの表現を考慮して、それらが同じ機能を示していることを証明します。 Haskellはチューリングが完全であるため、これを一般的に行うことはできません。そのため、機械的なプロバーは、プルーフアシスタント（ユーザーガイダンスを使用した半自動）またはモデルチェッカーでなければなりません。

この方向に試みがありました、例： P-Logic：Haskellプログラムのプロパティ検証 また Mizarを使用した機能プログラムの正確性を証明します. 。どちらも、実装よりも多くの方法を説明する学術論文です。

MSR Cambridgeによるごく最近の取り組み：http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf

道具 アプローブ （少なくとも）Haskellプログラムの終了を証明することができます。これは、正確性を証明することの一部です。詳細はにあります この紙 (より短いバージョン).

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

ツールを使用できます hs-to-coq Haskellをほとんど自動化してCoQに変換し、CoQの全力を使用してAssistantを証明してHaskellコードを確認します。論文を参照してください https://arxiv.org/abs/1803.06960 と https://arxiv.org/abs/1711.09286 いくつかの情報について。

ライセンス： CC-BY-SA と 帰属
所属していません StackOverflow
scroll top