2.Mizar-MSE の機能分析 2.1 CUI インターフェースツールの基本プルーフチェッカの機能はコンパイラに似ているコンパイラの場合はプログラムのコードを記述しそのコードをコンパイルし文法上の誤りが無ければオブジェクトを出力するコンパイラを利用する目的はコンパイラが生成し

Size: px

Start display at page:

Download "2.Mizar-MSE の機能分析 2.1 CUI インターフェースツールの基本プルーフチェッカの機能はコンパイラに似ているコンパイラの場合はプログラムのコードを記述しそのコードをコンパイルし文法上の誤りが無ければオブジェクトを出力するコンパイラを利用する目的はコンパイラが生成し"

さやなこうだ
5 years ago
Views:

1 形式論理教育ツール Mizar-MSE 用統合環境の実装 Implementation for the proof checker Mizar-MSE 福良博史 FUKURA Hirofumi 誤りが見過ごされる危険性がある形式論理の証明の内容についての教育訓練を行う場合このような自明であるというような論理の飛躍を許さずきちんと証明の基本ルールに則り誰もが納得のいくプロセスで証明が行われることが必要であるこれを可能にするためには何らかのツールが必要となるこのツールは自動証明のツールではない自動証明の場合は結果が出るまでに長時間かかる場合もあるまた証明できないこともあるここで求めているツールはプルーフチェッカでありこれは証明の記述に誤りがあるか否かを検証してくれるこのツールは証明の記述がルール通りに行われているか否かを判定するだけなのでプルーフチェッカが試行錯誤することはないそのため処理時間が予測できないほど長時間かかることはありえないプルーフチェッカ Mizar というツールがあるしかしこれは専門家がそれなりの訓練を積んでからでないと使いこなせないそこで専門家向けではない初心者向けの証明の検証をおこなってくれるツール Mizar-MSE を用いて教育訓練を実施することとしたこのツールは Linux 上で CUI(Character-based User Interface) インターフェースで用いられていたそれを Windows で動作できるように東京校において改造し利用していた (1) この実習を始めて 3 年目となる今年度はこのツールを GUI (Graphical User Interface) 形式で利用できるように改造したこの改造は Java にて行ったこの改造方法を紹介し今後同様なツールの改造をより汎用的に実装するための方式を提案する 1. 緒言これからのソフトウェア技術者が身に付けておくべき基本的な知識の一つは形式論理学であると考えているこれがなぜソフトウェア技術者に必要なのかというと高信頼性を維持したソフトウェアシステムを構築するためには現在のソフトウェア工学の技術レベルにおいて形式手法がその解決への入り口と考えるからであるこの手法を用いるためには形式論理学の知識と訓練が欠かせないソフトウェア設計手法の一つであるオブジェクト指向による設計方法論の UML には OCL という言語が用意されているこの言語も形式手法の一種と考えられているこの言語を理解するためにも形式手法の知識が必要であるそのため東京校において形式論理の教育訓練を情報技術科の二年生を対象に 3 年前から実施している形式論理を集合教育で教える上で困難なことは証明が正しいか否かを確認する方法が紙の上での記述だけでは個々人のレポートを読み厳密な検証を行うときに論理の飛躍や微妙に誤っている論証を総てチェックするための時間がなかなかとれず誤りを見落としやすくなり実質的な訓練にならなくなる恐れがあるまた別の観点で考えると高校や大学の数学のテキストにおいて証明が自明であると書かれてしまうと人により理解の深さが異なっているため理解できる人理解できない人誤解する人などが出てくるそして実は自明であると書いたのが誤りでそのような証明が不可能かもしれないこのように論証を紙の上で行っている場合は -66-

2 2.Mizar-MSE の機能分析 2.1 CUI インターフェースツールの基本プルーフチェッカの機能はコンパイラに似ているコンパイラの場合はプログラムのコードを記述しそのコードをコンパイルし文法上の誤りが無ければオブジェクトを出力するコンパイラを利用する目的はコンパイラが生成したオブジェクトを用いてソフトウェアを動かすことにあるプルーフチェッカの場合は証明のコードを記述しその内容がルールに則っているか否かを判定するこの場合重要なのは証明の正しさに対する診断結果である CUI ツールとして必要なものは証明のコードを入力し構文解析し構文上の誤りがあればそれを指摘する構文上の誤りが無い場合は証明の記述に飛躍や無理がないか証明のルールに則っているかを調べ検証の妥当性を調べその結果を表示する Mizar-MSE の場合はテキストファイルから論証のコードを入力しその診断結果を標準出力している 2.2 Mizer-MSE の利用方法 Mizar-MSE を利用するためには以下のような手順を踏んで利用することになる手順 1: テキストエディタで証明のコードを記述し保存する手順 2: コマンドプロンプトを起動する手順 3: コマンドプロンプトから必要なディレクトリに移動し Mizar-MSE を起動するこのとき手順 1で作成したファイルを入力として指示する手順 4: 診断結果が標準出力に表示される手順 5: 診断結果を見て間違いがあれば手順 1に戻るこのようなツールを使うことで集合教育でもツールがあたかも個人ごとのチュータのような役割を担ってくれている個人ごとに証明の書き方に間違いがあれば指摘してくれるまた論証が飛躍している場合も指摘してくれるしかしその推論方法が根本的におかしいのかまたは若干飛躍しているのかの判断はツールでは判断できないこの点は学生がどうしても証明できないときに教官に質問しに来て教官がその意味を説明することで学生の理解が進むつまり学生と教官との対話が論証の本質的な内容近辺での議論となるすなわち本質的な考え方の訓練に教官が集中できるような環境が整えられると考えているパスの設定やスクリプトの記述などを知っている人は CUI インターフェースのツールを使うことに抵抗感を感じていないしかし近年 GUI 操作には慣れていてもコマンドプロンプトで操作をする環境に不得手の人が増えているこのような状況において形式論理を訓練するためにパソコンの操作に重点を置いている余裕は無いので GUI インターフェースでのワンストップサービスという観点からツールの使い勝手の工夫を考えた 2.3 ユニバーサルデザインの7 原則ツールの使い勝手を考える上で以下に示すユニバーサルデザインの 7 原則 (2) を参考とした第一原則 ( 公平性 ) への適合性すべてのユーザにとって GUI の起動により誰もが同じ方法で各種メニューを開くことにより使えるようにデザインされている第二原則 ( 柔軟性 ) への適合性テキストエディタの利用プルーフチェッカの利用その他各種機能は, メニューから選択することによりサービスが受けられるこのためユーザが自分の理解や早 -67-

さのペースに合わせて自身でメニューを選択し行動をすることができるようにデザインされている第三原則 ( シンプル ) への適合統合環境として, テキストエディタもプルーフチェッカも一つのツールの中にメニューで選択して作業ができるようにシンプルなデザインを採用している第四原則 ( 理解容易 ) への適合メニューを見ると何ができるのかが容易に理解できるようにデザインされている第五原則 ( 寛容

3 さのペースに合わせて自身でメニューを選択し行動をすることができるようにデザインされている第三原則 ( シンプル ) への適合統合環境として, テキストエディタもプルーフチェッカも一つのツールの中にメニューで選択して作業ができるようにシンプルなデザインを採用している第四原則 ( 理解容易 ) への適合メニューを見ると何ができるのかが容易に理解できるようにデザインされている第五原則 ( 寛容 ) への適合操作に異常が見受けられた場合は警告を発するようにデザインされている第六原則 ( 操作極小 ) への適合統合環境としたことで, 別々のツールをその都度呼び出したりすることなくメニューから選択することで必要な機能をすべて扱えるように操作性を極力減少させたデザインとなっている第七原則 ( サイズ空間 ) への適合テキストエディタのフォントを3 種類用意したこのことにより人それぞれの見易い文字の大きさを選択できるまたプレゼンテーション用に大きな文字を表示することが可能なデザインとなっている 3.Mizar-MSE 統合環境 3.1 Mizar-MSE の GUI 化した統合環境上記のようにこのツールを設計する上でユニバーサルデザインの7 原則を参考に使い勝手の機能を考えた GUI 化したツールとこの 7 原則には違和感がなく自然と機能の選別ができた 2.2で述べた各ステップを踏む手順を GUI 化したツールの中に一体化することができたこのツールはワンストップサービスとしての統合環境を目指したツールであるこのためテキストエディタとプルーフチェッカを一つにまとめて GUI 化し各種メニューをクリックしていくことで証明の格納再読み込み Mizar-MSE による検証などが統一して操作できるようになっている図 1に今回製作したツールの画面例を図 2 に実装した Mizar-MSE 統合ツールの概要を示す図 1 Mizar-MSE の GUI 化した統合環境ツールの画面例 -68-

4 統合環境制御エディタバッチ起動結果表示証明のコード証明の結果モニター表示実線の矢印 : 制御の関係図 2 Mizar-MSE の統合ツールの構成イメージ 3.2 Mizar-MSE 統合環境の実装方針このツールを設計する上で考慮したことは元のツールに手を加えるのはコードが公開されている場合は簡単であるということであるこのツールの場合もコードが公開されているのでコードを改造することができるしかしそれではこのツール独自の改造となってしまうそれではあまり汎用性がない特殊な改造に留まる今回の方針として今回のようなGUI 化されていないツールを一定の条件が整えばどのような場合でもGUI 化が可能となるつまりソースコードが公開されていなくてもGU I 化が可能な方策を検討したその結果今回採用した実装上の考え方は以下の通りである (1) メニュー形式による機能の呼び出し (2) エディタ機能の組込み (3) Mizar-MSEをバッチファイルとしバッチファイルの起動 ( 注 ) この仕組みによりエディタで作成したコードを外部ファイルとしバッチファイルの入力とするそして標準出力も外部ファイル化しておくつまり形式論理の検証結果をユーザに見せるための情報を引き継げるようにしておく (4) 検証結果をファイルから読み込み画面表示 3.3 Mizar-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(); 図 3 バッチファイルの起動部分図 3にバッチファイルの起動箇所のコード例を示すこの場合 cmdというのがコマンドプロンプトを起動することでありコマンドプロンプトで mizarmse.batというバッチファイルを起動しているこのバッチファイルの内容は図 4に示す cd.. MizarMSE mizar-mse<.. sources %1 >.. log verification.log exit 図 4 バッチファイルの内容 verification.logという名前のファイルが Miz ar-mseの検証結果を標準出力となっている -69-

5 ものをテキストファイルとして格納しているこの情報の受けとり方はは図 5のように検証結果のverification.logを読み込み画面に表示している 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(); 図 5 検証結果の受取表示例 4. ツールの汎用化このようなツールを個々に実装するのは人手がいくらあっても足りなくなるそこで C UIとして用いているツールをGUI 化することが汎用的な環境定義を行うことにより利用できるようになると色々な過去のツールが使いやすくなる可能性がでてくるこのようにツールを汎用化させるためには外部定義により色々な条件を入力しこれを解釈してその定義に応じてツールの機能がインタープリティブに変化するようにできればよいこのための外部定義は XMLでの記述形式を用いると人が見て理解しやすい構造で定義体を記述できるこのように現在のツールを改造すると概ね図 6のような形態になるこのときに定義体に必要な機能的な内容は表 1に示したような項目が考えられる XML での定義統合環境制御エディタバッチ起動結果表示コード実行結果モニター表示実線の矢印 : 制御の関係図 6 汎用化した統合ツールのイメージ -70-

6 表 1 定義体に必要な機能 No 機能 1 画面のタイトル 2 メニューの種類 3 エディタの有無 4 バッチファイルの指示 5 入力情報の指示 6 出力情報の指示 7 排他制御の必要なプロセスの指示 8 並列処理が可能なプロセスの指示 9 シリアライズが必要なプロセスの指示 10 エラーへの対処 5. まとめこのツールを利用して 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 原則 about_ud/udprinciples.htm -71-

C#の基本

C#の基本 C# の基本 ~ 開発環境の使い方 ~ C# とはプログラミング言語のひとつであり C C++ Java 等に並ぶ代表的な言語の一つである容易に GUI( グラフィックやボタンとの連携ができる ) プログラミングが可能であるメモリ管理等の煩雑な操作が必要なく比較的初心者向きの言語である C# の利点 C C++ に比べてメモリ管理が必要ない GUIが作りやすい Javaに比べてコードの制限が少ない