新機能 イベントメッセージの予約機能を追加しました。イベント主催者様は、参加者へのメッセージ送信を事前に予約できます。詳しくはこちらをご確認ください。

新機能 イベント詳細画面に「参加者への情報」欄を追加しました。イベント管理者、発表者、参加者(抽選中や補欠は除く)だけに表示されるフィールドです。詳しくはこちら

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

Jul

24

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

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

Organizing : 株式会社 PRINCIPIA

Hashtag :#形式手法
Registration info

一般

8000 (Pre-pay)

FCFS
5/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/07/24(Fri)

13:00
17:00

Registration Period
2020/07/16(Thu) 00:00 〜
2020/07/24(Fri) 12:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(5)

billtherizard

billtherizard

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

Shin Sahara

Shin Sahara

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

tukejonny

tukejonny

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

Tute

Tute

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

takarakasai

takarakasai

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

Attendees (5)