セミナーの内容

自分の好きなプログラミング言語でプログラム検証器を作るセミナーです。検証器を作ること通じてプログラム検証の理論である 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 を使用します。

プログラムが正しくても仕様の規定が不十分であれば証明はできないので、必要十分な仕様を書くというトレーニングにもなります。検証が自動で行われることから「プログラムのここをこう変えたらどうなるだろう？」、「仕様の条件をもっと弱くしたらどうなるだろう？」といった試行が簡単にできます。そのような試行を通じてプログラムの性質が深く理解できるようになります。この経験は普段のプログラミングやテストによい影響を与えることでしょう。

プログラミングは高度な知的作業で、正しいプログラムを書くのはとても難しいことです。十分なテストをするにも技術が必要です。もしプログラム検証器が支援してくれるとしたらすばらしいことでしょう。しかもその検証器を自分で作ることができるのです。この楽しいプログラミングセミナーにぜひご参加ください。

プログラム

1. Hoare 論理

• プログラムの正当性
• 事前条件・事後条件
• 契約によるプログラミング
• Hoare 論理
• 最弱事前条件

2. SMT solver Z3

Z3 の使い方を説明します。

3. プログラム検証器の設計と実装

OCaml と Scheme のサンプル実装を例にプログラム検証器のしくみを解説します。

4. プログラム検証器の適用

• 代入文：swap
• 条件文：最大値・絶対値
• ループ：掛け算・総和
• 探索とは何か？：線型探索
• 2分法：自然数の平方根の近似値
• 2分探索：やさしそうで実はとても難しい
• バブルアップ：この謎が解けるか？

講師について

株式会社 PRINCIPIA 代表取締役 初谷 久史

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師

セミナー参加の前提条件

前提知識

必要な知識は変数、代入文、条件文、ループといった基本的なプログラミングの知識です。「～でない・かつ・または」といった高校で習う程度の論理の知識を仮定します。条件文やテストを書くときに使う範囲で十分です。

必要なもの

• PC
• 使用するプログラミング言語での開発環境（サンプル実装を動かすためには OCaml または Gauche という Scheme 処理系が必要です．OCaml による実装は version 4.08.0 を使って動作確認しています）
• Z3
• 計算用紙と筆記用具（途中で演習があります）

配布物

スライド資料（PDF)とサンプル実装のソースコードを CONNPASS のメッセージにて配布します。

Zoom Meeting link

CONNPASS のメッセージにてお知らせします。

プログラムの規模

プログラム検証器（サンプル実装）の規模は次のとおりです。

• OCaml 213 行（他にオプションとしてのパーサ 237 行、lex + yacc 使用）
• Scheme (Gauche) 86 行

注意事項

• 配布スライド資料とサンプル実装の公開は禁止です。検証事例はご自由にお使いください（自分で実装したプログラム検証器と一緒に公開するなど）。
• 実装はセミナー後各自で行っていただくスタイルです．質問はメールにて受け付けます．

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。

参考文献

• The Science of Programming, D. Gries, 1981 （邦訳：プログラミングの科学，培風館，1991）

• The SMT-LIB Standard http://smtlib.cs.uiowa.edu/language.shtml

• Z3 https://github.com/Z3Prover/z3