Papers/2018/nozomi-master: presentation/slide.html comparison

comparison presentation/slide.html @ 122:c195713cf7d7

Update slide

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Tue, 14 Feb 2017 15:45:03 +0900
parents	137aae675a94
children	81978a9122f0

comparison

equal deleted inserted replaced

-:137aae675a94
+:c195713cf7d7
 <div class='slide '>
 <!-- === begin markdown block ===
 generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-on 2017-02-14 15:02:42 +0900 with Markdown engine kramdown (1.13.0)
+on 2017-02-14 15:44:26 +0900 with Markdown engine kramdown (1.13.0)
 using options {}
 -->
 <!-- _S9SLIDE_ -->
 <h1 id="section">プログラミング言語とソフトウェアの信頼性</h1>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">本発表ではモデル検査的アプローチについて中心に見ていきます</h1>
+<h1 id="section-2">モデル検査的アプローチについての流れ</h1>
-<ul>
-<li>修士論文の内部の比率は半分半分くらい</li>
-<li>定理証明の方は説明する内容が多くて複雑</li>
-<li>モデル検査的アプローチは過去論文を提出したもの
-<ul>
-<li>なのでそちらをメインで発表します</li>
-</ul>
-</li>
-</ul>
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="section-3">モデル検査的アプローチについての流れ</h1>
 <ul>
 <li>既存のモデル検査器について</li>
 <li>Continuation based C (CbC) 言語について</li>
 <li>CbC における CodeSegment と DataSegment を用いたプログラミングスタイル</li>
 <li>CbC とメタ計算について</li>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-4">メタ計算</h1>
+<h1 id="section-3">メタ計算</h1>
 <ul>
 <li>とある計算を実現するための計算</li>
 <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
 <li>CbC は通常レベルの計算とメタ計算を分離して考える
 <ul>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-5">赤黒木</h1>
+<h1 id="section-4">赤黒木</h1>
 <ul>
 <li>データの保存に用いる二分木</li>
 <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
 <ul>
 <li>ルートノードと葉ノードの色は黒</li>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-6">仕様の記述とその確認</h1>
+<h1 id="section-5">仕様の記述とその確認</h1>
 <ul>
 <li>「バランスが取れている」とは何かを表現できる必要がある
 <ul>
 <li>実行可能な CbC の条件式を使った assert になる</li>
 </ul>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-7">チェックする仕様</h1>
+<h1 id="section-6">チェックする仕様</h1>
 <ul>
 <li>赤黒木の高さに関する仕様に以下のものがある
 <ul>
 <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
 </ul>
 </li>
-<li>以下のような条件式を仕様として CbC で定義、検証できる</li>
+<li>以下のような条件式を仕様として CbC で定義できる</li>
 </ul>
 <pre><code>__code verifySpecificationFinish(struct Context* context) {
 if (context-&gt;data[AkashaInfo]-&gt;akashaInfo.maxHeight &gt;
 2*context-&gt;data[AkashaInfo]-&gt;akashaInfo.minHeight)
 <li>goto された時に挿入される要素の組み合わせを全て列挙して実行する
 <ul>
 <li>赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……</li>
 </ul>
 </li>
-<li>その度に仕様の式は成り立つかをチェックする</li>
+<li>挿入する度に仕様の式が成り立つかをチェック</li>
 </ul>
 </li>
 <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
 </ul>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="agda-">Agda における証明</h1>
+<ul>
+<li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
+<ul>
+<li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li>
+</ul>
+</li>
+<li>論理式は型に相当して、証明はその値の導出</li>
+<li>三段論法の証明は以下のようになる
+<ul>
+<li>「((A ならば B) かつ (B ならば C)) ならば (A ならば C)</li>
+</ul>
+</li>
+</ul>
+<pre><code>f : {A B C : Set} -&gt; ((A -&gt; B) × (B -&gt; C)) -&gt; (A -&gt; C)
+f = \p x -&gt; (snd p) ((fst p) x)
+</code></pre>
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="agda--1">Agda における等式の証明</h1>
+<ul>
+<li>Agda では等式も証明できる
+<ul>
+<li>依存型という型を変数として扱える型システムを持つ</li>
+<li>型を取って型を返す型などが定義可能</li>
+</ul>
+</li>
+<li>等式の証明は両方が同じ項に簡約されることを示せば良い</li>
+<li>自然数の加法の交換法則は以下のようになる</li>
+</ul>
+<pre><code>addSym : (n m : Nat) -&gt; n + m ≡ m + n
+addSym O       O   = refl
+addSym O    (S m)  = cong S (addSym O m)
+addSym (S n)   O   = cong S (addSym n O)
+addSym (S n) (S m) = begin
+(S n) + (S m)  ≡⟨ refl ⟩
+S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
+S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
+S (m + S n)    ≡⟨ refl ⟩
+(S m) + (S n)  ∎
+</code></pre>
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="agda--datasegment">Agda と DataSegment</h1>
 <ul>
 <li>CbC の DataSegment は Agda のレコード型
 <ul>
 <li>名前付きの値が複数ある(C の構造体)</li>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-8">メタレベルの型付け</h1>
+<h1 id="section-7">メタレベルの型付け</h1>
 <ul>
 <li>メタ計算とは通常のレベルとは区別された計算</li>
 <li>任意の通常のレベルの計算を扱えなくてはならない
 <ul>
 <li>ライブラリが呼び出されるプログラムは無数にあるようなイメージ</li>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="agda-">Agda 上のメタ計算</h1>
+<h1 id="agda--2">Agda 上のメタ計算</h1>
 <ul>
 <li>ノーマルレベルの型を保持したままメタレベルの計算を利用できる
 <ul>
 <li>cs0 の定義はメタ計算用に変更しなくても良い</li>
 </ul>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="agda--3">Agda 上で証明できた性質</h1>
+<ul>
+<li>CodeSegment の合成則</li>
+</ul>
+<pre><code>comp-associative : &gt; (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
+-&gt; csComp  c (csComp b a) ≡ csComp  (csComp c b) a
+comp-associative (cs _) (cs _) (cs _) = refl
+-- c . (b . a) ≡ (c . b) . a
+</code></pre>
+<ul>
+<li>スタックの操作についての性質</li>
+</ul>
+<pre><code>push-pop-type : ℕ -&gt; ℕ  -&gt; ℕ -&gt; Element ℕ -&gt; Set₁
+push-pop-type n e x s = M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
+-- goto (pop . push) mds ≡ mds
+n-push-pop-type : ℕ -&gt;  ℕ  -&gt; ℕ -&gt; SingleLinkedStack ℕ -&gt; Set₁
+n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop  n) (n-push n)) meta ≡ meta
+-- goto (pop*n . push*n) mds ≡ mds
+</code></pre>
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="agda--cbc-">Agda 上に CbC を記述した成果</h1>
 <ul>
 <li>部分型で CbC の型付けができた</li>
 <li>メタ計算をきちんと階層化できた
 <ul>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-9">まとめ</h1>
+<h1 id="section-8">まとめ</h1>
 <ul>
 <li>Continuation based C 言語を対象にした二種類の検証アプローチ</li>
 <li>モデル検査的なアプローチ
 <ul>
 <li>継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装</li>
-<li>有限の要素数まで保証できた</li>
+<li>有限の要素数まで検証できた</li>
 </ul>
 </li>
 <li>証明的なアプローチ
 <ul>
 <li>証明支援系 Agda 上で CbC のプログラムを定義して直接証明</li>
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-10">今後の課題</h1>
+<h1 id="section-9">今後の課題</h1>
 <ul>
 <li>より大きなサイズの赤黒木の検証</li>
 <li>赤黒木の挿入に関する性質を証明する</li>
 <li>部分型を利用してCbCを型付け</li>
 <li>依存型をCbC に導入して自身を証明可能にする</li>
-<li>型情報から stub を自動生成すkる</li>
+</ul>
-</ul>
+</div>
-</div>
+<div class='slide '>
-<div class='slide '>
+<!-- _S9SLIDE_ -->
-<!-- _S9SLIDE_ -->
+<h1 id="section-10">発表履歴</h1>
-<h1 id="section-11">発表履歴</h1>
 <ul>
 <li>Agda 入門.
 <ul>
 <li>オープンソースカンファレンス 2014 Okinawa, May 2014.</li>
 </ul>

Mercurial > hg > Papers > 2018 > nozomi-master

comparison presentation/slide.html @ 122:c195713cf7d7