Mizar用統合環境の開発を応用した簡易汎用統合環境の提案
A model of simple general-purpose Integrated Development Environment(IDE)that came out of development of IDE for proof checker Mizar
福良 博史 FUKURA Hirofumi １．緒言 教育用のプルーフチェッカMizar-MSE用の 統合開発環境の制作を行い、その内容を2009 年に紹介(1)した。このツールは、学生の記号論 理教育に用いている。このツールが安定して使 えているのでそのノウハウを基に、プロのため のプルーフチェッカとして世界で利用されて いるMizar(2)の統合開発環境を提案(3)し、現在 その試作を行っている。 これらのツールを制作する動機は、本来のツ ールがCUI環境での提供のみとなっていたた め、コンピュータの素人にとって、熟練した指 導者が近くにいないと導入が難しい。このため、 GUI化し、より親しみやすい環境を提供するこ とを目指した。 このツールづくりを通して、CUI環境のみを サービスしているソフトウェア・ツール自身の 内部に手を加えずに改造する、つまり外側から オプラードで包む方式により、GUI化を行うた めの道筋が見えてきた。そこで、今後色々なツ ールをGUI化するための方法の一提案を行う。 ２．Mizar 用統合開発環境の基本的な機能 Mizarを利用するパソコンの環境は、基本 的 に は イ ン タ ー ネ ッ ト に つ な が っ て い な い 環境（オフライン環境）において利用できる ことが望ましいと考えている。これは、イン タ ー ネ ッ ト に ト ラ ブ ル が 生 じ て も こ の ツ ー ル の 利 用 が 停 止 し な い よ う に す る こ と が 望 ましい。このためにこのツールを利用する状 況は、インターネットとは切り離して利用で きるように機能を整理し、機能の確認を行う。 ２．１ Mizar の利用者がとる主な行動 Mizar を利用するためには、パソコンが必要 となる。オペレーティング・システムは、Linux かWindows 環境が必要となる。Mizar だけを 利用するためには、テキスト・エディタがあれ ばその他には特にソフトは必要ではない。しか し、Mizar を利用して証明を記述するためには これだけの環境で済ませることには無理があ る。その主な内容を以下に説明する。 Mizar を用いて自分のアーティクル（自分の 論文の理論）を作成するためには、過去に蓄積 された既存の1000 を超えるアーティクルが保 存されているライブラリを検索しなければな らない。このためには検索ツールが必要になる。 ある定理の意味を調べて理解するためにも検 索ツールの利用が基本となる。この理解の助け となるMizar の既存のアーティクルを HTML 形式にしたものが用意されている。このHTML 形式で用意されているものは、各々の定義・定 理の中に記述されている個々の単語をその元 になる他のアーティクルの中の該当の定義・定 理にリンクを張り、検索・閲覧を迅速・確実に 行えるように配慮されている。このためHTML でできているツールは欠かせないと考える。し かしこれは現在オンラインでのみ提供されて いる。このためインターネットにトラブルが生 じると利用できなくなる。Mizar をどのように 記述していけばよいのかについての学習を含 めたチュートリアル等も欠かせない情報源と なっている。 Mizar システムはコマンド形式で各種ツー ルを提供している。これらのツールをどのよう に利用するのかが初心者には理解しにくい。ま ず証明の妥当性の検査を行うツール（mizf.bat というバッチファイル）は必須となる。しかし
未投稿であったり、投稿しても未だ受理されて いないライブラリを使いたい場合、自分のパソ コンにそのライブラリを仮に登録しておきた くなる。この操作を行うためのツールが用意さ れている。このツールを用いて環境を整えてか ら自分のアーティクルを検査しなければなら ない。そして自分のアーティクルが完成したあ とそれを投稿するためには、事前にその証明の Mizar 記述のコードを整形し、無駄な記述の整 理を行うことが要求されている。このためのツ ールが数種類用意されている。これらのツール を用いるときにツールによってアーティクル のファイル名の拡張子が必要であったり不要 であったりする。これらの操作には初心者でな くても戸惑う場合がある。 ２．２ 必要な機能の整理 以上の検討において顕在化した部分を機能 として取り入れるとすると、以下のような機能 が必要になると考える。 （１）基本機能 ・ 開発支援ツールをGUI 化すること ・ オペレーティング・システムの依存度を 下げること （２）アーティクル作成・検証機能 ・ 自分のアーティクル・ファイルの参照・ 更新・テキスト編集 ・ 自分のアーティクルの検証とアーティ クルの仮登録 ・ アーティクル投稿の事前整形 （３）調査・検索機能 ・ アーティクルの HTML リンク形式によ る調査・検索 ・ アーティクルおよびアブストラクトの テキスト検索 ・ 各種チュートリアルの閲覧 以上のうち、（３）の機能は、インターネッ ト上には既に備わっている。しかし、これを オフライン環境に取込むことが望ましい。 ２．３ ツールの構成 2.2 で述べた機能を網羅するためのツールの 構成はどのように考えるのが良いのか。 基本機能として GUI 化は必須と考える。オ ペ レ ー テ ィ ン グ ・ シ ス テ ム は 取 り 敢 え ず Windows のみとする。ツール自身は Java にて 作成することとする。Mizar-MSE 用のツール もJava で制作した。こうすることで GUI 化ツ ールの開発も以前のノウハウを利用できる。ま たJava を利用することで移植性が良いと考え る。テキスト・エディタは各自が利用している ものがそのまま使えれば良い。このためには任 意のエディタが指定できるようなインターフ ェースが好ましい。そこで外部のツールを動か すためにはバッチファイル化し、この中身のス クリプトを変更すればよい、という柔軟さを取 り入れた。汎用のXML 形式によるパラメータ 化は、取り敢えず今回は考慮しないこととした。 HTML 形式の情報の取り扱いはどうするのが 良いか。裏で Apache をつないでローカルな HTTP サーバを構築することが好ましいと考 えるが、開発が大掛かりになりすぎる。今回は 小さな HTTP サーバを作成し動かすことを考 えてみた。HTTP で作成された Mizar アーテ ィクルその他のドキュメント類はダウンロー ドし、内部に取り込むこととした。この場合の 著作権の問題が多少気になるが、基本的には非 営利ならば問題ないと考えている。しかしツー ルを公開するとなると明確にしておく必要が ある。HTTP を閲覧するためのブラウザは、 個々のパソコンに備わっているブラウザを利 用することとした。これもバッチファイルに必 要なスクリプトを入れておき、それを起動する ことで対応できるように考えた。デフォルトで はWindows の場合 Internet Explorer を起動 するためのサンプルをあらかじめ作成してお く。しかしバージョン更新時に多少の修正を余 儀なくされる場合のことも考えておく必要が ある。これを避けるためにはブラウザも自前で 用意することを考えなくてはならないかもし れない。Mizar アーティクルとアブストラクト の検索機能は内部に構築しておく。
３．Mizar 用統合開発環境（IDE）の例 以下では、Mizar 開発支援の GUI ツールの 画面例を紹介する。これらの動作は未だ完成し たものではないが、基本的な機能とソフトウェ アの構成に大幅な変更は無いと考えている。 （１）統合開発環境の立ち上げ ツールを立ち上げた初期状態の画面（図1） で、アーティクル作成時の主なブロックを、雛 形として表示している。 図1 MizarIDE の初期画面 （２）テキスト・ファイルの選択 ファイル・メニュー（図2）から既存のファ イルを修正するのか、または新規作成するのか を選択する。そして編集が終わると保存する。 保存は上書きかまたは別の名前で保存する。 図2 MizarIDE のファイル・メニュー （３）外部エディタへの引き渡し ファイル・メニューで選択したテキスト・フ ァイルのファイル名を記憶しておき、外部エデ ィタに引き渡せるようにする。（図3） 図3 MizarIDE の 外部エディタ呼び出しメニュー （４）プルーフチェッカの起動 作成したアーティクルに記述されている定 義・定理の証明の正しさをプルーフチェッカ・ メニュー（図4）の MizarVerify（mizf.bat を 裏で起動）により検証することができる。 図4 MizarIDE の プルーフチェッカ・メニュー Make abs を用いると、アーティクルのア ブストラクトである拡張子が“.abs”のファイ ルを生成する。Make prel を用いると、公開 されていないアーティクルを自分の開発環境 の中に仮登録し参照できるようになる。
（５）投稿前の整形 作成したアーティクルのVerify が済んだ後、 投稿するためには、コードの整形が要求されて いる。このためのツール群の選択メニュー（図 ５）を示す。relprem から irrths までが、整 形用ツール群を示す。errflag は、エラー情報 をアーティクルのソースコード内部に埋め込 んでくれるので、エラー情報を、ソースコード に埋め込まれたものを読み取ることができる ので、エラーの判別が容易になる。 図５ Mizar 投稿前の 整形用ツール群の選択メニュー （６）フォントの種類 このツール自身でコードを編集する場合、フ ォントを 3 種類選択（図６）できる。大きい フォントはプレゼンなどの時の説明用と考え ている。 図６ Mizar テキストの フォント選択メニュー （７）各種ドキュメントの閲覧とアーティクル 等の検索 各種ドキュメントの閲覧とアーティクルの 検索用メニュー（図７）を示す。 図７ チュートリアル等の閲覧および アーティクル等の検索選択メニュー この中のBrowser を選択すると、現在、図 ８に示す画面が表示される。ブラウザが参照す る HTTP のルートは、ドライブのルートに proofchecker フォルダを用意し、その子供と してmizerDoc というフォルダを創り、このフ ォルダをHTTP のルートとしている。 図８ チュートリアル等の閲覧画面 （８）その他 ヘルプメニューは、このツールのメニューの 説明などを表示する。
４．Mizar 用ツールの構成イメージ Mizar 統合開発環境のソフトウェア構成イ メージは、図９の通り。フォルダの構成はツー ル を 格 納 す る ド ラ イ ブ の ル ー ト か ら proofchecker フォルダを創り、その子供のフ ォルダ mizarTool にこの統合開発環境のプロ グラム群を格納し、mizarDoc に HTML 群な どの閲覧用情報群を格納する。 ５．今後の課題 Mizar 用の統合開発環境の GUI ツールは、未 だ完成はしていないがほぼ出来上がった。今後 の主な課題は以下の通り。 （１） HTTP のサーバとクライアント サーバについては、Apache のような高度な 機能を採用しないとコンテンツのバリエーショ ンに耐えられない。コンテンツに html 以外の ファイルを一切含まないようにできれば現状の ままの小さなHTTP サーバでも耐えられる。現 在、サーバを立ち上げない形式でも取敢えず利 用できている。自分でサーバを立ち上げている 場合の競合などを考えると各種の条件を考えな いとブラウザ利用の形態は意外な問題が出てく るかも知れない。この場合、ポート番号をロー カルな番号にしておくのが最良の選択と考える。 クライアントは既存の各自が利用しているブラ ウザを利用することで問題は無いと思われるが、 これも専用のツールを用いた方が良いかもしれ ない。 （２） パラメータのXML 化 ツールの環境定義などの定義情報は XML 化が最近の流れのように思える。ここでは当面 バッチファイルでのスクリプトのまま利用す る。今後、操作性を考慮するとXML 化も視野 に入れておく必要があると思われる。 （３） Linux 版への対応 とりあえず使い勝手を確認した後、必要性が 高ければ考慮することとし、今は考えない。 （４） 実際に利用しての評価を行う 今後、ツールを整備し Mizar の利用者に使 ってもらい評価していくこととしたい。 （５） 著作権の問題 今後、ツールを公開する場合、各種閲覧ドキ ュメントの著作権が問題となるかもしれない。 この問題が生じるおそれのあるコンテンツは、 図８の中のオフラインで示した内容に限定さ れる。オンラインで示したツールは、リンクを 張っているだけのため直接問題は生じないと 考える。著作権の問題が解決しない場合は、イ ンターネットからの独立性は、犠牲にせざるを 得なくなると考える。 ６．おわりに 以上は、CUI インターフェースのツール を GUI インターフェースのツールに改造 統合開発環境制御 エディタ 外部ツールの起動 ファイル名保存 Miz ファイル更新 コマンドプロンプト モニター表示 各種バッチ起動 実線の矢印：制御の関係 破線の矢印：情報の流れ バッチファイル群 図９ ツール主な構成
した２例目となる。このオプラードで包 み込むような構造のツール構成による使 い勝手の向上を図ることは、からり簡便 にできる、ということが見えてきた。こ の MizarIDE 用ソースコードは、改造した り、違うツールに応用したりできるよう に、ウェブ上で公開(4)している。プログ ラミングの素養があれば、上記のソース を改造して自分が使っているツールを GUI 化することは 1 日か 2 日くらいで使え るものが完成すると考える。 今後は既存の CUI ベースのツールを、 GUI 化するためのより簡単な、軽く、ソフ トウェアのプログラミングの知識がない 人にも汎用的に、誰もが簡便に GUI 化で きるようなソフトウェアに整備していき たい。 参考文献 (1) 福良博史：“形式論理のための教育訓練ツー ル（Mizar-MSE）のユーザインターフェー ス向上”、職業能力開発研究、Vol.27(2009)、 pp.55～67 (2) Mizar についての情報： http://mizar.web.fc2.com/null/indexse.html (3) 福良博史：“Mizar のための統合環境の提 案”、日本Mizar 学会、2009 秋季大会 (4) ソースコード公開の URL： http://mizar.web.fc2.com/null/ study/vingtetuncruise/index.html
