参加者が自分の好きなプログラミング言語でプログラム検証器を作るセミナーです。検証器を作ること通じてプログラム検証の理論である Hoare 論理を学びます。
作っていただくプログラム検証器は、事前条件・事後条件のペアで表された仕様とプログラムを受け取り、プログラムが仕様を満たしているかどうか自動で検証します。もしプログラムが正しければ OK を返し、正しくなければ反例を返します。この反例を見てプログラムのどこが悪いのかを分析し修正することができます。
以下に線型探索の例を示しました。中括弧 {…} で囲まれたところが仕様（2行目が事前条件、最後の3行が事後条件）です。このプログラムは正しいので OK が返されます。
vars x n i v[]
{n >= 0}
i := 0;
while i < n & v[i] != x
inv 0 <= i & i <= n & ALL j. 0 <= j & j < i => v[j] != x
do
i := i + 1
od
{0 <= i & i <= n
& (i < n => v[i] = x)
& (i = n => ALL j. 0 <= j & j < n => v[j] != x)}正しくないプログラムの例として、例えばループの条件にある
i < n を i <= n
と書いてしまったとします。すると検証器は次のように反例を返してくれます。これを分析することで誤りを見つけることができます（出力の読み方はセミナーの中で説明します）。
sat
(model
(define-fun i () Int
0)
(define-fun v () (Array Int Int)
(lambda ((x!1 Int)) (ite (= (ite (<= 0 x!1) 0 (- 1)) 0) (- 1) 3)))
(define-fun n () Int
0)
(define-fun x () Int
0)
)このような検証ができるのは Hoare 論理という理論があるからです。Hoare 論理を使うと数学の証明問題のように机上でプログラムの正しさを証明することができます。しかし人手による証明はなかなかたいへんな作業で間違いもしがちです。せっかくプログラムの正しさを証明できる理論を持っていても、計算ミスをしてしまっては意味がありません。そこで証明をプログラムで自動化してしまおうというのがこのセミナーの趣旨です。
証明はすべて自動で行われます。これは SMT solver というツールのおかげです。SMT solver とは条件を満たす変数の値を見つけてくれるツールで、証明にも使うことができます。証明できない場合は反例が示されます。このセミナーでは Z3 という有名な SMT solver を使用します。
プログラムが正しくても仕様の規定が不十分であれば証明はできないので、必要十分な仕様を書くというトレーニングにもなります。検証が自動で行われることから「プログラムのここをこう変えたらどうなるだろう？」、「仕様の条件をもっと弱くしたらどうなるだろう？」といった試行が簡単にできます。そのような試行を通じてプログラムの性質が深く理解できるようになります。この経験は普段のプログラミングやテストによい影響を与えることでしょう。
プログラミングは高度な知的作業で、正しいプログラムを書くのはとても難しいことです。十分なテストをするにも技術が必要です。もしプログラム検証器が支援してくれるとしたらすばらしいことでしょう。しかもその検証器を自分で作ることができるのです。この楽しいプログラミングセミナーにぜひご参加ください。
Z3 の使い方を説明します。
OCaml と Scheme のサンプル実装を例にプログラム検証器のしくみを解説します。
必要な知識は変数、代入文、条件文、ループといった基本的なプログラミングの知識です。「～でない・かつ・または」といった高校で習う程度の論理の知識を仮定します。条件文やテストを書くときに使う範囲で十分です。
プログラム検証器（サンプル実装）の規模は次のとおりです。
The Science of Programming, D. Gries, 1981 （邦訳：プログラミングの科学，培風館，1991）
The SMT-LIB Standard http://smtlib.cs.uiowa.edu/language.shtml