目のつけどころが"ソフト"でしょ　開発プロセス考17　――たしかめること

　「正しい」プログラムを作ることが，ソフトウェアの世界ではつねに課題です．しかし，「正しい」とは何か？

　一般的には，仕様をプログラムが満足しているか否かという基準で，正しさが与えられます．このことをソフトウェアの世界では「検証（verification）」と呼んでいます．

　検証は実世界では「テスト」という手段をとって疑似的に行われます．疑似的というのは，次のDijkstraのことばを指しています．「テストによってバグの存在を示すことはできる．しかし，バグが存在しないことを示すには絶望的に不十分である」．テストは決して正しさを示す確実な方法ではありません．与えたテスト・ベクトルについて期待した結果が得られたことを示すのみで，多くの場合，それは想定する入力ベクトルのほんの一部にすぎません．

　ではどうしているかというと，それでもテストで代用します．しかし，実用という点に少しだけ目をつぶるならば，「プログラム検証」という確実な手法があります．

●プログラム検証とは？

　この世界では，検証の定義は以下のように明確に与えられます．
プログラムPがPL（プログラミング言語）によって与えられている．仕様φがSL（仕様記述言語）によって与えられている．このとき，Pがφを満足することを示すこと．言い換えれば，φに関するPの正当性を示すこと．

　図1において，プログラムPはラベルL0の状態からスタートして，Lhで停止することを考えます．αは一つのプログラムの状態変化のパスを表しています．

　ラベルL0では文pが，ラベルLhでは文qが真であるとします．pは入力仕様であり，qは出力仕様になります．あるいは，事前条件，事後条件とも呼びます．これらはまとめて「表明」と呼ぶこともあります．今考えている仕様φは，<p,q> として与えられます．プログラムとは，ある入力仕様と出力仕様が与えられたときに，それを満足する計算になります．これを，次のように表現します．

　　　｛p｝C｛q｝

［図1］　プログラムP

　当然のことながらプログラムC は，いつか停止しなくてはなりません．また，途中でエラーによって事後条件を満足する前に停止してはいけません．

　例えば，整数だけで平方根を計算するプログラムの「表明」は次のように記述できます．

　　　事前条件　{p} : x ≧ 0，
　　　事後条件　{q} : y*y ≦ x ＜（y+1）*（y+1）

　今，Cをリスト1のように考えます．変数a，bを導入して，最初の状態でy:=0，a:=1，b:=1とします（:=は代入の記号）．実際に値を入れて考えてみます．今，xを5として計算します．

　　　（x, y, a, b）：（5, 0, 1, 1）→（5, 1, 4, 3）→（5, 2, 9, 5）

　この例を見てわかるとおり，b＝2*y＋1で，a＝（y＋1）*（y＋1）になります．また，ループ中は，y*y≦xなので，事後条件を満足していることがわかります．また，x－a＋bは，x－（y*y＋2*y＋1）＋2*y＋1＝x－y*yで正であり，事後条件を満足します．x＜aで事後条件を満足しなくなりますから，停止します．したがって，停止することも保証されています．

●良いプログラムを作るうえで，「表明」の考えかたは重要

　ここまでに書いた方法は，FloydやHoareによる「表明」を用いた証明の方法になります．ソフトウェア工学の黎明期から30年以上の歴史を持ち，その後，さまざまな証明方法が発達してきました．しかし，ここでの考えかたは，70年代の，すなわち今のプログラマが利用しているプログラミング言語に大きな影響を与えており，今わたしたちはその成果の一部を利用しています．

　ソフトウェアは，機構設計などと異なり物理的な影響を受けないため，ほかの世界の「検証」とは異なっているかもしれません．文字一つ打ちまちがえただけで，致命的なエラーを生じる可能性があるという点においてです．しかし，一方で入力と出力が明確に定義できるならば，（物理現象の影響を受けずに）正しいプログラムを作れる可能性があるともいえます．そこまでいかなくても，このようなアプローチを考えることは，自分たちのしごとを振り返り，より良いプログラムを作るうえで，重要と考えています．

(本コラムはDESIGN WAVE MAGAZINE 2003年2月号に掲載されました)

◆筆者プロフィール◆
伊藤昌夫（いとう・まさお）．自動車会社，航空機関連会社のソフトウェア・エンジニアを経て，ニルソフトウェアを設立．ソフトウェア・プロセスおよび開発環境が専門で，そのためのコンサルテーションおよびツールの提供を行っている．設計における人間の認知活動に興味を持っている．