日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

Java プラットホーム上での Coq 検証済みコードの実行について
湯浅 能史

田辺 良則

定理証明法によるソフトウェア検証は、数学的なモデリングが可能なら、原理的には必ず適用できるという意味で、非常に強力な検証手法である。しかしながら、実用的な適用例に関しては、残念ながら現状では限定的と評価せざるを得ない。その原因の一つは、開発現場で主流となっている言語で開発されたシステムとの親和性にあると思われる。現在、我々は、Java プラットホームを対象に、証明支援系 Coq による検証済みコードを、他のプログラムとシームレスに結合して利用する方法の研究を進めている。本講演では、Coq 言語で書かれたプログラムを、Java 仮想マシン上のインタープリタで直接実行する方法や、Java 言語の関数型への拡張である Scala 言語に変換する方法などを紹介し、それぞれの評価を元に議論したい。

るのが普通である。しかし、そのような場合でも検証

1 はじめに手法として、定理証明法が用いられることはあまり無定理証明の方法によるソフトウェア検証は、モデルい。技術者不足を脇に置けば、これは、作成される検検査と並ぶ代表的な形式手法による検証方法である。

証済みコードが、システムの他の部分や全体の実行環数学的なモデリングが可能なら、原理的には必ず適用境などとの親和性が低いことに原因があると思われできるという意味で、潜在的には極めて強力な方法でる。定理証明法が得意とするのは、主に関数型プログはあるが、その適用事例は決して多くはない。モデル

ラムの検証であり、また最終的に生成される実行コー検査手法がかなり普及していることと比較すると大ドも、特定の関数型言語のものに限られていることがきな差がある。

多い。一方、システム全体をこのような言語で開発・普及を妨げる要因として、よく挙げられるのは、検運用するケースは、現状では稀である。

証に要する工数が比較的大きいことや、この手法を扱

しかし、これに関しては、近年、若干の状況の改善える技術者が少ないなど、開発体制やコストに関わるが見られる。Java 言語に関数型言語の特徴を統合しことである。その一方で、プログラミング言語をはじた Scala 言語が提案され、Web サービスの開発現場めとするシステムの開発環境や、想定している動作環などで徐々に普及してきている。このような背景を踏境に関する要因も無視できない。実際のシステム開発

まえ、我々は、証明支援系 Coq で検証した関数プロにおいては、ソフトウェアのすべての部分が検証の観グラムを Java プラットホーム上で、他のプログラム点から同等の重要性を持つわけでは無く、高度な信頼とシームレスに結合して動作させる方法を研究して性を期待されるごく一部分にのみ検証手法を適用すいる。我々が検討しているのは、主に以下の２つの方法である。

Yoshifumi Yuasa, 神 奈 川 大 学 総 合 理 学 研 究 所, Research Institute for Integrated Science, Kanagawa
University.
Yoshinori Tanabe, 鶴 見 大 学 文 学 部 ド キュメ ン テ ーション 学 科, Department of Library, Archival andInformation Studies School of Literature, Tsurumi
University.

• Coq 言語の証明式からの Scala プログラム抽出• Java 仮想マシン上で動作する Coq 言語処理系の開発
本稿では、この研究のこれまでの経緯や現状、また今後の計画について概要を述べる。

2 プログラム抽出

3 Scala による Coq 言語処理系の実装

Coq システムは元々、証明からプログラムを抽出

本節で述べるのは Coq 言語を Java 仮想マシン上する仕組みを備えている [3]。抽出できるプログラミで直接処理する方法である。まだ研究は初期段階でング言語は OCaml(ML), Haskell, Scheme の３つであり、システムの基本部分を作成しているところであある。これらは全て関数型言語である。

る。ここでは設計/実装の方針について、現時点で考Scala 言語は、その関数型言語としての側面においえているものを簡単に説明する。ては、 ML に類似したものと理解できる。Java から実装言語は Scala である。システムは Coq の宣言引き継いで拡張したクラス機構は ML の型システムと文列を読み、それらが形成する関数評価環境を Scala

凡そ自然な対応関係があり、これを踏まえれば、Coqのオブジェクトとして作成する。他のオブジェクトシステムの OCaml プログラム抽出ツールを Scala

は、これにメッセージとして Coq 式を送り、戻り値プログラム向けに改造することができる。今井 [2] はとして評価値を得る、という形で Coq コードとの連これを実際に行い、抽出先言語として Scala を追加携を図ることが可能になる。また、効率的連携を可能する拡張を行っている。しかし、これは Coq システにするため、以下の２点をシステム設計上の課題としムの特定の実装に強く依存しているため、そのバーて掲げた。

ジョンアップに追随するコード修正が頻繁に必要とな

1. 無駄のない関数評価戦略るという難点がある。

2. Scala 関数の Coq 言語への埋め込み

逸見ら [1] は、この点に鑑み、既存の Coq システム

Coq 言語の証明式には、処理の記述とその正当性の実装変更の影響を受けにくい別の方法を試みてい証明が混在している。評価戦略の如何によっては、簡る。Coq システムにおいては、証明から対象言語のプ約化が後者に対しても適用されてしまい、大きなオーログラムを直接抽出しているわけではない。簡易 MLバーヘッドになる場合もある。最終的な出力に不必要言語である Mini-ML のプログラムをまず抽出し、後な計算はできるだけ行わずに済ませるために、遅延にこれをそれぞれの対象言語へ変換しているのであ評価 (lazy evaluation) を基本的な評価戦略としたい。

る。逸見らの方法では、この中間的な Mini-ML プ

課題 2 は、既存の Scala ライブラリ等を有効に利用ログラムを元に Scala コードを生成する。Mini-MLする上で特に重要である。これをどのような形で実現の言語仕様は シンプルで普遍性のあるものなので、するかについては、現在検討中である。

Coq システムのバージョンアップ等でも、変更されることはまず無いと思われる。

なお、Coq 言語処理系の独自実装には、別の応用も考えられる。それは、前節で述べたた Scala コー

一方、この方法の難点は Coq による Mini-ML コー

ド抽出を Java 仮想マシン上で行えるようにすること

ド抽出の際に多くの型情報が失われてしまう点にあである。これにより、特定の Coq システム実装へのる。その結果、Scala コンパイラが必要とする型情報依存が無くなり、今井の方法の難点を克服することがを復元することができず、変換が失敗に終わこるとができる。

ある。通常の ML 言語であれば完全な型推論が可能だが、ここで用いている Mini-ML は、任意の型キャ

4 まとめと今後の展望ストを行う特殊関数を含んでおり、またプログラム抽

本稿では Java プラットホーム上での、Coq 検証済

出アルゴリズムもこれに大きく依存しているため、状コードを利用する方法についての、我々のこれまでの況の改善には相応の困難が伴うと思われる。

研究を紹介した。現在、前二節に述べたツールや処理系の改善/開発を進めている。
最後に今後の展望について述べたい。本稿で述べた手法は、検証 “済み” コードをの利用を目指したものであるが、今後はこれまで得た知見を踏まえつつ、者（サービスを受ける側）に伝えることもできる。こより発展的な研究テーマとして Java オブジェクト指のような考え方は、契約プログラミング (Design by

向プログラミングにおける検証 “付き” コード (ProofContract) における形式手法や、それに基づくシステCarrying Code) の利用についても視野に入れていきム検証等に、応用できるのではないかと予想してる。

たい。関数プログラミングにおいては、基礎となる型理論を依存型に強化することで、関数定義と定理の証

参 考 文 献明を、同一の枠組みで扱うことができるようになる[ 1 ] 逸見港，田辺良則，今井宜洋，萩谷昌己: 検証済みのコードによる Coq から Scala へのコード抽出． 第31 回ソフトウェア科学会大会．(2014)[ 2 ] Yoshihiro Imai, Coq2scala for coq8.3.(2012)
http://proofcafe.org/wiki/Coq2Scala[ 3 ] Pierre Letouzey, Certified functional programming - Program extraction within Coq proof assistant. PhD thesis, University Paris-sud (2004)[ 4 ] The Coq Development Team. The coq proof assistant. http://coq.inria.fr[ 5 ] The Scala Development Team. The scala programming language. http://scala-lang.org

ことが知られている。Coq 等の定理証明系はこの原理 (Curry-Howard 対応) を応用したものである。型理論に対する同様の強化を、適切な形で Scala 言語
でも行うことができれば、システムが提供するサービスの正当性証明を、関数オブジェクトとして表現して保持できるようになると思われる。また、状態遷移の確証を、オブジェクトの受け渡しによって他