-
利用者の手間のかけ具合に応じて2種類のプログラム検証[1]手法を混合して使う『漸進的検証』を提唱
-
既存の静的検証手法から漸進的検証手法を構成する枠組みを考案
-
C風のプログラミング言語に対する漸進的検証手法を実際に構成
このgistは(大人版)今年読んだ一番好きな論文2018 Advent Calendarの1日目の記事です。
といっても、年明けてから大幅に書き換えており、現在の記事はアドベントカレンダー当日のものとは別物ですのでご了承ください。
趣味で多少論文を読むことがある程度の新社会人のお話なので大人版としては専門性控えめかもしれませんが、少々お付き合いいただければ幸いです。
- タイトル
- 著者
-
Johannes Bader, Jonathan Aldrich, Éric Tanter
- 出典
第一著者の修論が同じような内容の硏究で、この論文はその後に対象のプログラミング言語や基盤となる検証手法を変えて適用してみたもののようです。
プログラムからバグを発見することの重要性と難しさについては説明するまでもないかと思います。
バグを防止するために、多くのソフトウェア開発ではソフトウェアテストという手法で検証しています。これは本質的には「決まった操作(入力)で動かしてみて、期待通りの動作(出力)をするか見る」というシンプルなものです。[2]
また、プログラムを実行せずに解析してありがちな問題[3]を発見する手法も併せて使われることがあります。
極端な例ですが、人工衛星のプログラムを作る時に、「動作確認のために何回か飛ばしてみましょう」なんてやってられませんよね。[4]
プログラムの検証手法は他にも色々あるのですが、上のようにプログラムを実行する検証と、実行しない検証の2つに大別されます。ここでは論文に倣って前者を 動的検証 、後者を 静的検証 と呼びます。[5]
ざっくり言うと、以下のように長短があります。
- 動的検証
-
動かすだけなので、やろうと思えばツールを一切使わなくてもできる(とはいえ普通は何かしら使う)。入力が1〜100の時に問題が起こらないことは100回テストすればわかるが、101を入力した時に問題が起こらないとは限らない。
- 静的検証
-
どんな問題を見つけたいのか等によって多様なツールと設定項目が存在し、比較的使うのが難しい。問題を見逃してしまったり、正しいコードを問題として報告してしまうことがある。[6]
今回は、 別々に用いられている動的検証と静的検証を、協働するように一つの手法にまとめてしまおう というお話です。
とりあえず前提知識として大事な概念が2つあるので、それを確認しておきましょう。
ソフトウェアを検証するためには、そのソフトウェアがどう動くべきか(仕様)を検証ツールに伝える必要があります。
ソフトウェアテストでは入出力のペアによって表しますが、別の方法として 契約 というものがあります。
契約はソフトウェアを構成する関数に対して記述するもので、 事前条件 と 事後条件 の2種類があります。前者はその関数が 呼び出される時 に満たすべき条件を、後者はその関数が 終了する時 に満たすべき条件を示しています。
言い換えれば、 呼び出す側 が呼び出す関数の事前条件を守る限り、 呼ばれる側 は自分の事後条件を守らなければなりません。このように、契約には責任の所在を明らかにするという効果もあります。
例えば、ATMからお金を引き出す処理で、「引き出す額が預金残高以下である」という事前条件と、「引き出した後の残高がマイナスにならない」という事後条件を考えましょう。
これを今回は以下のように書きます。処理は思いっきり簡素化しています。なお、 result は返り値を表すキーワードです。
// 残高と引出額を引数にとって引き出し後の残高を返す関数
int withdraw(int balance, int amount)
requries (balance ≧ amount) // 事前条件
ensures (result ≧ 0) // 事後条件
{
return balance - amount;
}
さて、今回は「引き出した後の残高がマイナスにならない」という事後条件を考えましたが、「残高が減っている」とか「ちゃんと引き出した分だけ減っている」といった事後条件が思い浮かんだ方もいるかもしれません。
この辺りはこの硏究の重要な論点なので、後で改めて見てみましょう。
話はソフトウェア検証から逸れてしまいますが、動的/静的と言う話で最近熱いのが漸進的型付けです。
ここでは、動的型付けと静的型付けをうまく組み合わせた型付けとだけ理解してもらえればいいですが、一応少しだけ説明しましょう。
漸進的型付けは、ユーザが何もしなければ動的型付けとして振る舞います。しかし、動的型付けは実行してみないと型エラーの有無が確認できない上、プログラム実行時に型検査処理が入るため、プログラムが遅くなります。
一方、静的型付けでは変数に対して型を指定することで、実行前に型検査が可能です。ただ、型を指定する(型注釈を入れる)ことが面倒だったり、プログラムの自由度が下がってしまうことがあります。
漸進的型付けでは 一部の変数のみに 型を指定することができ、その部分だけを静的に検査します。最初はプログラムだけ書いておいて、後から少しずつ、つまり 漸進的に 型を指定していく、と言うのが漸進的型付けです。
今回はこのアイディアを検証に応用していく[8]ことが主題となります。
さて、いよいよ論文の内容に入っていきます。まずは普通の契約の検証について考えてみましょう。
先ほどの withdraw 関数を使って、以下のようなC風のプログラムを考えます。
// 再掲
int withdraw(int balance, int amount)
requries (balance ≧ amount) // 事前条件
ensures (result ≧ 0) // 事後条件
{
return balance - amount;
}
// 以下がmain関数相当
int balance := 100;
balance := withdraw(balance, 30);
balance := withdraw(balance, 40);
このプログラムでは withdraw 関数を2回使っています。この程度のプログラムなら検証するまでもないですが、実際には withdraw がめちゃくちゃ複雑な処理を行なっていると思ってください。
さて、このプログラムは明らかに問題ないため動的検証は成功しますが、実は静的検証は2回目の withdraw 呼び出しで違反の可能性を検出します。なぜなら、この時の balance は1回目の呼び出し結果であり、withdraw の事後条件である balance ≧ 0 以上のことは考慮してくれないため、2回目の事前条件 balance ≧ 40 が保証できないのです。
鋭い読者の皆様は、もしかしたらツッコミたいかもしれないので、以下に2つほど予防線を張っておきます。ただし、論文に書いてあったものではなく個人的な意見なので、間違っていたらご容赦を。
withdrawの定義を見ればbalanceが70になるのがわかるのでは？-
その通りですが、それはつまり、契約にないことまで暗に要求しているブラック雇用主になってしまうということです。
契約には、(お互いに)条件さえ守っていればあとは自由にやっていい、という責任の所在を明らかにする意味もありました。それ以外の部分まで検証に使うのであれば、関数の内容を変更する時にどこまで変えていいのかわからなくなってしまいます。 - 事後条件をもっと正確に書けばいいのでは？
-
そうですね。
balance = old(balance) - amountとかすれば静的検証も成功します。この例に限って言えばそれでいいですが、一般には2つの問題があります。
一つは、oldのような書き方が許されるかどうか、です。許されるシステムを作れ、という話ではありますが、今回は既存の静的検証システムを漸進的検証に変える手法を考えることも目的に入っています。
もう一つは、事後条件をどこまで書けばいいのか、という点が問題になってきます。今回は実装がシンプルなこともありますが、事後条件が関数定義と同一になっています。もっと複雑な関数が出てきた時、そして仕様変更が入った時、事後条件に関数定義を書き続けるのでしょうか。乱数や入出力に至っては契約に書くことも許されないでしょう。
ということで、静的検証の難しさがわかっていただけたかと思います。[9]
この問題を解決するのが漸進的検証です。
漸進的検証の基本アイディアは、静的検証できなかった部分を動的検証でカバーし、かつ背的検証時のデータを使うことで動的検証を最小限に止めるという点です。
まず、 withdraw の事後条件を次のように書き換えます。
// 再掲
int withdraw(int balance, int amount)
requries (balance ≧ amount) // 事前条件
ensures (result ≧ 0 ∧ ?) // 事後条件 末尾に注目！
{
return balance - amount;
}
// 以下がmain関数相当
int balance := 100;
balance := withdraw(balance, 30);
balance := withdraw(balance, 40);
事後条件に ∧ ? というのが追加されましたが、これは「書ききれないけど他にも暗黙の条件があるよ」という意味です。 ∧ は論理記号の「且つ」ですね。漸進的検証においても、この記述がなければやはり静的検証に失敗します。
この検証は大まかに以下のステップを踏みます。
-
静的検証を行う
-
通常なら静的検証に失敗する場面に
∧ ?が関わっていたら、?に何が入れば契約が真になるか算出する -
2の結果を動的検証のための式としてプログラムに追加する (逆に言えば、それ以外の部分は動的検証しない)
ということで、先述の例であれば、1回目の呼び出しは静的検査に成功するので動的検査はなし、2回目の呼び出しの直前 のみ balance ≧ 40 というチェックが実行時に入ることになり、無事に検証成功します。動的検証を0にしたければ事後条件を正確なものに書き換えればいい、というわけですね。
ステップ2は実はある程度ステップ1の結果を利用できることがわかっています。というのも、静的検証で間違っていると判定するためには、あるべき状態と導き出される状態を比較する必要があり、その差分こそが2で求めたい部分である可能性が高いからです。
論文では実際に静的検証から漸進的検証を構成していたり、(漸進的型付けのような)望ましい性質を持っていることを示したりしているのですが、その辺は準備がたくさん必要なのでここではやりません。この先はキミの目で確かめてくれ！というやつですね。
ありそうでなかった「漸進的検証」という力強いタイトルが一番好きなところです。
計算機科学は科学と工学を跨いでいるためか若いためか、様々な概念と手法が発明されては消えていく気がするのですが、それを眺めて驚いたり感心したりするのが大好きなんですよね。
この論文も結論の頭に「We have developed the formal foundations of gradual program verification」とか書いていて、ここから発展させていく気満々ですが、そういう開拓者めいた論文を好んで読んでいます。
実用の観点からはどうなんでしょうね。既存のシステムに追加するものとはいえ、そこそこ計算量があるように思えるので、複雑な検証を現実的な時間で終えられるかの確認が待たれるところです。
実装例もあるとはいえ、プログラムは分岐も書けないようなシンプルなものですし、既存言語に対する検証システムを作るとなると課題も多いように思えます。
ただ、自動挿入される動的検査の内容を見ることができれば(簡単にできるでしょう)、そこからプログラムへの理解が深まったりもすると思うので、少しずつ静的検証に誘導していくには確かに有効だと思っています。
ソフトウェアテストの亜種として、特定の性質を満たすような入力を自動生成するProperty-based Testingという手法がありますが、このあたりを経由して契約を書くように仕向け、最終的に静的検証へ……と行けば面白いなあとか。
理論面がしっかりしているところとか、進的検証化するメタな手法を提案しているところも好きなところです。まあメタ手法を使えば自動的に漸進的検証が出来上がるって感じでもないので、何でもかんでも漸進的にできるということにもならないのですけど。
個人的にアドベントカレンダーはコンパクトにまとまってるのが好きなのですが、自分で書くとどうしても予防線を張ったり詰め込んだりしちゃって長くなってしまいますね。
『今年読んだ一番好きな論文アドベントカレンダー』においては背景説明とかが無くても楽しそうな雰囲気が伝わってくれば読む側としては満足なのですが、やはりどうせなら色々と知ってもらいたくなります。
大人版は参加人数2人と寂しい結果に終わってしまいましたが、個人的にはこういう場があると論文を読み続けるモチベーションになって嬉しいですね。
お粗末様でした。
0 というのはどこかで定数として定義されている変数だったりします。実際に使ったことがないのでわかりませんが、もう少し上等なこともできるでしょう。