新機能 オンラインイベントが検索できるようになりました。オンラインイベントとして検索できるようにするには こちら をご確認ください

このエントリーをはてなブックマークに追加

May

2

プログラム検証器を作って学ぶ Hoare 論理

好きな言語でプログラム検証器を作りましょう。

Organizing : 株式会社 PRINCIPIA

Hashtag :#FormalVerification
Registration info

一般

8000 (Pre-pay)

FCFS
10/10

About Prepayment

About Prepayment Contact Info:

(Only shown to attendees.)

Cancel/Refund Policy:

お支払いいただくのは資料(スライド資料とサンプル実装および事例モデル)の代金です.セミナー参加費は無料です.したがいまして資料配布後にキャンセルしても代金は返却されません.特に主催者から見て資料配布後にキャンセルを認識した場合は返却されません.よくご検討の上,お申し込みください.

Print receipt data:

発行しない (詳しくはこちら)

Description

セミナーの内容

参加者が自分の好きなプログラミング言語でプログラム検証器を作るセミナーです。検証器を作ること通じてプログラム検証の理論である 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 < ni <= 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 までお気軽にご連絡ください。

参考文献

Media View all Media

If you add event media, up to 3 items will be shown here.

Ended

2020/05/02(Sat)

14:00
18:00

Registration Period
2020/04/21(Tue) 00:00 〜
2020/05/02(Sat) 13:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(10)

TakeshiHori

TakeshiHori

プログラム検証器を作って学ぶ Hoare 論理 に参加を申し込みました!

hxf_vogel

hxf_vogel

証明初心者です、楽しみにしてます

tkokamo

tkokamo

プログラム検証器を作って学ぶ Hoare 論理に参加を申し込みました!

Ken Sonoda

Ken Sonoda

プログラム検証器を作って学ぶ Hoare 論理に参加を申し込みました!

elkel53930

elkel53930

プログラム検証器を作って学ぶ Hoare 論理に参加を申し込みました!

IKEBE Ryohji

IKEBE Ryohji

プログラム検証器を作って学ぶ Hoare 論理 に参加を申し込みました!

shigemi1014

shigemi1014

I joined プログラム検証器を作って学ぶ Hoare 論理!

hirofumi

hirofumi

プログラム検証器を作って学ぶ Hoare 論理 に参加を申し込みました!

tos

tos

プログラム検証器を作って学ぶ Hoare 論理 に参加を申し込みました!

チェシャ猫

チェシャ猫

プログラム検証器を作って学ぶ Hoare 論理 に参加を申し込みました!

Attendees (10)