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

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

May

23

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

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

Organizing : 株式会社 PRINCIPIA

Registration info

一般

8000 (Pre-pay)

FCFS
3/16

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 処理系が必要です)
  • Z3

配布物

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

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

プログラムの規模

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

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

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

注意事項

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

連絡先

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

Media View all Media

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

Feed

プログラム検証器を作って学ぶ Hoare 論理 has been canceled. You cannot attend this event.
You can ask questions to the event organizer by writing a comment on the event page.

03/27/2020 21:11

hatsugai

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

03/01/2020 18:25

プログラム検証器を作って学ぶ Hoare 論理 を公開しました!

中止

2020/05/23(Sat)

12:10
17:50

You cannot RSVP if you are already participating in another event at the same date.

Registration Period
2020/03/01(Sun) 00:00 〜
2020/05/23(Sat) 12:00

Location

アクセア 神保町貸会議室 第1貸会議室 4F

東京都千代田区神田神保町2-13-1 西遊ビル4F

Organizer

Attendees(3)

tacke_jp

tacke_jp

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

tkokamo

tkokamo

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

秋津早苗

秋津早苗

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

Attendees (3)