形式論理教育ツール Mizar-MSE 用統合環境の実装
Implementation for the proof checker Mizar-MSE福良 博史 FUKURA Hirofumi １．緒 言 これからのソフトウェア技術者が身に付けて おくべき基本的な知識の一つは形式論理学であ ると考えている。これがなぜソフトウェア技術 者に必要なのかというと、高信頼性を維持した ソフトウェア・システムを構築するためには、 現在のソフトウェア工学の技術レベルにおいて、 形式手法がその解決への入り口と考えるからで ある。この手法を用いるためには、形式論理学 の知識と訓練が欠かせない。 ソフトウェア設計手法の一つであるオブジェ クト指向による設計方法論のUML には、OCL という言語が用意されている。この言語も形式 手法の一種と考えられている。この言語を理解 するためにも形式手法の知識が必要である。 そのため、東京校において形式論理の教育・ 訓練を情報技術科の二年生を対象に3 年前から 実施している。 形式論理を、集合教育で教える上で困難なこ とは、証明が正しいか否かを確認する方法が紙 の上での記述だけでは、個々人のレポートを読 み、厳密な検証を行うときに、論理の飛躍や、 微妙に誤っている論証を総てチェックするため の時間がなかなかとれず、誤りを見落としやす くなり、実質的な訓練にならなくなる恐れがあ る。また別の観点で考えると、高校や大学の数 学のテキストにおいて証明が「自明である」と 書かれてしまうと、人により理解の深さが異な っているため、理解できる人、理解できない人、 誤解する人などが出てくる。そして実は「自明 である」と書いたのが誤りで、そのような証明 が不可能かもしれない。 このように論証を紙の上で行っている場合は、 誤りが見過ごされる危険性がある。形式論理の 証明の内容についての教育訓練を行う場合、こ のような、「自明である」というような論理の飛 躍を許さず、きちんと証明の基本ルールに則り、 誰もが納得のいくプロセスで証明が行われるこ とが必要である。これを可能にするためには、 何らかのツールが必要となる。このツールは、 自動証明のツールではない。自動証明の場合は、 結果が出るまでに長時間かかる場合もある。ま た証明できないこともある。ここで求めている ツールは、プルーフ・チェッカであり、これは、 証明の記述に誤りがあるか否かを検証してくれ る。このツールは、証明の記述がルール通りに 行われているか否かを判定するだけなので、プ ルーフ・チェッカが試行錯誤することはない。 そのため、処理時間が予測できないほど長時間 かかることはありえない。 プルーフチェッカMizar というツールがある。 しかしこれは専門家がそれなりの訓練を積んで からでないと使いこなせない。そこで専門家向 けではない、初心者向けの証明の検証をおこな ってくれるツールMizar-MSE を用いて教育訓 練を実施することとした。このツールは、Linux
上でCUI（Character-based User Interface） インターフェースで用いられていた。それを Windows で動作できるように、東京校において
改造し、利用していた(1)。この実習を始めて 3
年 目 と な る 今 年 度 は 、 こ の ツ ー ル を GUI （Graphical User Interface）形式で利用でき
るように改造した。この改造はJava にて行っ
た。この改造方法を紹介し、今後、同様なツー ルの改造をより汎用的に実装するための方式を 提案する。
２．Mizar-MSE の機能分析 ２．１ CUI インターフェース・ツールの基本 プルーフ・チェッカの機能は、コンパイラに 似ている。コンパイラの場合は、プログラムの コードを記述し、そのコードをコンパイルし、 文法上の誤りが無ければ、オブジェクトを出力 する。コンパイラを利用する目的は、コンパイ ラが生成したオブジェクトを用いてソフトウェ アを動かすことにある。プルーフ・チェッカの 場合は、証明のコードを記述し、その内容が、 ルールに則っているか否かを判定する。この場 合重要なのは証明の正しさに対する診断結果で ある。CUI ツールとして必要なものは、証明の コードを入力し、構文解析し、構文上の誤りが あればそれを指摘する。構文上の誤りが無い場 合は、証明の記述に飛躍や無理がないか、証明 のルールに則っているかを調べ検証の妥当性を 調べ、その結果を表示する。 Mizar-MSE の場合は、テキスト・ファイル から論証のコードを入力し、その診断結果を標 準出力している。 ２．２ Mizer-MSE の利用方法 Mizar-MSE を利用するためには、以下のよ うな手順を踏んで利用することになる。 手順１：テキスト・エディタで証明のコードを 記述し、保存する。 手順２：コマンド・プロンプトを起動する。 手順 3：コマンド・プロンプトから必要なディ レクトリに移動し Mizar-MSE を起動 する。このとき、手順１で作成したフ ァイルを入力として指示する。 手順４：診断結果が標準出力に表示される。 手順５：診断結果を見て間違いがあれば、手順 １に戻る。 このようなツールを使うことで、集合教育で も、ツールが、あたかも個人ごとのチュータの ような役割を担ってくれている。個人ごとに証 明の書き方に間違いがあれば、指摘してくれる。 また、論証が飛躍している場合も指摘してくれ る。しかし、その推論方法が根本的におかしい のか、または若干飛躍しているのかの判断は、 ツールでは判断できない。この点は、学生がど うしても証明できないときに教官に質問しに来 て、教官がその意味を説明することで学生の理 解が進む。つまり学生と教官との対話が、論証 の本質的な内容近辺での議論となる。すなわち 本質的な考え方の訓練に、教官が集中できるよ うな環境が整えられる、と考えている。 パスの設定やスクリプトの記述などを知って いる人は、CUI インターフェースのツールを使 うことに抵抗感を感じていない。しかし近年 GUI 操作には慣れていてもコマンド・プロンプ トで操作をする環境に不得手の人が増えている。 このような状況において、形式論理を訓練する ために、パソコンの操作に重点を置いている余 裕は無いので、GUI インターフェースでのワン ストップサービスという観点から、ツールの使 い勝手の工夫を考えた。 ２．３ ユニバーサル・デザインの７原則 ツールの使い勝手を考える上で、以下に示す ユニバーサル・デザインの7 原則(2)を参考とし た。 第一原則（公平性）への適合性 すべてのユーザにとってGUI の起動に より、誰もが同じ方法で各種メニューを 開くことにより使えるようにデザインさ れている。 第二原則（柔軟性）への適合性 テキスト・エディタの利用、プルーフチ ェッカの利用その他各種機能は，メニュー から選択することによりサービスが受け られる。このためユーザが自分の理解や早
さのペースに合わせて自身でメニューを 選択し行動をすることができるようにデ ザインされている。 第三原則（シンプル）への適合 統合環境として，テキスト・エディタ もプルーフチェッカも一つのツールの中 にメニューで選択して作業ができるよう にシンプルなデザインを採用している。 第四原則（理解容易）への適合 メニューを見ると何ができるのかが容 易に理解できるようにデザインされて いる。 第五原則（寛容）への適合 操作に異常が見受けられた場合は、警告 を発するようにデザインされている。 第六原則（操作極小）への適合 統合環境としたことで，別々のツール をその都度呼び出したりすることなく、 メニューから選択することで必要な機 能をすべて扱えるように操作性を極力 減少させたデザインとなっている。 第七原則（サイズ・空間）への適合 テキスト・エディタのフォントを３種 類用意した。このことにより人それぞれ の見易い文字の大きさを選択できる。ま たプレゼンテーション用に大きな文字 を表示することが可能なデザインとな っている。 ３．Mizar-MSE 統合環境 ３．１ Mizar-MSE の GUI 化した統合環境 上記のようにこのツールを設計する上で、ユ ニバーサル・デザインの７原則を参考に使い勝 手の機能を考えた。GUI 化したツールと、この 7 原則には違和感がなく、自然と機能の選別が できた。２．２で述べた各ステップを踏む手順 を GUI 化したツールの中に一体化することが できた。 このツールは、ワンストップ・サービスとし ての統合環境を目指したツールである。このた め、テキスト・エディタとプルーフチェッカを 一つにまとめてGUI 化し、各種メニューをクリ ックしていくことで証明の格納、再読み込み、 Mizar-MSE による検証などが統一して操作で きるようになっている。 図１に今回製作したツールの画面例を、図２ に実装したMizar-MSE 統合ツールの概要を示 す。 図１ Mizar-MSE の GUI 化した統合環境ツールの画面例
３．２ Mizar-MSE 統合環境の実装方針 このツールを設計する上で、考慮したこと は、元のツールに手を加えるのは、コードが 公 開 さ れ て い る 場 合 は 簡 単 で あ る と い う こ とである。このツールの場合もコードが公開 されているので、コードを改造することがで きる。しかしそれではこのツール独自の改造 となってしまう。それではあまり汎用性がな い。特殊な改造に留まる。 今回の方針として、今回のようなGUI化さ れていないツールを、一定の条件が整えばど のような場合でもGUI化が可能となる。つま りソースコードが公開されていなくてもGU I化が可能な方策を検討した。その結果今回 採 用 し た 実 装 上 の 考 え 方 は 以 下 の 通 り で あ る。 (1) メニュー形式による機能の呼び出し (2) エディタ機能の組込み (3) Mizar-MSEをバッチファイルとし、バッ チファイルの起動 （注）この仕組みにより、エディタで作成し たコードを外部ファイルとし、バッチファ イルの入力とする。そして、標準出力も外 部ファイル化しておく。つまり、形式論理 の検証結果をユーザに見せるための情報を 引き継げるようにしておく。 (4) 検証結果をファイルから読み込み画面表 示 ３．３ Mizar-MSE 統合環境のコード例 こ の ツ ー ル を 構 築 す る 上 で の 骨 格 部 分 の 具体的なコード例を以下に示す。 図３ バッチファイルの起動部分 図３にバッチファイルの起動箇所のコード 例を示す。この場合、cmdというのがコマンド プロンプトを起動することであり、コマンドプ ロンプトで、mizarmse.batというバッチファ イルを起動している。このバッチファイルの内 容は、図４に示す。 図４ バッチファイルの内容 verification.logという名前のファイルが、Miz ar-MSEの検証結果を標準出力となっている
private void nowVerify() { //検証 try{ String cf = currentFile.getName(); Process p = Runtime.getRuntime().exec( "cmd /c start ..¥¥MizarMSE¥¥mizarmse.bat " + cf); } catch (Exception e) { e.printStackTrace(); } } cd ..¥MizarMSE mizar-mse<..¥sources¥%1 > ..¥log¥verification.log exit 統合環境制御 エディタ バッチ起動 証明のコード 証明の結果 モニター 表示 結果表示 実線の矢印：制御の関 係 図２ Mizar-MSE の統合ツールの構成イメージ
ものを、テキストファイルとして格納している。 この情報の受けとり方はは、図５のように、検 証結果のverification.logを読み込み、画面に表 示している。 図５ 検証結果の受取表示例 ４．ツールの汎用化 このようなツールを個々に実装するのは、人 手がいくらあっても足りなくなる。そこで、C UIとして用いているツールをGUI化すること が汎用的な環境定義を行うことにより利用で きるようになると、色々な過去のツールが使い やすくなる可能性がでてくる。 このようにツールを汎用化させるためには、 外部定義により、色々な条件を入力し、これを 解釈して、その定義に応じてツールの機能がイ ンタープリティブに変化するようにできれば よい。このための外部定義は、XMLでの記述 形式を用いると、人が見て、理解しやすい構造 で定義体を記述できる。このように現在のツー ルを改造すると、概ね図６のような形態になる。 このときに定義体に必要な機能的な内容は、 表１に示したような項目が考えられる。 private void confirmVerify() { //検証結果確認
try {
BufferedReader reader = new BufferedReader( new FileReader(
"..¥¥log¥¥verification.log")); StringBuilder sb = new StringBuilder(); for(String line; (line=reader.readLine())!=null;) { sb.append(line+"¥n"); } reader.close(); textArea.setText(sb.toString()); } catch (IOException e) { e.printStackTrace(); } } 実線の矢印：制御の関 係 図６ 汎用化した統合ツールのイメージ 統合環境制御 エディタ バッチ起動 コード 実行結果 モニター 表示 結果表示 XML での定義
５．まとめ このツールを利用して、3年目の教育訓練 を行っている。今後使い勝手の情報を収集し、 よりよいものにしていくことが望まれる。 なお、このツールのXML化を今後検討し ていきたいと考えている。こうすることによ り、他のツールに対しても同じような機能の 提供が簡単にできる可能性がでてくる。 参考文献 (1)福良博史：”プルーフ・チェッカ Mizar-MSE を 用 い た 形 式 論 理 の 実 践 的 な 教 育 訓 練 法” ,Proceedings of the Technical Symposium and General Assembly of Mizar JAPAN (Spring 2007) Volume 2, Number 1, May 18, 2007 (2)ユニバーサル・デザインの 7 原則 http://www.design.ncsu.edu/cud/ about_ud/udprinciples.htm 表１ 定義体に必要な機能 No 機 能 1 画面のタイトル 2 メニューの種類 3 エディタの有無 4 バッチファイルの指示 5 入力情報の指示 6 出力情報の指示 7 排他制御の必要なプロセスの指示 8 並列処理が可能なプロセスの指示 9 シリアライズが必要なプロセスの指示 10 エラーへの対処
