.


ソフトウェアの問題を解く
張 漢明




張 漢明 ちょう・かんめい 

数理情報学部助教授、情報通信学科。
専攻分野はソフトウェア工学。  長期研究テーマは「形式手法に基いたソフトウェア開発支援環境」。  短期研究テーマは「形式手法に基いた組込みシステム開発手法」。  担当科目は『プログラミング数学』など。


 私は大学を辛うじて卒業して、コンピュータのソフトウェアの会社に就職しました。大学での専攻は機械工学でしたが、そもそも機械工学とはどのようなものかも知らずに入学した私は、機械の図面を書いたり、エンジンを設計したりすることに全く興味をおぼえず遊び惚けていました。そんな中で、唯一面白いと思ったのはコンピュータのプログラミングでした。自分の書いたプログラムが、コンピュータ上で思い通りに動作したときの喜びは今でも忘れられません。そのようなわけで、就職先はコンピュータ関係の会社と心に決めていました。機械関係の勉強をおろそかにした私が、何とか卒業単位を取得するまでにはいろいろ面白い話があるのですが、それはまた別の機会にしたいと思います。
 就職先のソフトウェアの会社では、銀行のATMの開発部署に配属されました。私が初めて担当した仕事は、ATMの制御の中で、ある動作をやめるようにプログラムを修正することでした。このプログラムの修正は、プログラム中のある一行を削除するだけだったのですが、大変な労力を必要としました。修正にあたっての文書の整備や、テストの手順書作成とテストの実行、さらに、品質管理部門の検査などがありました。ATMは銀行システムの一部で、ATMのプログラムの誤りは甚大な被害を与える可能性があるので、プログラムの品質には厳しいものが求められていました。私は、プログラムを開発する仕事の難しさと、その社会的責任の重さを感じるとともに、自分のプログラムが社会システムの一端を担うことを誇りに思いました。
 学生時代に趣味でプログラムを作ることと、会社で仕事としてプログラムを開発することは全く違います。仕事としてのプログラム開発では、大規模で高い信頼性が求められるシステムを複数の人数で開発します。システムに求められる機能がコンピュータ上で実現されることはもちろんですが、思いがけない動作にも十分対処できなければなりません。自分の書いたプログラムは他の人がその保守をするかも知れないので、誰が見ても分かり易いものでなければなりません。また、将来のシステムの変更を想定して、機能拡張に柔軟に対応できるようにする必要があります。信頼性の高いソフトウェアを効率よく開発するための技術や方法論を追求する学問を「ソフトウェア工学」と呼びます。
 水道、ガス、電気などと同様に、コンピュータと通信ネットワークは日常生活に必要な社会基盤として認識され、整備されつつあります。コンピュータが安価で性能も向上し、また、ネットワーク接続がいつでもどこでもできるようになり、ハードウェア技術の発展は目覚しいものがあります。しかし、普段使っているコンピュータが突然フリーズしたり、銀行のオンラインシステムが停止したりするのは、実はソフトウェアの開発技術がハードウェアの進歩に追いつかず未成熟の分野だからです。もちろん、ソフトウェアの開発をいいかげんにやっているわけではありませんが、ソフトウェア開発は個人の能力に依存した職人技の域にあるのが現状です。ソフトウェア工学の研究を発展させて、ソフトウェア開発を「工藝」から「工学」の域に高めなければなりません。
 ところで、私の会社での話に戻すと、プログラム開発の経験を積むにつれて、自分にソフトウェアに関する基礎的な素養が足りないことに気づき始めました。そこで、奮起一番、会社を辞めて大学院で勉強し直すことにしました。今から考えれば無謀な行動だったのですが、幸運にも大学院に進学することができました。ここで出会ったのが現在の私の研究分野である「形式手法」です。  形式手法とは、数学の考えに基づいたソフトウェア開発における技術のことです。形式手法にもいろいろな分野があるのですが、指導教官から私に与えられた研究テーマは、ソフトウェアの仕様を数学の論理記号等で表現する「形式仕様言語」というものでした。研究を始めた当初は、こんなものは実際の開発現場では役に立たないなと、高を括っていました。ところが、勉強を進めていたある日突然、「これはすごい!」と形式手法の熱狂的な信者となってしまいました。形式手法こそソフトウェア開発の実際の現場に必要な技術だと言い出す始末です。この時の直観を信じて、今現在も形式手法の研究を続けています。
 ソフトウェア開発の難しさは、ソフトウェアが実際に目に見えるものではなくて、人間の思考をコンピュータ上に具現化する作業にあります。ソフトウェア開発は、物事を抽象的に捉えて形式(記号)化し論理的に解く作業です。数学の概念はこのような作業の支援に大変役立ちます。中学や高校での数学の文章題を解くことを考えてください。文章を読んで内容を理解して、方程式をたて解を求めます。方程式をたてること、つまり問題を解ける形で形式化できれば問題は解けたも同然です。ここで大事なことは、与えられた問題を形式化する能力と、形式化された問題に対する知識です。形式化するだけではだめで、形式化されたものが解ける問題かどうかを判断する能力が重要です。解けない問題を解こうとする行為はばかげています。問題の対象が解けないことを知ることもとても大切です。
 このように問題を系統的に解く姿勢はエンジニアの分野では当たり前ですが、ソフトウェアの世界では、問題を系統的に解く方法がまだ見つかっていません。系統的な方法を見出すためには、基礎理論の研究と実際のソフトウェア開発の事例の蓄積が必要です。私の研究は、形式手法のアプローチで対象の問題をモデル化して問題の特性を明らかにし、その解法を提示することです。現実の問題を一つひとつ地道に解いて問題を分析し、そのモデルを提示していくことが私の仕事です。私の所属する数理情報学部は、ソフトウェアの専門家と数学の専門家が同居する、私の研究にとって最適な環境です。