プログラム利用時のすべてのユース・ケース を 完璧に網羅 する 検証テスト なんてありえない! なら、「論理的」に「プログラムの正しさ・完璧さ」 を 証明する「定理証明支援系言語」か? ~ その関数型言語 との関係

  • 80
    いいね
  • 0
    コメント

この記事は、「形式証明」や「定理証明」を行うプログラミング言語とその使い方について調査を始めた作業メモです

400年の難問、「ケプラー予想の証明」やっと100%終わる

add2.png

コペルニクスが提唱した地動説を、天体運行法則で不動のものにした偉人ヨハネス・ケプラー。

そのケプラーが1611年に提唱した「球は、八百屋に山盛りのオレンジみたいにピラミッド型に並べると一番沢山入る」という説が、400年の歳月を経て、100%正しかったことがコンピュータの力で証明されました。
この立体最密充填の解答は、誰でも直感的になんとなく正しいことがわかります。けれども証明するとなると超厄介で、世界歴代の天才がいくら頭脳を結集しても証明できなくて、ずっと「定理」ではなく「ケプラー予想」と呼ばれ続けてきた難題中の難題です(参考)。

証明したのは、米ピッツバーグ大学のトマス・ヘールズ教授です。もともと氏が1998年に発表し、「フェルマーの最終定理以来の難問が解けた!」と世界中が沸き立ったのですが、なんせ文章で300ページにも及ぶ遠大な証明でして、間違いチェックがまだ終わっていなかったのです。どびょ~ん。
審査員12人が答え合わせに挑戦するも、4年後には残り1%のところでギブアップ。前例のない労力をつぎ込み脳みそがショートするまでがんばって99%正しいことまではわかったのですが、もう精も根も尽き果ててしまって、残り1%がどうしてもクリアできない…。相変わらずケプラー「予想」のままとなりました。

これではいかんと、2003年にはヘールズ教授自らが証明支援ツールで形式的証明を目指す「Flyspeckプロジェクト」を発表、32コアの並列処理をガンガンやってしらみ潰しに答え合わせをしてきたのであります。

証明支援プログラムとして使ったのは、John Harrisonが開発した「HOL Light」と、HOL後継システムの「Isabelle」です。

いずれも実証が簡単な一連の短い論述をベースにするもので、時間さえ充分に与えてやれば、他の一連の論述(例えば数学的証明)の正しさがチェックできます。

この「充分に与えてやれば」というのが曲者で、延々この日曜までかかりました。結果はセーフ、ミスはゼロ。ヘールズ教授は、天晴れて証明が裏付けられた今の心境を「10年若返った気分だよ」とNew Scientistに語っていますよ。

複雑&高度な数学的証明は毎年何百本となく世に出ています。こんな風に人力ではムリでも自動定理証明機で実証できるとなれば、気が遠くなるような答え合わせの部分はコンピュータに任せてしまって、人間はクリエイティヴな思考に集中できます。これをふまえると今回の発表は、教授以外の人にも朗報ですね。

Haskell や、Haskell 以外の 関数型言語 一般について調べ始めるなかで、「形式証明」 やら 「定理証明」 を支援する言語、というものがあることを知った。

なにやら、作成したプログラムの検証テストでは、すべてのユース・ケースを想定できない限界があるが、この 「形式証明支援系言語」 を使うと、論理的に、そのプログラムには誤りがない ことを 証明 できるらしい。

Google でエンジニア求人サイトを調べてみると、数は少ないけど、プログラム品質保証 や 検証テスト の要員募集で、「定理証明の経験のある方」 とか、「形式証明支援系言語 CoqAgda 経験 ○年」 などの記載もある。

大学の研究室の世界だけでなく、プログラム開発現場でも、実際に使われて定着している言語 ということのようだ。


形式証明支援系言語 と 関数型プログラミング言語 との 関係

形式証明支援系言語Haskellを 例とした(純粋型付け)関数型言語 との 係わり合い に ついては、以下のウェブサイトに書いてあることが、鍵になるのではないか??

関数型言語の技術マップ 「Curry-Howard対応」

( 以下、上記 ウェブサイトからの転載 )

Curry-Howard対応

プログラミング言語の中での関数型言語の位置付けを考える上で重要なのがCurry-Howard対応(Curry-Howard correspondence)です。

Curry-Howard対応の詳細は上記Wikiページやk.inabaさんのCurry-Howard Isomorphism も参考になります。

ざっくりいうと、「単純型付ラムダ計算」と「直感主義命題論理&自然演繹」がIsomorphism(同型)ですから文字通り相互変換が可能ということです。

この枠組みの中では「型=命題」、「計算=証明」となり、コンパイルが成功すれば証明完了となります。

まさにプログラミングが数学の証明と同じということです。 凄いですね。

残念ながら「直感主義命題論理&自然演繹」で記述できる範囲は狭いので、汎用的に一般の問題を記述できるわけではありません。

しかし、同型という形で数学と直結している点が重要です。

「直感主義命題論理&自然演繹」を軸に、数理論理学の膨大な理論体系をプログラミングに取り込む可能性がみえてきます。

純粋関数型言語

関数型言語は大きく純粋関数型言語と(純粋でない普通の)関数型言語に分類することができます。

純粋関数型言語は、副作用がないといった性質が有名?ですが、重要なのは「単純型付ラムダ計算」をプログラミング言語として実現した物ということであろうと思います。

「純粋関数型言語」=「単純型付ラムダ計算」であればさらに、「純粋関数型言語」=「直感主義命題論理&自然演繹」であるわけで、プログラミング言語と数理論理学が直結することになります。

関数型言語データ型 は、どれも数学的(代数学的な)構造を『型』として定義している もののようなので、それらの『型』どうしを合成(関数)したり、組み合わせて、コードを構築していく 際には、どうしても、代数学的構造の要素と要素の間の相互関係 を記述した、群論 や 圏論 を(数学を純粋知性の冒険として愉しみ、味わいながら) 理解を深めていく必要がありそうだ。

関数型言語 でコードを記述していくこと(それ自体が、代数学的な建築物を構築していく営み??)と、形式証明 との係わり合いも、こうしたことを学び、理解を深めていくことで、だんだんと景色が見えてきそうな気が する。 :blush:

(静的型付き)関数型言語 と 数学(圏論) との 関係性

要約する と、以下のようになっています。


  • 1. 関数型言語における関数 は、(引数が同じならば返り値が常に同じ)数学的な意味での関数 で ある。
  • 2. 関数型言語 では、値と同様、関数 を 引数にとったり、関数 を 返り値 にとる高階関数 を定義したり、合成関数 を 容易に 定義できる。
  • 3. 合成関数を実装するとき、"一方の関数" の 返り値 として定義された「型」(=「値域」の範囲) と "もう片方の関数" の 持つ引数 の「型」(=「定義域」の範囲)とが一致していることを、「型」の一致の観点から、コンパイラ が 機械的 に チェックしてくれる(静的型チェック)。
  • 4. "数学的な意味での「関数」" を 基本構成要素とする のが 関数型言語である ため、関数型言語は、コンパイラ レベル でコードを最適化する際に、数学の「圏論」という、"「関数」 と 「関数」 との間に成立している、数学的に発見(証明)された知見" を 最大限 に 活用 している。
  • 5. 関数型言語のなかでも、(積極評価のOCmal言語とは違い)Haskellは、遅延評価の言語である(seq式で、積極評価の実行も可能)。このため、フィボナッチ数列 や 素数列 など、無限に続く数学的構造を宣言的に定義することができる。(実行時に必要とされるところまでしか、式は評価されないため、式の評価時(コード実行時)には、無限数列から、有限個の値しか生成されることがないから)実行時に計算がとまらなくなることを心配せずに、無限数列や、無限に再帰するデータ構造を、宣言的に記述することができる。

この辺の事情 は、以下の本 で 明確に、わかりやすく述べられています。

  • 大川 徳之(著)『関数プログラミング実践入門』(技術評論社)

スクリーンショット 2017-01-17 21.22.50.png

  • 大川 徳之(著)『[増補改訂]関数プログラミング実践入門 ──簡潔で,正しいコードを書くために』(技術評論社)

スクリーンショット 2017-01-17 23.10.47.png

大川 徳之(著)『関数プログラミング実践入門』(技術評論社) pp.24-27

関数型言語においては抽象化を行う際、関数型プログラマの誰もが明確に良いと言える方向性があります。

それは、群論 や 圏論 (脚注30) といった数学方向への抽象化です。

( 以下、脚注30 )

群論 や 圏論数学的な構造を扱う ための分野です。

関数型言語では数学的な意味での関数を扱う ため、数学的構造を扱う手法 が そのまま適用しやすい傾向 が あります

( 中略 )

数学は実に多くの問題を扱うことができますし、問題を一度数学の世界に抽象化できてしまえば、コンピュータの歴史よりも長きにわたり蓄積された豊か で 強力 な 数学の世界 の 成果 を、すべてそのまま適用できる状態になります。

( 中略 )

関数型言語の最適化

前述したとおり、関数型言語では数学的な抽象化を行います。

数学的に綺麗な世界を経由することで、最適化についても数学の成果を利用したものが可能となります。

ここで、1 から n までの自然数 を すべて足す関数 totalFrom1To を 考えてみましょう。

( 中略 )

このコードでは2つの関数、リストの中身をすべて足し算して総和の値にする関数 sum と、1 から N まで の リスト を 作る関数 enumFromTo 1 を 関数合成しています

Haskell のコードの例のように、一度中間的にリストを作ってから作ったリストを全部走査するような処理を書いたら、「リストを作る分 処理 が もったいないのでは?」と思うかもしれません。

ですが、こういった処理は最適化により、C言語のコードと同じように中間リストを作らない処理にすることができます。

これは、ある種の構造(今回の例ではリスト)を作る関数 と、 ある種の構造(今回の例ではリスト) を 畳み込む 関数 は、合成したとき に 中間構造 を 作らない関数 に 変換できる、という 数学の世界の成果 が 取り入れられている から です。

( 中略 )

関数型言語 では、 抽象化の項 でも説明したとおり、数学的な抽象化 を良いものとして利用しますので、他の言語でも行われるような通常の最適化の他に、数学的な抽象化を利用した最適化の段階 を 持つ こと が あります。

当たり前ですが、言語の持つ性質が数学的に綺麗であるほど、数学的な最適化は適用しやすくなります。 

また、5番目では、以下に言及しました。

  • 関数型言語のなかでも、遅延評価を行うHaskellでは、無限数列を、(実行時に計算が終わらないことを心配せずに)宣言的に定義できる。
  • Haskellは、遅延評価を行う言語であるため(同じ関数型言語でもOCamlは積極評価)、無限数列(がもつ構造や性質)を宣言的に記述しても、計算が永遠に終わらないというバグが発生することはない。(数学的構造をそのまま、宣言的に記述できる)

以下、長文ではあるが、再び大川本(pp.212-214)から抜粋して引用する。

遅延評価の利点、積極評価の欠点

遅延評価の1つの利点は、必要のない計算は本当に行わないことで計算量を低減できることです。

( 中略 )

明確に遅延評価を採用する利点と言えるところは、計算の定義とその実行を区別できることです。

この定義と実行が分離しているという性質により、再帰的定義を用いるべき箇所では気軽に用いることができるようになります。

結果として、積極評価を凌駕するモジュラリティの実現が容易になるでしょう。

たとえば、積極評価では、

  • ある性質の無限列を生成するもの
  • 列から指定個を取り出すもの

を、それぞれ個別に定義し、部品として使うことは難しいのです。

  • ある性質の無限列のうち指定個までを生成するもの

までしか、部品としては分割できないことが多いでしょう。

積極評価では無限を定義した上で、それを使ってしまったら、実際に無限個のデータを作り始めてしまうためです。

具体的には、

  • フィボナッチ数列のn番目までを作る
  • 素数列のn番目までを作る

という粒度の2つの処理を用意することは簡単ですが、

  • (無限の)フィボナッチ数列を作る
  • (無限の)素数列を作る
  • 数列のn番目までを取り出す

まで分割した粒度の3つの処理を用意し、これらを組み合わせることによって、

  • 「(無限の)フィボナッチ数列を作る」から「数列のn番目まで取り出す」
  • 「(無限の)素数列を作る」から「数列のn番目まで取り出す」

として元々の2つの処理と同じ処理を実現することは難しいのです。

後者のほうが、「数列のn番目までを取り出す」を共通部品として利用できているため、モジュラリティが高いのは明らかです。

( 中略 )

遅延評価では、無限に生成するような再帰的定義を行ったところで、実行も無限に行われてしまうわけではありません。
もし実行されれば定義に沿った値を提供しますが、実際には必要とされたところまでしか実行されません。

( 中略 )

遅延評価の言語では、定義と実行が区別されているからこそ、無限のデータ構造を定義して使ってしまっても問題ないのです。


関数型言語 & 関数型プログラミング に おける 数学の圏論 の 使われ方

Java8で関数が値として扱えるようになりました。

このことが、「関数が渡せると便利だよね」という観点ではなく、プログラミング言語としての能力をどのようにあげるか考えてみます。

圏論からのテクニックが使いやすくなる

集合論はどちらかというと値にたいする理論でしたが、圏論は関数呼び出しに関する理論です。

プログラムには、関数呼び出しを連結させて値を変換していくという側面があります。

そのような関数呼び出しの扱い方を整理するのが圏論で、圏論の考え方を使うことでより安定したプログラムを書くことができます。

モナドなど圏論由来のテクニックを使うには、どうしても関数を値として扱う必要があります。

関数を値として扱うことで、圏論のテクニックが使いやすくなり、安定したプログラムの書きやすさにつながります。

型の証明能力があがる

動的な型付の言語にくらべて、静的な型付の言語はプログラムが間違いにくいといわれます。

コンパイル時に検査ができるからなのですが、型の検査が通るということは、実は証明が行われたということになります。

カリー・ハワード同型対応といって、プログラムの型と、論理の証明は、同じものであることが示されています。

つまり、「Aという型である」ということは、「Aである」ということの証明です。

そして、「Aという引数をとってBを返す関数」を実装することは「AならばBである」ことの証明になります。

関数を値として扱うことでは、実際には証明能力は変わりませんが、命題の記述しやすさが変わり、コンパイルが通った時点で保証できる範囲が広げやすくなります。

カリーハワード同型対応での山場は、排中律がSchemeのcall/ccに対応するというところで、gotoなどもだいたいこれにあてはまるようです。

排中律、つまり「a または not a」という命題です。これは証明としてはアヤシイので、古典論理からはずしましょうとなって、直観主義論理というのができました。
これが、gotoはアヤシイのでプログラミング言語からはずしましょうという話に対応するわけです。ここがおもしろい。


Wikipedia で、「カリー=ハワード同型対応」について調べてみると、下記のように書いてあった。なるほど、やはり、そのものずばり、らしい。

ニコニコ大百科(仮)「単語記事: カリー=ハワード同型対応」

カリー=ハワード同型対応(Curry-Howard correspondence / Curry-Howard isomorphism)とは、プログラムと数学の定理が対応するという理論である。

概要

カリー=ハワード同型対応とは、入力(引数)や出力(戻り値)の「型」が命題に、プログラムが命題の証明に対応するという理論である。

定理証明によるプログラム検証の理論的根拠にあたる。

Wikipedia カリー=ハワード同型対応

add_2.png
add_3.png

WIKIBOOKS Haskell/カリー=ハワード同型

add_4.png

カリー=ハワード同型(Curry-Howard isomorphism)は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。

これよりカリー=ハワード同型は単に C-H と表記する。

C-H が示しているのは、定理の本質を反映するような型を構築し、それからその型を持つ値を見つけさえすれば、どんな数学的定理をも証明することができる、ということだ。これは最初は極めて不思議に思える。

型と定理にどんな関係があるというのだろうか?しかしながら、以下に述べるように、このふたつは非常に近しい関係にあるのである。

( 中略 )

Haskellの高階関数の機能を使えばとても複雑な型を構築することができる。

( 中略 )

信じられないことに、型が数学の論理における真である定理と対応するときだけ、型は空でないことがわかるのである。

( 中略 )

定理と型

それでは、形式論理においては型 a -> b は何を意味するのだろうか?
簡単なことに、単にa → bを意味しているのだ。

もちろん、これはa と bが形式理論において解釈可能な型であるときだけ成り立っている。これは C-H の本質である。また、先程述べたように、a -> b が空でない型であるとき、その時に限り a → bは定理となる。

もっとも単純な Haskell 関数のひとつを使ってみていこう。

const は a -> b -> a という型を持つ。
形式論理ではa → b → aとなる。

値constがあるので、これは型 a -> b -> a が空ではなく、定理であることは間違いない。

いま、a → bは「もしa が真だとすれば、b は真である」の別の表現なのである。

したがって、a → b → a は「もしaが真であり、もしbが真であるなら、aは真であると結論できることを意味する。
aが真であると仮定するなら、仮定によりaが真であるから、これはもちろん定理である。


( 以下がわかりやすい )

京都大学 哲学基礎文化学系ゼミナールⅡ(2009年)「カリー・ハワード同型対応入門」(1回目レクチャー)

(同上)2回目 レクチャー


定理証明支援言語 Agda, Coq

さて、当の「形式証明支援系言語 CoqAgda」だが、Qiita にも、CoqAgda、定理証明 のタグがあり、記事が投稿されていた。

まだまだ、これらの記事を読みこなすには道が遠そうだが、千里の道も1歩から入門のとっかかりになりそうなウェブサイト を、集めてみた。

Coq という言語

Wikipedia 「Coq」
Coq を始めよう ~ 〜 絶対にバグのないプログラムの書き方 〜

Coq は定理証明支援系言語です。定理証明、と聞いて皆さんは何を思い浮かべるでしょうか。多くの人は「数学」の二文字を連想し、「プログラミングは好きだけど数学はちょっと……」と思って積極的な気持ちを持たないかもしれません。 しかし、Coq の用途は数学の定理を証明することにも使われますが、むしろプログラムの正しさを保証したり、安全なプログラムを書く、といった用途で使われます。筆者は数学が好きで Coq に興味を持ったため、遊び感覚で数学の上の簡単な定理を示したりすることもあります。ただ、プログラムの証明を書くことの方が多く、そのときは数学と Coq は切り離して考えています。
ではプログラムの正しさを保証することにはどんな意味があるのでしょうか。テストをするだけでは何が足りないのでしょうか。たとえば、テストでは検査すべき状態が膨大になり、たくさんのテストケースが必要になる場合がありますが、もし証明できるのであれば証明は一回で十分です。このようにテストでなく証明が有用なケースがあり、実際にも利用されています。

Agda という言語

AgdaCoqはそれぞれ、OCamlHaskell と文法が近いだけでなく、これらの関数型言語で開発されているらしい??

Haskel などの関数型言語 との係わり合い

INRIA といえば、MATLAB の無償ツール版で知られる Scilab を開発・提供しているフランスの国立研究所だ。
グラン・ゼコール (Grandes Écoles) の École PolytechniqueÉcole Normale Supérieure で知られる秀才たちは、この分野でも世界のデファクト・スタンダードになるソフトウェアをつくりあげていたのか :dizzy_face:

SCILAB 日本語ページ

Scilabは、 INRIA (フランス国立 コンピュータ科学・制御研究所)と ENPC で 開発された高機能な科学技術ソフトウエアです。

2003年にScilab の開発は Scilab コンソーシアムに移管され、 現在は更にDigiteoに統合されて、 その1部門として Scilab コンソーシアムの活動を行っています。 2008年以降、Scilabは、GPL互換の FLOSS ライセンスに基づく オープンソースソフトウエアとして配布が行われています。

特徴を以下にまとめます。

Scilab は、UNIX,Mac,MS-Windowsで動作し、 自由に配布/使用することが可能です。
netlib 等で配布される高度な数値演算ライブラリを使用しており、 行列の固有値計算のみならず、各種のシミュレーション、 最適化計算、制御系設計、信号処理等に使用することが可能です。
カスタマイズ性に優れており、ユーザー定義の関数等を簡単に付加できます。
Xcos により、信号ラインをマウスで結ぶだけでシミュレーションが簡単に 実行可能です。(MATLAB(tm)のSimulink(tm) に似た機能を提供します。)
Scilabパッケージシステム ATOMSや Forge により、オプションのツールボックスを容易に入手/ インストールすることが可能です。

Qiita Theorem Prover Advent Calendar 2014

Qiita Theorem Prover Advent Calendar 2014

Qiita タグ

Qiita 「定理証明」タグ
Qiita_teirishoumei_tag.png

Qiita 「Coq」タグ
Qiita_Coq_tag.png

Qiita 「Agda」タグ
Qiita_Agda_tag.png

その他、使われている事例

  • (修士論文)定理証明支援系 Coq を用いた
    プログラム運算

    プログラム運算は,プログラムを,その意味を変えない運算定理を用いて,より効率のよいプログラムに書き換えていくプログラミング手法である.運算前のプログラムが自明に正しいプログラムであれば,運算後のプログラムも意味を保存しているため検証が不要であり,正しく効率のよいプログラム開発に貢献すると期待される.しかし,支援システムがなければ正しい運算は難しいにもかかわらず,支援システム開発のコストの高さなどから,広く使われている支援システムは少ない.

    本研究で,我々は定理証明支援系 Coq のライブラリによってプログラム運算を支援する手法を提案する。この手法は,Coq によって運算定理および運算定理の適用の正しさが保証される,対話的な運算ができる,拡張性が高いなどの特徴を持ち,その実装コストは高くない.

    本論文では,プログラム運算支援について論じ,支援システムの実装となる tactic ライブラリを紹介する.また tactic ライブラリを用いたプログラム運算理論の表現および運算の実例を紹介し,その際に現れる諸問題と,対処法について論じる

  • 関数型プログラミング言語と証明支援器を使った
    金融情報システムの開発について

    add.png

    add2.png

    add3.png

    add4.png

Coq 学習のとっかかり 参考サイト

参考情報(と紹介されているもの)

Coq本家のリファレンス

本家は王道

Jacques Garrigue先生の講義資料

数理解析・計算機数学がCoqの使い方っぽい

CPDT

Coqのすごい人の講義資料

Coqt

IIJのアルバイトの方が書いたCoqの入門記事

Coq'Art

Coqの中身についてもがっつり書いている

fm-forum

形式手法についての勉強会

ProofCafe

Proof Summit

函数プログラムの集い

勉強会

めっちゃ、お洒落やん :star2:

add7.png

学習サイト

まずは、この勉強会が公開しているウェブ教材をしっかり読み込んでみて、疑問点を書き出してみよう

ソフトウェアの基礎

study_guide_00.png

( 前書き )

study_guide_1.png

( 目次 )

study_guide_0.png


【 計算機科学 における 「圏論」の使用 】

( 指針 )

Joseph A. Goguen A CATEGORICAL MANIFESTO
Wikipedia 「圏論」

計算機科学のための圏論

計算機科学 (computing science) は、急速に発展した若い領域であることから、その領域内の諸概念を組織的に定式化する手法に未成熟であった。圏論はその計算機科学の必要としていた手法をもたらすものであったため、現在まで有効に活用されている。計算機科学における圏論の使用はジョセフ・ゴーグエンのA Categorical Manifestoによってその指針が与えられている。

WIKIBOOKS Haskell/Denotational semantics(表示的意味論)

導入

この章ではHaskellプログラムの意味がどのように形式化されるかという表示的意味論(denotational semantics)を説明します。

「square x = x*x というプログラムの意味は、数をその平方数に写す数学の平方関数だ」ということを形式的に規定することはつまらないことにみえるかもしれませんが、それでは f x = f (x+1) のような無限ループするプログラムの意味はどうでしょうか? 以下ではまずこの疑問に対するScottとStracheyのアプローチを例示し、概して関数プログラムの、特に再帰的な定義の正しさについて論じる基盤を得ることにしましょう。もちろん、これらのトピックではHaskellプログラムを理解するために必要なものに集中します。[1].

( 以下、灘高等学校 パソコン研究部 部誌所収 論考が秀逸である )
灘校 パソコン研究部 (部誌 記事一覧)
  • (2012年 部誌 所収)「Haskell でLazy K 処理系を作る」
  • (2013年 部誌 所収)「圏論によるプログラミングと論理」
  • (2014年 部誌 文化祭号 所収)「Haskell 再考」

( 書籍 )

kenron.PNG


( YouTube ) 「圏論勉強会」シリーズ動画

圏論勉強会

kenron_study_movie.png

「圏論」オンライン学習教材

定理証明支援系言語 紹介ウェブサイト


【 関連 】証明駆動開発

この章では、Coq で挿入ソートを定義し、定義したソート関数が実際にリストを整列させることを証明します。

次の章では、Extraction という機能を使って、ここで定義した挿入ソートを OCaml や Haskell、Scheme のコードへ変換する方法を紹介します。

証明駆動開発

これまで Coq で色々な関数を定義し、定義した関数の性質を証明してきましたが、実際に Coq を使って安全性の保証されたソフトウェアを開発するところまでは解説しませんでした。

Coq で安全なソフトウェアを開発する流れは、

(1) まず書こうとしているプログラムがどういう性質をみたすべきかを記述し、
(2) Coq でそれをみたすようなプログラムを書き、
(3) 実際に最初に考えた性質を証明し、
(4) Extraction して他の言語のコードに変換する

となります。

このように、プログラムがみたすべき性質に合うようにコーディングし、ソフトウェアを開発するという考え方は「証明駆動」と呼ばれています。

これから二回にわたり、上の流れに沿ってリストをソートする関数をプログラミングしていきます。今回は他のソートアルゴリズムより証明が易しい、挿入ソートを実装します。


【 参考 】

Qiita 上の Coqによる定理証明 実例コード 掲載記事(一部)


Coq 学習サイト

Coq による「四色定理」の証明(最初の証明は、すでに1970年代に Appel and Haken の手でなされていたが、手作業を交えた長大な証明であった)

( 参考 )

( 関連 )四色定理を利用したアプリ)

Coq による「Feit-thomson定理」の証明

Microsoft と INRIA との共同研究所とは?

The Microsoft Research-Inria Joint Centre was founded by Inria (the French National Research Institute for Computer Science and Applied Mathematics), Microsoft Corporation, and the Microsoft Research Laboratory Cambridge.
The Centre's objective is to pursue fundamental, long-term research in Computer Science with a particular emphasis on formal methods and machine learning and some of their key applications.

In April 2005, the French Minister for Research, Gilles Kahn, Chairman of Inria , and Steve Ballmer, Chief Executive Officer of Microsoft Corporation, signed a memorandum of understanding and announced the creation of a joint laboratory in France.
In October 2005, the French Minister for Research, Gilles Kahn, and Bill Gates, founder of Microsoft, signed a framework agreement.

a new laboratory was created on the Plateau de Saclay, near the campus of INRIA Saclay, University of Orsay, Ecole Polytechnique, and Supelec.

Three research projects on Formal Methods and Security were launched in May 2006.


形式手法・定理証明 入門書籍 紹介ウェブサイト

前エントリー「僕が形式手法を学び始めたときに読んだ10冊 - masaterukの日記」のラインナップはあまりに入手困難なものばかりだったので、2012年に始めるならということで改めて選んでみた。

形式手法・定理証明 紹介解説ウェブサイト

(以下、ヴィッツ社ウェブページより抜粋して図表を転載)

formal_method_tools.PNG


Coq 以外の形式証明器・定理証明器

VDM(the Vienna Development Method)

VDMとは?

VDMは形式手法の1つであり、1960年代にIBMウィーン研究所で開発されました。 VDMには「VDM-SL」「VDM++」という2つの形式仕様記述言語があり、「VDM-SL」はISO標準となっています。
「VDM++」はVDM-SLを基礎にオブジェクト指向拡張を行った言語です。 VDMは形式手法の中でもモデル規範型と呼ばれ、モデルの状態を記述していくことに重点を置いています。

VDMTools

VDMToolsはデンマークのPeter Gorm Larsen博士が開発したVDM開発支援ツールであり、Windows・Linux・Mac OS Xで動作します。
また、ツール・マニュアル共に日本語化されており、日本の開発現場での使用に向いています。

2005年にSCSK(旧 CSKシステムズ)がデンマークの開発元から全ての権利を取得し、全世界に向けて提供しています。

VDMToolsは、形式技術と実用技術を巧みに統合し、現在は以下の機能を提供します。

VDMを始めるには、まずVDMToolsをダウンロードしましょう。

VDMToolsは、このWebサイトにユーザ登録すると
[ダウンロード] からダウンロードできます。

次にVDMとツールの使い方を例題を使って学んでいきましょう。

VDM開発環境の構築

VDMToolsやOvertureによる開発環境の構築方法があります。

VDMToolsチュートリアル

VDMToolsの基本的な操作方法が記述してあります

例題で覚えるVDM

VDMの問題と解答が載っています

目次

開発に必要なもの
VDMToolsインストール
エディタインストール・環境設定
参考URL

The Overture community supports the modelling method The Vienna Development Method (VDM) which is a set of modelling techniques that have a long and successful history in both research and industrial application in the development of computer-based systems.

The Overture Tool is an open-source integrated development environment (IDE) for developing and analysing VDM models. The tool suite is written entirely in Java and built on top of the Eclipse platform.


Z、B

【 応用事例 】

( 関連記事 )