セミナーの内容

参加者が自分の好きなプログラミング言語でプログラム検証器を作るハンズオンセミナーです。検証器を作ること通じてプログラム検証の理論である 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 処理系が必要です）
• Z3

配布物

セミナーの約1週間前にスライド資料（PDF)とサンプル実装のソースコードを配布します。

CONNPASS と PayPal に登録されているメールアドレスを今一度ご確認ください。

プログラムの規模

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

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

パーサを作らない場合は、プログラミング言語の構築子や初期化子を使って抽象構文木を手作業で記述します。他の選択としては、サンプル実装に含まれる OCaml のパーサで構築した抽象構文木から、使用するプログラミング言語のコードを生成するという方法があります。これは print 文を修正するだけなので難しくはありません（サンプル実装には Scheme 生成の例があります）。パーサを作る場合は時間の関係上セミナー当日以前に準備する方がよいでしょう。

注意事項

• 配布スライド資料とサンプル実装の公開は禁止です。検証事例はご自由にお使いください（自分で実装したプログラム検証器と一緒に公開するなど）。
• 録画・録音は禁止です。スチル写真撮影はかまいませんが、参加者が写る場合はご自分で許可を得てください。
• 飲食は可能ですが、ゴミはお持ち帰りください。
• 不測の事態によりセミナーが開催できなかった場合は、参加費用の返却にて対応させていただきます。
• CONNPASS ではなく PayPal に登録されているメールアドレスにご連絡を差し上げる場合があります。異なるメールアドレスを登録されている方はお見逃しがないようご注意ください。

連絡先

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