BEGIN:VCALENDAR VERSION:2.0 PRODID:-//https://techplay.jp//JP CALSCALE:GREGORIAN METHOD:PUBLISH X-WR-CALDESC:プログラム検証器を作って学ぶ Hoare 論理 X-WR-CALNAME:プログラム検証器を作って学ぶ Hoare 論理 X-WR-TIMEZONE:Asia/Tokyo BEGIN:VTIMEZONE TZID:Asia/Tokyo BEGIN:STANDARD DTSTART:19700101T000000 TZOFFSETFROM:+0900 TZOFFSETTO:+0900 TZNAME:JST END:STANDARD END:VTIMEZONE BEGIN:VEVENT UID:773587@techplay.jp SUMMARY:プログラム検証器を作って学ぶ Hoare 論理 DTSTART;TZID=Asia/Tokyo:20200523T121000 DTEND;TZID=Asia/Tokyo:20200523T175000 DTSTAMP:20260406T134341Z CREATED:20200301T141859Z DESCRIPTION:イベント詳細はこちら\nhttps://techplay.jp/event/77358 7?utm_medium=referral&utm_source=ics&utm_campaign=ics\n\nセミナーの 内容\n参加者が自分の好きなプログラミング言語でプ ログラム検証器を作るハンズオンセミナーです。検証 器を作ること通じてプログラム検証の理論である Hoare 論理を学びます。\n作っていただくプログラム検証器 は、事前条件・事後条件のペアで表された仕様とプロ グラムを受け取り、プログラムが仕様を満たしている かどうか自動で検証します。もしプログラムが正しけ れば OK を返し、正しくなければ反例を返します。この 反例を見てプログラムのどこが悪いのかを分析し修正 することができます。\n以下に線型探索の例を示しま した。中括弧 {...} で囲まれたところが仕様（2行目が 事前条件、最後の3行が事後条件）です。このプログラ ムは正しいので OK が返されます。\nvars x n i v[]\n{n >= 0}\ ni := 0\;\nwhile i < n & v[i] != x\ninv 0 <= i & i <= n & ALL j. 0 <= j & j < i => v[j] != x\ndo\n i := i + 1\nod\n{0 <= i & i <= n\n & (i < n => v[i] = x)\n & (i = n => ALL j. 0 <= j & j < n => v[j] != x)}\n\n\n\n正 しくないプログラムの例として、例えばループの条件 にある i < n を i <= n と書いてしまったとします。する と検証器は次のように反例を返してくれます。これを 分析することで誤りを見つけることができます（出力 の読み方はセミナーの中で説明します）。\nsat\n(model \n (define-fun i () Int\n 0)\n (define-fun v () (Array Int Int)\n ( lambda ((x!1 Int)) (ite (= (ite (<= 0 x!1) 0 (- 1)) 0) (- 1) 3)))\n (def ine-fun n () Int\n 0)\n (define-fun x () Int\n 0)\n)\n\n\n\nこの ような検証ができるのは Hoare 論理という理論があるか らです。Hoare 論理を使うと数学の証明問題のように机 上でプログラムの正しさを証明することができます。 しかし人手による証明はなかなかたいへんな作業で間 違いもしがちです。せっかくプログラムの正しさを証 明できる理論を持っていても、計算ミスをしてしまっ ては意味がありません。そこで証明をプログラムで自 動化してしまおうというのがこのセミナーの趣旨です 。\n証明はすべて自動で行われます。これは SMT solver というツールのおかげです。SMT solver とは条件を満た す変数の値を見つけてくれるツールで、証明にも使う ことができます。証明できない場合は反例が示されま す。このセミナーでは Z3 という有名な SMT solver を使用 します。\nプログラムが正しくても仕様の規定が不十 分であれば証明はできないので、必要十分な仕様を書 くというトレーニングにもなります。検証が自動で行 われることから「プログラムのここをこう変えたらど うなるだろう？」、「仕様の条件をもっと弱くしたら どうなるだろう？」といった試行が簡単にできます。 そのような試行を通じてプログラムの性質が深く理解 できるようになります。この経験は普段のプログラミ ングやテストによい影響を与えることでしょう。\nプ ログラミングは高度な知的作業で、正しいプログラム を書くのはとても難しいことです。十分なテストをす るにも技術が必要です。もしプログラム検証器が支援 してくれるとしたらすばらしいことでしょう。しかも その検証器を自分で作ることができるのです。この楽 しいプログラミングセミナーにぜひご参加ください。\ nプログラム\n1. Hoare 論理\n\nプログラムの正当性\n事前 条件・事後条件\n契約によるプログラミング\nHoare 論理 \n最弱事前条件と述語変換子\n\n2. SMT solver Z3\nZ3 の使い 方を説明します。\n3. プログラム検証器の設計と実装\n はじめに OCaml と Scheme のサンプル実装を例にプログラ ム検証器のしくみを解説します。それを参考に自分の プログラム検証器を設計・実装します。\n4. プログラ ム検証器の適用例と演習\n\n代入文：swap\n条件文：最大 値・絶対値\nループ：掛け算・総和\n探索とは何か？： 線型探索\n2分法：自然数の平方根の近似値\n2分探索： やさしそうで実はとても難しい\nバブルアップ：この 謎が解けるか？\n\n講師について\n株式会社 PRINCIPIA 代 表取締役 初谷 久史\nCSP 理論に基づいたモデリング・ 検査ツール SyncStitch 開発者\n国立情報学研究所トップ エスイープロジェクト「並行システムの設計検証」講 師\nセミナー参加の前提条件\n前提知識\n必要な知識は 変数、代入文、条件文、ループといった基本的なプロ グラミングの知識です。「～でない・かつ・または」 といった高校で習う程度の論理の知識を仮定します。 条件文やテストを書くときに使う範囲で十分です。\n 必要なもの\n\nノート PC\n使用するプログラミング言語 での開発環境（サンプル実装を動かすためには OCaml ま たは Gauche という Scheme 処理系が必要です）\nZ3\n\n配布 物\nセミナーの約1週間前にスライド資料（PDF)とサンプ ル実装のソースコードを配布します。\nCONNPASS と PayPal に登録されているメールアドレスを今一度ご確認くだ さい。\nプログラムの規模\nプログラム検証器（サンプ ル実装）の規模は次のとおりです。\n\nOCaml 213 行（他 にオプションとしてのパーサ 237 行、lex + yacc 使用）\nS cheme (Gauche) 86 行\n\nパーサを作らない場合は、プログラ ミング言語の構築子や初期化子を使って抽象構文木を 手作業で記述します。他の選択としては、サンプル実 装に含まれる OCaml のパーサで構築した抽象構文木から 、使用するプログラミング言語のコードを生成すると いう方法があります。これは print 文を修正するだけな ので難しくはありません（サンプル実装には Scheme 生 成の例があります）。パーサを作る場合は時間の関係 上セミナー当日以前に準備する方がよいでしょう。\n 注意事項\n\n配布スライド資料とサンプル実装の公開は 禁止です。検証事例はご自由にお使いください（自分 で実装したプログラム検証器と一緒に公開するなど） 。\n録画・録音は禁止です。スチル写真撮影はかまい ませんが、参加者が写る場合はご自分で許可を得てく ださい。\n飲食は可能ですが、ゴミはお持ち帰りくだ さい。\n不測の事態によりセミナーが開催できなかっ た場合は、参加費用の返却にて対応させていただきま す。\nCONNPASS ではなく PayPal に登録されているメールア ドレスにご連絡を差し上げる場合があります。異なる メールアドレスを登録されている方はお見逃しがない ようご注意ください。\n\n連絡先\nご質問等がありまし たら isaac@principia-m.com までお気軽にご連絡ください。 LOCATION:アクセア 神保町貸会議室　第1貸会議室 4F 東京都 千代田区神田神保町2-13-1　西遊ビル4F URL:https://techplay.jp/event/773587?utm_medium=referral&utm_source=ics&utm _campaign=ics END:VEVENT END:VCALENDAR