この記事は Windows & Microsoft 技術基礎 Advent Calendar 2015 の21日目の記事です。

「書かれてもあんまりシェアされないようなネタ」歓迎らしいので，マイナーな検証技術に関する話を書こうと思います。

マイクロソフトはソフトウェア検証に関する基礎的な研究も行っており，マイクロソフトが開発した検証ツールのいくつかが rise4fun で公開されています。今回はここで公開されているツールから以下の3つを紹介したいと思います。

VCC
Boogie
Z3

3者とも rise4fun のサイト上にプレイグラウンドがあり，オンラインで簡単に試すことができます。

VCC

VCC は注釈付き C プログラムの正当性検証ツールです。並行処理を行うプログラムの検証にも対応しています。

簡単な例として，以下の strlen 関数を VCC で検証してみましょう。Playground でも試せます。

#include <vcc.h>

// 文字列 str の長さ (max_len 以下) を返す。
unsigned strlen(char *str, unsigned max_len)
  // 事前条件
  _(requires \thread_local_array(str, max_len))
  _(requires str != NULL)
  // 事後条件
  _(ensures \result < max_len ==> str[\result] == 0)
  _(ensures \forall unsigned i; i < \result ==> str[i] != 0)
{
  unsigned i;
  for (i = 0; i < max_len; i++)
    // ループ不変式
    _(invariant \forall unsigned j; j < i ==> str[j] != 0)
  {
    if (str[i] == 0) break;
  }

  return i;
}

プログラムの事前条件と事後条件を注釈 _(requires ...) と _(eusures ...) で与えています。代わりに，プログラムの途中に表明 _(assert ...) を入れることも可能です。

ホーア論理は皆さんよくご存知ですよね！ループを含むプログラムは，多くの場合，検証の際にループ不変式が必要です。VCC では注釈 _(invariant ...) でループ不変式を明示的に与える必要があります。

このプログラムに対する実行結果は以下の通りです。検証に成功していることがわかります。

Verification of strlen succeeded. [3.16]

Boogie

Boogie はソフトウェア検証器のための中間言語です。なお，Boogieは Boogie言語で書かれた注釈付きプログラムの検証ツールの名前でもあります。VCC や Spec# などのソフトウェア検証器の内部で利用されることを想定して作られています。

VCC で検証を行った先の例は，（あまり忠実には再現できていませんが）Boogie だと以下のように書けます (Playground)。

procedure strlen(str: [int]int, max_len: int) returns (result: int)
  // 事前条件
  requires max_len >= 0;
  // 事後条件
  ensures result < max_len ==> str[result] == 0;
  ensures (forall i: int :: 0 <= i && i < result ==> str[i] != 0);
{
  var i: int;
  i := 0;
  while (i < max_len)
    // ループ不変式
    invariant (forall j: int :: 0 <= j && j < i ==> str[j] != 0);
  {
    if (str[i] == 0) { break; } 
  }
    
  result := i;
}

検証結果は以下の通りです。

Boogie program verifier finished with 1 verified, 0 errors

Z3

Z3 は SMT ソルバと呼ばれる種類のツールで，算術式などを含む論理式の充足可能性を判定することができます。Boogie をはじめとする様々な証明器の内部で使われています。

簡単な例として，$x > 1 \land y > 1 \land 2x + 3y < 11$ が整数上で充足可能か検証してみましょう。Playground でも試せます。

(declare-fun x () Int)
(declare-fun y () Int)

(assert (> x 1))
(assert (> y 1))
(assert (< (+ (* 2 x) (* 3 y)) 11))

(check-sat)  ; 充足可能性を判定
(get-model)  ; 式を充足する割当てを表示（あれば）

これを Z3 に投げると，以下のような出力が得られます。

sat
(model 
  (define-fun y () Int 
    2)
  (define-fun x () Int
    2) 
)

1行目に表示される sat は (check-sat) の結果であり，$x > 1 \land y > 1 \land 2x + 3y < 11$ が充足可能であると判定されたことを意味します。充足不能と判定されると unsat が返り，Z3 が力尽きて判定を諦めると unknown が返ります。

充足可能であった場合，(get-model) で式を充足する割当て（モデル）の一つを表示できます。今回のモデルは $\{ x \mapsto 2,\ y \mapsto 2 \}$ と一意に決まるはずです。

おわりに

さすがに VCC と Boogie と Z3 を一緒に紹介している日本語の文献はこれが初めてではないでしょうか？今度はZ3のソースを読んでみたいな。