まえがき
プログラムのエラーが悲惨な結果につながる可能性があることは秘密ではありません。 歴史は、カウンターのオーバーフローまたは未処理の例外が大きな材料費と人的犠牲をもたらした多くの場合を知っています。 したがって、たとえば、1996年6月4日、欧州のアリアン5ロケットは、飛行の39秒で文字通り崩壊しました。 インシデントの分析は、ソフトウェアエラーが原因で事故が発生したことを示しました。 1991年2月、パトリオットミサイルは丸め誤差により目標を逃し、500メートル余分に飛ぶことができました。 損害：28人が死亡し、100人以上が負傷しました。 この種のエラーはハードウェアにもあります。 浮動小数点数の誤った除算に関連するPentiumプロセッサの最近のバグにより、Intelは欠陥のあるチップを交換せざるを得ませんでした。 この間違いは、会社に4億7500万ドルの費用がかかりました。
信頼性の要件を高めたハードウェアまたはプログラムを設計する場合、正式な検証が広く使用されます-検証対象が正式な記述に準拠していることの正式な証明。 ここでの主題は、アルゴリズム、デジタル回路、HDLハードウェア記述などです。
正式な検証手順は、かなり長く、日常的な作業です。 したがって、すべての場合に正当化されるわけではありません。 日常のアプリケーションには、定期的なテストも適しています。 ここで、テストではプログラムにエラーがないこと、および正式な記述への準拠を証明できないことを理解する必要があります。
もちろん、すべてのステートメントが自動的に証明できるわけではありません。 そのような場合、プルーフチェッカー（プルーフアシスタント）システムが助けになります。その1つがCoqです。
はじめに
Coqは、定理を証明するための対話型シェルであり、依存型である独自の関数型プログラミング言語であるGallinaを使用します。 これは、80年代半ばにフランスINRIA研究所の従業員によって発明され、実装されました。 Coqは現在、GNU / Linux、Windows、およびMacOSで使用できます。 ソースコードは、LGPL v.2ライセンスの条件の下で配布されます。
Coqを操作するには、いくつかの方法があります：対話モードのコンソール、CoqIDEのグラフィックモード、またはProof Generalプラグインを使用したEmacs。
これで、Coqがインストールされ、準備完了です。 何か書いてみよう！
Coq言語には組み込みのバッテリーはありません-論理値も数値もありません（実際、多くの有用な定義と補題を持つ標準ライブラリがありますが、学術目的のためにこれは何もないと仮定します）。 代わりに、Coqは、新しいデータ型とこれらの型を操作および変換する関数を定義するための強力なツールを提供します。 特定の例を考えてみましょう：
誘導日：タイプ：= | 月曜日：日 | 火曜日：日 | 水曜日：日 | 木曜日：日 | 金曜日：日 | 土曜日：日 | 日曜日：日。
この宣言を使用して、データ値の新しいセット（型）を定義することをCoqに伝えます。 この型は
day
と呼ばれ、この型の値は
monday
、
tuesday
などです。これで、
day
型の値に関数を書くことができます。 翌営業日を計算する関数を作成します。
定義next_weekday（d：日）：日：= と一致するd | 月曜日=>火曜日 | 火曜日=>水曜日 | 水曜日=>木曜日 | 木曜日=>金曜日 | 金曜日=>月曜日 | 土曜日=>月曜日 | 日曜日=>月曜日 終わり。
Coqには、型推論、パターンマッチングなど、関数型プログラミング言語に共通するものがあります。
関数を定義したら、いくつかの例を使用してパフォーマンスをテストします。 最初に、
Eval simpl
使用できます。
（next_weekday friday）の簡易評価。
（* ==>月曜日：日*）
（next_weekday（next_weekday saturday））で簡易評価します。
（* ==>火曜日：日*）
第二に、期待される結果を明示的に示し、Coqにそれを確認するよう指示することができます。
test_next_weekdayの例： （next_weekday（next_weekday saturday））=火曜日。 証明。 簡単 反射性。 Qed。
CoqIDEで作業する場合、ステップバイステップのプログラム実行を使用して中間結果を確認すると便利です。
3番目の方法は、定義をプログラミング言語（OCaml、Scheme、またはHaskell）に抽出することです。 これはCoqシステムの主要な機能の1つであり、そのためにすべてが開発されました。
抽出言語Ocaml。 抽出 "/tmp/day.ml" next_weekday。
OCamlで関数を抽出した結果、次のようになりました。
タイプ日= | 月曜日 | 火曜日 | 水曜日 | 木曜日 | 金曜日 | 土曜日 | 日曜日 （** val next_weekday：day-> day **） let next_weekday =関数 | 月曜日->火曜日 | 火曜日->水曜日 | 水曜日->木曜日 | 木曜日->金曜日 | _->月曜日
おわりに
次のセクションでは、再帰関数を決定し、証拠の主な戦術を使用する方法を検討します。
推奨読書：
次の部分 。