AmazonのDafnyでの教育プログラムの検証

導入

私たちは最近、Amazonの科学者とエンジニアにプログラムの検証を教えるために使用したいくつかの教育資料を利用可能にしました。で構成されています 講義スライド

そして 解決策を備えたエクササイズ。 DAFNYとプログラムの検証について学びたい場合は、すぐに飛び込むことができます。DAFNYでプログラムする方法、DAFNYの使用方法を証明アシスタントとして使用する方法、最後にプログラムの検証方法を学びます。代わりに、プログラムの検証にもっと興味がある場合は、講義の組織と驚くべき証明アシスタントとしてのDAFNYに焦点を当てることができ、次のメモはいくつかのコンテキストと説明を提供する必要があります。

DAFNY：プログラムの検証者と証明アシスタント

証明は2つの役割を果たします。

（i）証拠は、声明が正しいことを読者に納得させます。

（ii）声明が正しい理由を説明する証拠。

最初のポイントは、小さな推論ステップの正確性を検証し、それらが正しい証拠を構成するかどうかを確認する管理（「簿記係」）活動で構成されています。広い画像を見る必要はありませんが、すべてのステップが正しいかどうかを段階的に確認する必要があります。 2番目のポイントは、定理の直観を与えることを扱っています。なぜこのプロパティが保持されるのはなぜそれほど自然なのですか？どうやってこのようにそれを証明するという考えに来たのですか？


   – ハーマン・ゲウバーズ、インチ プルーフアシスタント：歴史、アイデア、未来

執筆仕様や証明を含むプログラムの検証を導入する1つの方法は、本によって実証されています プログラム証明 K. Rustan M. Leinoが執筆し、MIT Pressが発行しました。その本の方法論の決定的な特徴は、検証は常にプログラムによって動機付けられているだけでなく、仕様と証明はプログラムの属性であるということです。この本は、仕様が事前条件とポスト条件として書かれている単純な命令プログラムを検討することから始まり、証明はループ用の注釈を書くことによって行われます。カリキュラムは複雑さを高めるプログラムで続き、仕様と証明は続きます “飾る” プログラム。証明の概念は、さまざまなプログラミングコンストラクトが仕様の妥当性に及ぼす影響を詳述するプログラムロジックを通じて、ある程度暗黙的に導入されます。これはプログラムの検証を教えるための効果的な方法です：dafnyと組み合わせて‘Sオートメーションでは、プログラムを高レベルで説明する理由を説明するいくつかのアサーションでプログラムを検証することができます。プログラム検証のスタイルを促進します 「証明」 説明に相当します。

残念ながら、自動化が不足している場合、どの説明が検証に役立つかは必ずしも明確ではないかもしれません。それを理解するための明確な方法論なしに、適切な場所で正しいアサーションを提供する必要があるように見えるかもしれません。これは、プログラムの検証がしばらくの間非常にシンプルに見えた後、今ではアドホックに見えるかもしれない開発者にとってイライラする可能性があります。 DAFNYのプログラム検証に関する補完的な視点を提供することにより、この問題に対処しようとします。重要なアイデアは、DAFNYを証明アシスタントとして紹介し、プログラムと明示的かつ独立して証明を研究することです。この観点から、自動化を活用する直感的な証拠を書く方法を学ぶだけでなく、自然控除の詳細な正式な証明を書くことも学びます。この方法論は、説得力を持って証明する可能性を開きます。実際に有効な場合、検証に最終的に合格する証拠を改善するために、ほんの一握りのルールを使用できます。

コースは3つの異なる部分で編成されています。最初の2つでは、DAFNYはプログラミング言語（検証なし）および証明アシスタント（プログラミングなし）として導入されます。プログラム検証は最後に導入され、外因性検証を強調します。

パート1：プログラミング言語としてのDAFNY

講義の最初のセットでは、検証を考慮せずに、DAFNYをプログラミング言語として紹介します。主な動機は、DAFNYの新人が言語の構文とセマンティクス、およびそのツール（CLI、IDE）に精通できるようにすることです。また、より多くのベテランのDAFNY開発者が検証に直接スキップできるようになります。最後に、DAFNYは、強力な静的タイピング、オブジェクト指向、および機能的特徴を備えた本格的で古典的なプログラミング言語であることを強調しています。 DAFNYを紹介する機会かもしれません‘s外部関数インターフェースと、DAFNYは大規模なソフトウェアプロジェクトの一部として使用できるという考え。

順番に紹介します 機能プログラミング、
命令的なプログラミング、 そして
オブジェクト指向プログラミング。通常、モジュールシステムのプレゼンテーションを最小限に抑えます。

パート2：プルーフアシスタントとしてのDAFNY

検証を無視しながらDAFNYをプログラミング言語として導入した後、プログラミングを無視しながらDAFNYについて証明アシスタントとして学びます。紹介することから始めます 仕様の言語

dafnyの。そのコアでは、DAFNY仕様は、タイプ、定数、述語、および関数シンボルの解釈されていないシンボルで構成されており、フォーミュラの言語は教会のバリアントです‘Sシンプルなタイプ理論または高次ロジック。また、この講義では、フォーミュラのファミリーを宣言し、シンボルの意味を公理化する方法としてLemmaを紹介しています。特に、リアルやセットなどの原始的なタイプと操作は、特定の理論として提示されます。

次に、方法を説明します 定義する それらを公理化し、それらの存在を想定するのではなく、タイプ、定数、述語、および関数。これは、偏見、関数の終了、固定点、および代数データ型について話す機会です。

最後に、私たちは、より直感的な方法でDafnyで証明を研究し始めます
説明することで証明します。このスタイルでは、より慣用的なDafnyスタイルの証拠であるこのスタイルでは、中間アサーションを作成することで高校のジオメトリクラスで書いている種類の証拠に似た方法で証明できます。 xを固定であるが任意の奇数とします）、および矛盾による証明、症例分析による証明、誘導による証明などの高レベルの証明方法。

最後に、そして最も重要なことは、自然控除の規則（およびシーケント計算）を使用して完全に詳細かつ厳密な証明を開発する方法を説明することにより、より正式な方法で証明を研究します。 Dafnyの正式な証明に対するこの体系的なアプローチは、
説得力を持って証明します、常に十分な詳細を提供できるという基本的な考え方で、検証者が実際に有効である場合、最終的にあなたの証拠を受け入れるようにします。

パート3：DAFNYのプログラム検証

紹介で述べたように、DAFNYのような言語でのプログラム検証について学習するための典型的なパスは、簡単な命令プログラム、プログラムアノテーションとしての仕様、およびプログラムロジックのプログラムアノテーションとしての証明から始めることです。しかし、Dafnyは証明アシスタントであり、証明は自然控除で表現されているという異常な観点をとることにより、プログラムとは独立して証拠を導入したため、プログラムの検証への旅は多少異なります。

数学の検証に大きく似ているため、機能プログラムの検証から始めます。より特別に、最初にレビューします
機能プログラムの外因性検証、つまり、機能を維持し、定義をタイプし、そのプロパティを指定および証明することから分離します（可能な限り）。実際には、関数にプロパティを注釈するのではなく、代わりに個別の補題として述べ、証明することを意味します。そうして初めて、私たちはやり直します
機能プログラムの固有の検証 事前およびポスト条件、およびサブセットタイプ。外因性と本質的な検証を別々に保つ動機は、証明の脆性について念頭に置くことの重要性を強調することであり、デフォルトの検証プログラミング戦略を作成するのではなく、検証を最も簡素化する本質的な検証を導入することがより良い戦略である可能性があることです。

次に、議論します 命令プログラムの検証。まず、地元の状態を紹介し、最終的に簡単にプログラムロジック、ループ不変剤、およびゴーストステートに言及します。また、強調します
重要な方法論 命令プログラムの特性を直接証明する代わりに、最初にそれが機能モデルとして動作することを証明し、次にその機能モデルで興味深い特性を証明します。

最後に、の検証について説明します オブジェクト指向プログラム。素材は標準ですが、オブジェクトを定義することの重要性を強調しています‘s APIは、一貫性がない、または実際に使用できないAPIを思い付かないように、最初にクライアントを作成します。また、ゴースト表現はセットに限定される必要はなく、その種類の表現のタイプでクラスの意図した構造を可能な限りキャプチャすることが非常に有用であることを強調します。最後に、の重要性を強調します マスター 検証を大幅に容易にすることができるデータ構造のノード。

結論

このコースの最初のバージョンは、 プログラム証明。その目標は、ベテランのDAFNYソフトウェアエンジニアに、aの一部を紹介することにより、証明についての別の考え方に紹介することでした。 証明システムの基礎に関するコース ;特に自然控除とシーケント計算。それが効果的であるという逸話的な証拠があり、このカリキュラムを開発し続けて、プログラム検証の紹介として、また専門家が証明スキルを次のレベルに引き上げるのを支援する方法として使用しています。自動化は、簡単な例や演習に取り組むことが難しくなっているため、DAFNYで正式な証拠を教えることにとって重要な課題になる可能性がありますが、説得力のある証明に関する講義は、そうする試みを示しています。