このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ソフトウェアにとって大事なこと: 正しさが判断できること

良いソフトウェアとは何か? という基準は人によって違うでしょう。機能が豊富、使いやすい、値段が安い、などの条件がありますよね。僕の関心と価値観から言うと、「正しさが判断できる」ことを重視します。良いソフトウェアの基準というよりは、むしろ、「これを満たさないとダメだよ」という基準なのですが、クリアするのは容易ではありません。

内容:

正しさが判断できるとは

正しいソフトウェアを作りたいと切望するのですが、そうはいってもソフトウェアは人間が作るもの、人間は間違うのでなかなか正しいソフトウェアは作れません。それは致し方ないことだと思っています。つまり、ソフトウェアはたいてい正しくないのです。できるだけ正しくしようという努力が続くだけです。しかし、もし正しさが判断できないなら、「より正しくしよう」という目標もスローガンも無意味となります。

「正しさが判断できる」とは、「正しくないこと=間違い」を検出・指摘できるということです。ですから、ちょっとくどい言い回しを使うなら、「正しいのか/正しくないのかを判断できる」となります。

ソフトウェアシステムを非常に大ざっぱに描写すれば、入力に対して処理をして結果を出力する仕掛けです。入力をx、処理をf、出力をyとすれば、y = f(x) という関数形式で書けるでしょう。この描写はあまりにも大ざっぱ過ぎると思うでしょうが、そうでもないのです。

僕が、y = f(x) と書いたからといって、fが純関数を意味するとは限りません。不純な計算が大好きな僕がそんなこと思うわけないです。状態遷移系を考えるとして、その状態空間をSとすれば、遷移は S→S という写像として定式化されます。遷移のキッカケとなる入力(ラベル、アクション、メッセージなどとも呼ぶ)の集合をMとすれば、S×M→S です。状態空間として、レジスタ、メモリ、諸々の外部ストレージなどすべてを考慮すれば、いかに不純な計算でも f:S×M→S という関数(写像)とみなせます。

という次第で、ソフトウェアシステムの挙動を、象徴的に y = f(x) と書くのは見当違いではないのです。

さて、「正しさが判断できる」の話題に戻り、「正しさ」やら「判断」やらの言葉をもう少し詮索します。いま、システムへの入力として具体値aが与えられたとして、そのaに対してシステムが正しく動くとはどういうことでしょう? それは、期待する出力bが得られることです。つまり、b = f(a) となることです。

それでは、「期待する出力b」とは何でしょう? この値bは、当該ソフトウェアシステムを動かした結果ではありません。あくまでも「期待する」のです。「期待する」とは「そうあるべき」と想定することであり、これが正しさの基準を与えます。実際に動かしてみて、「出力はbでした」と報告するのは正しさに関しては何の判断もしていません。実際に動かす前に、期待する出力/そうあるべき出力を特定できる必要があるのです。

もし、与えられたaに対して期待する出力/そうあるべき出力bを誰も特定できないとしたら、そのシステムは正しさの判断ができない状態になっています。「動かしてみないと、どうなるか分からない」状態ですね。このようなシステムでは、テストやデバッグという行為もナンセンスです。だってそうでしょう; 「正しいのか/正しくないのかを判断できる」からこそ、「テスト通りました、OKです」とか「これはバグですね、直しましょう」とかの発言に意味があるのです。

挙動の予測可能性

入力がaのとき、実行をしなくても「出力がbであるべき」と言えるのは、入力と出力のあいだに何らかの因果関係、法則性があるからです。法則があるからこそ、その法則に基づいて最終結果や結果に至るまでの過程を予測(あるいは期待)できるのです。正しさを判断する材料として、システムの挙動を制約する法則が必要です。その法則は、人間か別なソフトウェア(検証系)が理解できるものでなくてはなりません。

システムの挙動を制約する法則は、個別の入力群に対する出力群の列挙である必要はありません。もし、全ての入力値に対する出力値が事前にわかっているなら、ソフトウェアシステムがやること無いですもんね。法則というものは、個別事例の集積ではなくて、それらを包括的に記述できる、より抽象度の高い記述を持つものです。

法則の記述の具体例として、ホーア式メイヤーの契約があります。値のあいだの個別の関係 b = f(a) という形ではなくて、入力の範囲となる集合Aと出力の範囲となる集合Bが与えられます。そして、「x∈A ならば f(x)∈B」という論理的主張によって法則が記述されます。もちろん、法則の記述は複数の論理的主張(表明)を使ってもかまいません。番号1, 2, ... に対する「x∈A1 ならば f(x)∈B1」、「x∈A2 ならば f(x)∈B2」、… のような形です。

具体的に与えられた入力値aを見て、例えば a∈A2 であるなら、出力に関して f(a)∈B2 と期待できます。ここでいう期待は心情的で曖昧なものではなくて、法則に基づいた事前の判断、つまり予測のことです。ときに、最終結果だけではなくて、中間の過程までも予測できるかもしれません。

一言でいえば、正しさが判断できるためには、「システムの挙動が予測可能でなくてはならない」のです。その予測の根拠には法則があり、法則は論理的主張として記述されるべきです(値の列挙も悪くはないです、併用します)。

事前状況の制御可能性

今まで「入力が与えられたら」とか「入力がaのとき」のような言い方をしました。好きな値を入力に選べることを暗黙に仮定してます。しかし、入力とはいっても純関数に渡す引数のようなものとは限らず、巨大な状態遷移系の事前状態と、遷移をトリガーするメッセージかもしれません。ですから、入力よりは事前状況とでも呼ぶほうがふさわしいでしょう。

システムの挙動が予測可能であり、「入力がaのとき、出力はbのはず」と断言できても、そのa(事前状況)がユーザー数、ネットワークの混み具合、データベースに蓄えられた(膨大かもしれない)データ、実行時刻などから構成されていたら、aをセットアップするのは容易ではありません。入力値=事前状況を任意の値に調整するのは事実上不可能かもしれません。

もし、入力値aが準備できないなら、「入力がaのとき、出力はbのはず」という予測を確認することはできません。法則とそれに基づく予測があっても実証はできないのです。実証できないなら、正しいも正しくないも言えません。

どうしたらいいでしょうか? 選択肢はあまりないように思えます。

  1. 実証のための環境内で、任意の事前状況をセットアップ可能とする。
  2. 実証済みの事実から、実証できない結果を推論可能にする。

二番目の方法では、結局は実証はされません。実証のための事前状況がセットアップできないのです。しかし、例えば、システムが実証可能なサブシステム達から構成され、全体の構成法が明確であり、信頼に値する推論ができるなら、推論をもって実証に代えることも許容されると思います。

一番目の「任意の事前状況をセットアップ可能とする」がベターであるのはもちろんで、稼働環境の仮想化とかメタ巡回的構造とかにより、テスト環境で何でも再現できるのが理想です。

事後状況の観測可能性

システムの挙動が予測可能であり、しかも入力値=事前状況も制御可能で、「入力がaのとき、出力はbのはず」と言えたとします。入力値=事前状況もセットアップできます。これなら、実証を遂行できるでしょうか? まだ、出力値=事後状況の確認が残っています。

「出力値はbである」とか「出力値は集合Bに含まれる」とか判断するためには、出力値=事後状況を観測可能でなくてはなりません。システムが動作した結果をくまなく調べて、期待通りか確認できなくてはなりません。この確認には、変化した部分だけではなくて、変化してないことの確認作業も含まれます。

「副作用」という言葉が「悪いもの」という文脈で使われることがあります。「悪いもの」として扱われる副作用は、いつ/どこで/なにが起こるか分からないものです。副作用の結果が観測にかかりにくいのですね。明白に観測可能なら、それは主作用といってもよく、嫌う理由はありません。

観測にかからない出力は、最初からシステムの挙動を統制する法則に記述されてないケースがあります。実際には、観測にかからない出力もシステムの挙動に影響を与えます(与えないならまーいいのですが)。その影響がシステムの法則性として考慮されてないなら、その法則は役立たずになります。見えない謎の効果により、法則が乱されるのですからアテになりません。予測も検証も信頼できません。

まとめ

ソフトウェアシステムの正しさが判断できるためには、(理想論としては)次が必要です。

  1. システムの挙動を制約する法則が記述されており、その法則に基づいて挙動を予測することができる。
  2. 処理の入力値=事前状況が制御可能であり、任意の状況にセットアップできる。
  3. 処理の出力値=事後状況が観測可能であり、比較や計測が完全に行える。

これらのことは理想論であると同時に、ものすごく当たり前のことです。理想を追うのは悪いことではなく、当たり前のことをしないのは悪いことです。どうすべきかを具体的に示すことは僕にはできません。が、どこに向かうべきかは明らかだと思えます。