Mercurial > hg > Papers > 2019 > ryokka-sigss

--- a/slide/slide.html	Tue Jan 15 17:59:14 2019 +0900
+++ b/slide/slide.html	Wed Jan 16 03:19:15 2019 +0900
@@ -10,7 +10,7 @@
    <title>GearsOS の Hoare Logic を用いた検証</title>

    <meta name="generator" content="Slide Show (S9) v4.0.1 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]">
-   <meta name="author"    content="Masataka Hokama" >
+   <meta name="author"    content="外間政尊 , 河野真治" >

 <!-- style sheet links -->
 <link rel="stylesheet" href="s6/themes/projection.css"   media="screen,projection">
@@ -77,7 +77,7 @@
       <tr>
         <td>
           <div align="left">
-              Masataka Hokama
+              外間政尊 , 河野真治
               琉球大学 : 並列信頼研究室
             <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;">
           </div>
@@ -93,7 +93,7 @@


 <!-- _S9SLIDE_ -->
-<h2 id="研究背景">研究背景</h2>
+<h2 id="os-の検証技術としての-hoarelogic-の問題点">OS の検証技術としての HoareLogic の問題点</h2>
 <ul>
   <li>OS やアプリケーションなどの信頼性は重要な課題</li>
   <li>信頼性を上げるために仕様を検証する必要</li>
@@ -102,7 +102,8 @@
       <li>事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす</li>
     </ul>
   </li>
-  <li>既存の言語ではあまり利用されていない</li>
+  <li>OS の検証などで使われているが、実装の記述の他に関数型の記述が必要となる</li>
+  <li>HoareLogic の単位である代入や、WhileLoop に対応する分解が煩雑</li>
 </ul>


@@ -111,14 +112,14 @@

 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="背景">背景</h2>
+<h2 id="gearsos-によるメタ計算としての-hoarelogic-の導入">GearsOS によるメタ計算としての HoareLogic の導入</h2>
 <ul>
   <li>当研究室では 処理の単位を <strong>CodeGear</strong>、データの単位を <strong>DataGear</strong> としてプログラムを記述する手法を提案</li>
-  <li>CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
-<!-- - Gear 間の接続処理はメタ計算として定義 -->
-<!--   - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証 --></li>
+  <li>CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む</li>
   <li>この単位を用いて信頼性の高い OS として GearsOS を開発している</li>
-  <li>本発表では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する</li>
+  <li>Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する</li>
+  <li>CodeGear は CbC により、C と同等の速度で実行可能かつ Agda の継続記述にもなっている</li>
+  <li>変換を必要とせずに HoareLogic による証明をメタ計算として記述できる</li>
 </ul>


@@ -150,94 +151,19 @@

 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="cbc-について">CbC について</h2>
-<ul>
-  <li>Gears の単位でプログラミングできる言語として当研究室で開発している <strong>CbC</strong> (Continuation based C) が存在
-    <ul>
-      <li>これは C からループ制御構造と関数呼び出しを取り除き、代わりに継続を導入したもの</li>
-    </ul>
-  </li>
-  <li>現在の CbC でもメタ計算での検証は可能</li>
-  <li>将来的には証明も扱えるようにしたいが現段階では未実装</li>
-  <li>そのため Gears の単位を定理証明支援系の言語である <strong>Agda</strong> で記述し、 Agda で証明している</li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-とは">Agda とは</h2>
+<h2 id="agda-での-datagear">Agda での DataGear</h2>
 <ul>
-  <li>Agda は定理証明支援系の言語</li>
-  <li>依存型を持つ関数型言語</li>
-  <li>Curry-Howard の証明支援系</li>
-  <li>型と値がある</li>
-  <li>Agda の文法については次のスライドから軽く説明する</li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2>
-<ul>
-  <li>Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数</li>
-  <li>CPS の関数は引数として継続を受け取って継続に計算結果を渡す</li>
-  <li><strong>名前 : 引数 → (Code : fa → t) → t</strong></li>
-  <li><strong>t</strong> は継続</li>
-  <li><strong>(Code : fa → t)</strong> は次の継続先</li>
-  <li>DataGear は Agda での CodeGear に使われる引数
+  <li><strong>DataGear</strong> は CodeGear でつかわれる引数</li>
+  <li><strong>データ型</strong>と<strong>レコード型</strong>がある</li>
+  <li>データ型は一つのデータ
     <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre>whileTest : {l : Level} {t : Set l} -&gt; (c10 : ℕ)
-                   → (Code : Env -&gt; t) -&gt; t
-whileTest c10 next = next (record {varn = c10 ; vari = 0} )
+  <div class="code"><pre>data Nat : Set where
+zero : Nat
+suc  : Nat → Nat
 </pre></div>
 </div>
     </div>
   </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-での-gears-の記述whileloop-1">Agda での Gears の記述(whileLoop)</h2>
-<ul>
-  <li>関数の動作を条件で変えたいときはパターンマッチを行う</li>
-  <li>whileLoop は varn が 0 より大きい間ループする
-    <ul>
-      <li>lt は Nat を２つ受け取って値の大小を比較
-```AGDA
-{-# TERMINATING #-}
-whileLoop : {l : Level} {t : Set l} -&gt; Env
-          -&gt; (Code : Env -&gt; t) -&gt; t
-whileLoop env next with lt 0 (varn env)
-whileLoop env next | false = next env
-whileLoop env next | true =
- whileLoop (record {varn = (varn env) - 1
-                  ; vari = (vari env) + 1}) next</li>
-    </ul>
-  </li>
-</ul>
-
-<p>lt : Nat → Nat → Bool</p>
-<pre><code>
-## Agda での DataGear
-- **DataGear** は CodeGear の引数
-- **データ型**と**レコード型**がある
-- データ型は一つのデータ
-```AGDA
-data Nat : Set where
-  zero : Nat
-  suc  : Nat → Nat
-</code></pre>
-<ul>
   <li>レコード型は複数のデータをまとめる
     <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre>record Env : Set where
@@ -256,20 +182,79 @@

 <div class='slide'>
   <!-- _S9SLIDE_ -->
+<h2 id="agda-での-gears-の記述whiletest">Agda での Gears の記述(whileTest)</h2>
+<ul>
+  <li>Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数</li>
+  <li><strong>{}</strong> は暗黙的(推論される)</li>
+  <li>継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す</li>
+  <li>CodeGear の型は<strong>名前 : 引数 → (Code : fa → t) → t</strong></li>
+  <li><strong>t</strong> は継続(最終的に返すもの)</li>
+  <li><strong>(Code : fa → t)</strong> は次の継続先
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>whileTest : {t : Set} → (c10 : Nat)
+          → (Code : Env → t) → t
+whileTest c10 next = next (record {varn = c10
+                               ; vari = 0} )
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2>
+<ul>
+  <li>関数の動作を条件で変えたいときはパターンマッチを行う</li>
+  <li>whileLoop は varn が 0 より大きい間ループする</li>
+  <li><strong>lt</strong> は Nat を２つ受け取って値の大小を比較する関数
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>whileLoop : {t : Set} → Env
+            → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true =
+   whileLoop (record {varn = (varn env) - 1
+                    ; vari = (vari env) + 1}) next
+</pre></div>
+</div>
+    </div>
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>lt : Nat → Nat → Bool
+lt x y with (suc x ) ≤? y
+lt x y | yes p = true
+lt x y | no ¬p = false
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
 <h2 id="agda-での証明">Agda での証明</h2>
 <ul>
-  <li>関数の型に証明すべき論理式</li>
-  <li>関数自体にそれを満たす導出</li>
-  <li>完成した関数は証明</li>
-  <li><strong>{}</strong> は暗黙的(推論される)</li>
-  <li>下のコードは Bool型の x と true の and を取ったものは x と等しいことの証明
+  <li>証明の見た目関数と同じ</li>
+  <li>関数との違いは<strong>型が証明すべき論理式</strong>で<strong>関数自体がそれを満たす導出</strong></li>
+  <li><strong>refl</strong> は <strong>x == x</strong> で左右の項が等しいことの証明</li>
+  <li>変換で使っている <strong>cong</strong> は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明</li>
+  <li><strong>+zero</strong> は任意の自然数の右から zero を足しても元の数と等しいことの証明
     <ul>
-      <li><strong>refl</strong> は <strong>x == x</strong> の左右の項が等しいことの証明
+      <li><strong>y = zero</strong> のときは <strong>zero ≡ zero</strong> のため refl</li>
+      <li><strong>y = suc y</strong> のときは cong を使い y の数を減らして再帰的に<strong>+zero</strong>を行っている</li>
+      <li>y の数を減らしても大丈夫なことを cong の関数として受け取った数を suc する関数で保証している
         <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre>∧true : { x : Bool } →  x  ∧  true  ≡ x
-∧true {x} with x
-∧true {x} | false = refl
-∧true {x} | true = refl
+  <div class="code"><pre>+zero : { y : Nat } → y + zero ≡ y
++zero {zero} = refl
++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
 </pre></div>
 </div>
         </div>
@@ -284,19 +269,160 @@

 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gears-をベースにした-hoarelogic-と証明全体">Gears をベースにした HoareLogic と証明(全体)</h2>
+<h2 id="agda-での項変換による証明-13">Agda での項変換による証明 1/3</h2>
+<ul>
+  <li>次は<strong>x + y ≡ y + x</strong> の証明 <strong>+-sym</strong></li>
+  <li>項変換の例として zero, suc y のパターンをみる</li>
+  <li><strong>zero + suc y</strong>を変換して<strong>suc y + zero</strong>にする</li>
+  <li>begin の下の行に変形したい式を記述</li>
+  <li><strong>≡⟨  ⟩</strong> に変形規則、その次の行に変換した結果、 <strong>∎</strong> が項変換終了</li>
+  <li>{ }0, { }1 は ? で置いたあとコンパイルを通すと Agda が示してくれる
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>+-sym : { x y : Nat } → x + y ≡ y + x
++-sym {zero} {zero} = refl
++-sym {zero} {suc y} = let open ≡-Reasoning  in
+        begin
+          zero + suc y
+        ≡⟨ { }0 ⟩
+          { }1
+        ∎
+----------------------
+?0 : zero + suc y ≡ suc y + zero
+?1 : Nat
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での証明項変換-23">Agda での証明(項変換) 2/3</h2>
 <ul>
-  <li>Gears をベースにした while Program で実行できる
+  <li>はじめの変換規則は何も書かずに簡約</li>
+  <li>次に右から zero を足しても等しくなる証明規則を使いたい
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>+-sym {zero} {suc y} = let open ≡-Reasoning  in
+        begin
+          zero + suc y
+        ≡⟨⟩
+          suc y
+        ≡⟨ { }0  ⟩
+          { }1
+        ∎
+----------------------
+?0 : suc y ≡ suc y + zero
+?1 : Nat
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-での証明項変換-33">Agda での証明(項変換) 3/3</h2>
+<ul>
+  <li>証明の例で使用した<strong>+zero</strong>は<strong>y + zero ≡ y</strong></li>
+  <li>これを使いたいが今回は<strong>y + zero ≡ y</strong></li>
+  <li>Agda の StandartLibrary にある sym を用いて <strong>+zero</strong> を <strong>y + zero ≡ y</strong> として適応することで証明ができる
+```AGDA
+– +zero : { y : Nat } → y + zero ≡ y
++-sym {zero} {suc y} = let open ≡-Reasoning  in
+        begin
+          zero + suc y
+        ≡⟨⟩
+          suc y
+        ≡⟨ sym +zero  ⟩
+          suc y + zero
+        ∎</li>
+</ul>
+
+<p>sym : Symmetric {A = A} <em>≡</em>
+sym refl = refl</p>
+<pre><code>
+## HoareLogicをベースとした Gears での検証手法
+- 今回 HoareLogic で証明する例の疑似コードを用意した
+- このプログラムは変数iとnをもち、 n&gt;0 の間nの値を減らし、i の値を増やす
+- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。
+```C
+   n = 10;
+   i = 0;
+</code></pre>
+<div class="language-c highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>   <span style="color:#080;font-weight:bold">while</span> (n&gt;<span style="color:#00D">0</span>)
+   {
+     i++;
+     n--;
+   }
+</pre></div>
+</div>
+</div>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gears-をベースにしたプログラム">Gears をベースにしたプログラム</h2>
+<ul>
+  <li>test は whileTest と whileLoop を使った Gears のプログラム</li>
+  <li>whileTest の継続先にDataGear を受け取って whileLoop に渡す
     <ul>
-      <li>これは証明も持っている</li>
+      <li><strong>(λ 引数 → )</strong>は無名関数で引数を受け取って継続する</li>
     </ul>
   </li>
-  <li>whileループを任意の回数にするため<strong>c10</strong>は引数</li>
+  <li>説明のため whileTest と whileLoop の型を載せておく
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>test : Env
+test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
+</pre></div>
+</div>
+    </div>
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>whileTest : {t : Set} → (c10 : Nat)
+          → (Code : Env → t) → t
+</pre></div>
+</div>
+    </div>
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>whileLoop : {t : Set} → Env
+            → (Code : Env → t) → t
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gears-をベースにした-hoarelogic-と証明全体">Gears をベースにした HoareLogic と証明(全体)</h2>
+<ul>
+  <li>proofGears は HoareLogic をベースとした証明
+    <ul>
+      <li>先程のプログラムと違い、引数として証明も持っている</li>
+    </ul>
+  </li>
   <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい
     <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre>proofGears : {c10 :  Nat } → Set
-proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1
-       (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
+  <div class="code"><pre>-- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
+proofGears : {c10 :  Nat } → Set
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →
+       conversion1 n p1  (λ n1 p2 → whileLoop' n1 p2
+       (λ n2 →  ( vari n2 ≡ c10 ))))
 </pre></div>
 </div>
     </div>
@@ -315,19 +441,21 @@
   <li>proof2は Post Condition が成り立つことの証明
     <ul>
       <li><strong><em>/\</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li>
-      <li>２つのものを引数に取り、両方が同時に成り立つことを示す</li>
+      <li>２つのものを引数に取り、両方が同時に成り立つことを表している</li>
+      <li><strong>refl</strong> は <strong>x == x</strong> で左右の項が等しいことの証明</li>
     </ul>
   </li>
   <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong>
     <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre>whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } →
+  <div class="code"><pre>-- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t
+whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } →
       (Code : (env : Env)  →
           ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-hileTest' {_} {_} {c10} next = next env proof2
+whileTest' {_} {_} {c10} next = next env proof2
 where
   env : Env
   env = record {vari = 0 ; varn = c10}
-  proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)      &lt;-- PostCondition
+  proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
   proof2 = record {pi1 = refl ; pi2 = refl}
 </pre></div>
 </div>
@@ -350,32 +478,70 @@
   </li>
   <li>proof4 は LoopInvaliant の証明</li>
   <li>Gears での HoareLogic の完全な記述は <strong>引数 → PreCondition → (Code : fa → PostCondition → t) → t</strong>
-```AGDA
-conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  Nat } →
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  Nat } →
         ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
         → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
 conversion1 env {c10} p1 next = next env proof4
 where
-  proof4 : varn env + vari env ≡ c10</li>
+  proof4 : varn env + vari env ≡ c10
+</pre></div>
+</div>
+    </div>
+  </li>
 </ul>

-<pre><code>
+
+
+</div>

-##  Agdaでの証明(≡-Reasoning)
-- Agda では証明の項を書き換える構文が用意されている
-```AGDA
-    proof4 : varn env + vari env ≡ c10
-    proof4 = let open ≡-Reasoning  in
-      begin
-        varn env + vari env
-      ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
-        c10 + vari env
-      ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
-        c10 + 0
-      ≡⟨ +-sym {c10} {0} ⟩
-        c10
-      ∎
-</code></pre>
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="hoarelogic-の証明">HoareLogic の証明</h2>
+<ul>
+  <li>HoareLogic の証明では基本的に項の書き換えを行って証明している</li>
+  <li>proof4 の証明部分では論理式の<strong>varn env + vari env</strong> を 書き換えて <strong>c10</strong> に変換している</li>
+  <li>変換で使っている <strong>cong</strong> は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明</li>
+  <li>変換後の式を次の行に書いて変換を続ける
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>-- precond : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+conversion1 env {c10} precond next = next env proof4
+where
+  proof4 : varn env + vari env ≡ c10
+  proof4 = let open ≡-Reasoning  in
+    begin
+      varn env + vari env
+    ≡⟨ cong ( λ n → n + vari env ) (pi2 precond ) ⟩
+      c10 + vari env
+    ≡⟨ cong ( λ n → c10 + n ) (pi1 precond ) ⟩
+      c10 + 0
+    ≡⟨ +-sym {c10} {0} ⟩
+      c10
+    ∎
+--  +-sym : { x y : Nat } → x + y ≡ y + x
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gears-と-hoarelogic-をベースにした証明whileloop">Gears と HoareLogic をベースにした証明(whileLoop)</h2>
+<ul>
+  <li>whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre>-- whileLoop : {t : Set} → Env → (Code : Env → t) → t
+whileLoop' : {t : Set} → (env : Env) → {c10 :  Nat } → ((varn env) + (vari env) ≡ c10) → (Code : Env → t) → t
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>


@@ -405,7 +571,6 @@
   <!-- _S9SLIDE_ -->
 <h2 id="まとめと今後の課題">まとめと今後の課題</h2>
 <ul>
-  <li>HoareLogic の while を使った例題を作成、証明を行った</li>
   <li>Gears を用いた HoareLogic ベースの検証方法を導入した
     <ul>
       <li>証明が引数として渡される記述のため証明とプログラムを一体化できた</li>
@@ -424,326 +589,9 @@

 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogic">Agda 上での HoareLogic</h2>
-<ul>
-  <li>Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと
-それを Agda2 に書き写したものが存在している。</li>
-  <li>今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて Agda2上で HoareLogic を構築する</li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="hoarelogic-とは">HoareLogic とは</h2>
-<ul>
-  <li>Floyd-Hoare Logic (以下HoareLogic)は部分的な正当性を検証する</li>
-  <li>プログラムは事前条件(Pre Condition)、事後条件(Post Condition)を持ち、条件がコマンドで更新され、事後条件になる</li>
-  <li>事前、事後条件には変数や論理式、コマンドには代入や、繰り返し、条件分岐などがある。</li>
-  <li>コマンドが正しく成り立つことを保証することで、このコマンドを用いて記述されたプログラムの部分的な正しさを検証できる</li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="hoarelogic-の理解">HoareLogic の理解</h2>
-<ul>
-  <li>HoareLogic 例として疑似コードを用意した</li>
-  <li>このプログラムは変数iとnをもち、 n&gt;0 の間nの値を減らし、i の値を増やす</li>
-  <li>n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。</li>
-  <li>次のスライドから Agda 上 HoareLogic を実装し、その上でこの whileProgram の検証を行う
-    <div class="language-C highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre> n = <span style="color:#00D">10</span>;
- i = <span style="color:#00D">0</span>;
-
- <span style="color:#080;font-weight:bold">while</span> (n&gt;<span style="color:#00D">0</span>)
- {
-   i++;
-   n--;
- }
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogic条件変数の定義">Agda 上での HoareLogic(条件、変数の定義)</h2>
-<ul>
-  <li><strong>Env</strong> は while Program で必要な変数をまとめたもの</li>
-  <li>varn、vari はそれぞれ変数 n、 i</li>
-  <li><strong>Cond</strong> は Pre、Post の Condition で Env を受け取って Bool 値(true か false)を返す
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre> record Env : Set where
-   field
-     varn : Nat
-     vari : Nat
-
- Cond : Set
- Cond = (Env → Bool)
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogicコマンド定義">Agda 上での HoareLogic(コマンド定義)</h2>
-<ul>
-  <li><strong>Comm</strong> は Agda のデータ型で定義した HoareLogic のコマンド
-    <ul>
-      <li><strong>PComm</strong> は変数を代入のコマンド</li>
-      <li><strong>Seq</strong> はコマンドの推移、 Command を実行して次の Command に移す</li>
-      <li><strong>If</strong> は条件分岐のコマンド</li>
-      <li><strong>while</strong> は繰り返しのコマンド</li>
-    </ul>
-  </li>
-  <li>他にも何もしないコマンドやコマンドの停止などのコマンドもある</li>
-  <li><strong>PrimComm</strong> は Env を受け取って Env を返す定義
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre>   data Comm : Set where
-     PComm : PrimComm → Comm
-     Seq   : Comm → Comm → Comm
-     If    : Cond → Comm → Comm → Comm
-     While : Cond → Comm → Comm
-
-   PrimComm : Set
-   PrimComm = Env → Env
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogic実際のプログラムの記述">Agda 上での HoareLogic(実際のプログラムの記述)</h2>
-<ul>
-  <li>先程定義したコマンドを使って while Program を記述した
-    <ul>
-      <li>任意の自然数を引数に取る形になっているが<strong>c10 == 10</strong>ということにする</li>
-    </ul>
-  </li>
-  <li><strong>$</strong> は <strong>()</strong> の糖衣で行頭から行末までを ( ) で囲う</li>
-  <li>見やすさのため改行しているが 3~7 行は1行
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre> program : ℕ → Comm
- program c10 =
-    Seq ( PComm (λ env → record env {varn = c10}))                -- n = 10;
-    $ Seq ( PComm (λ env → record env {vari = 0}))                -- i = 0;
-    $ While (λ env → lt zero (varn env ) )                         -- while (n&gt;0) {
-      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++;
-        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))   -- n--;
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogicコマンドの保証13">Agda 上での HoareLogic(コマンドの保証)1/3</h2>
+<h2 id="発表終了">発表終了</h2>
 <ul>
-  <li>保証の規則は HTProof にまとめられてる</li>
-  <li><strong>PrimRule</strong> は <strong>PComm</strong> で行う代入を保証する</li>
-  <li>3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述
-    <ul>
-      <li><strong><em>⇒</em></strong> は pre, post の Condition をとって post の Condition が成り立つときに True を返す
-        <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre> data HTProof : Cond → Comm → Cond → Set where
- PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} →
-              (pr : Axiom bPre pcm bPost) →
-              HTProof bPre (PComm pcm) bPost
--- 次のスライドに続く
-</pre></div>
-</div>
-        </div>
-        <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre> Axiom : Cond → PrimComm → Cond → Set
- Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
-</pre></div>
-</div>
-        </div>
-      </li>
-    </ul>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogicコマンド保証23">Agda 上での HoareLogic(コマンド保証)2/3</h2>
-<ul>
-  <li><strong>SeqRule</strong> は Command を推移させる Seq の保証</li>
-  <li><strong>IfRule</strong> は If の Command が正しく動くことを保証
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre>-- HTProof の続き
-   SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} →
-           {cm2 : Comm} → {bPost : Cond} →
-           HTProof bPre cm1 bMid →
-           HTProof bMid cm2 bPost →
-           HTProof bPre (Seq cm1 cm2) bPost
-   IfRule : {cmThen : Comm} → {cmElse : Comm} →
-          {bPre : Cond} → {bPost : Cond} →
-          {b : Cond} →
-          HTProof (bPre /\ b) cmThen bPost →
-          HTProof (bPre /\ neg b) cmElse bPost →
-          HTProof bPre (If b cmThen cmElse) bPost
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogicコマンド保証33">Agda 上での HoareLogic(コマンド保証)3/3</h2>
-<ul>
-  <li><strong>WeakeningRule</strong> は通常の Condition からループ不変条件(Loop Invaliant)に変換</li>
-  <li>Tautology は Condition と不変条件が等しく成り立つ</li>
-  <li><strong>WhileRule</strong> はループ不変条件が成り立つ間 Comm を繰り返す
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre>-- HTProof の続き
-   WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} →
-               {bPost' : Cond} → {bPost : Cond} →
-               Tautology bPre bPre' →
-               HTProof bPre' cm bPost' →
-               Tautology bPost' bPost →
-               HTProof bPre cm bPost
-   WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} →
-               HTProof (bInv /\ b) cm bInv →
-               HTProof bInv (While b cm) (bInv /\ neg b)
-</pre></div>
-</div>
-    </div>
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre> Tautology : Cond → Cond → Set
- Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogic証明">Agda 上での HoareLogic(証明)</h2>
-<ul>
-  <li><strong>proof1</strong> は while Program の証明</li>
-  <li>HTProof に 初期状態と先程コマンドで記述した whileProgram である <strong>program</strong> と終了状態を渡す</li>
-  <li>Condititon は initCond や termCond のようにそれぞれ定義する必要がある</li>
-  <li>program に近い形で証明を記述できる
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre> proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
- proof1 c10 =
-       SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
-       $ SeqRule {λ e →  Equal (varn e) c10} ( PrimRule lemma1   )
-       $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)}  lemma2 (
-          WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
-          $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
-             $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
-
- initCond : Cond
- initCond env = true
-
- termCond : {c10 : Nat} → Cond
- termCond {c10} env = Equal (vari env) c10
-</pre></div>
-</div>
-    </div>
-    <!-- * lemma1~5は rule それぞれの証明 -->
-    <!-- program : Comm -->
-    <!-- program =  -->
-    <!--   Seq ( PComm (λ env → record env {varn = 10})) -->
-    <!--   $ Seq ( PComm (λ env → record env {vari = 0})) -->
-    <!--   $ While (λ env → lt zero (varn env ) ) -->
-    <!--     (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -->
-    <!--       $ PComm (λ env → record env {varn = ((varn env) - 1)} )) -->
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="証明の一部lemma1">証明の一部(lemma1)</h2>
-<ul>
-  <li>PComm の証明である lemma1 だけ解説</li>
-  <li>lemma1 は n に 10 を代入したあと、 i に 0 を代入するところ</li>
-  <li>証明することは<strong>事前条件の n ≡ 10 が成り立つか</strong></li>
-  <li>PreCondition が成り立つとき、Command を実行するとPostConditionが成り立つ
-    <ul>
-      <li>Axiom は x ⇒ y  ≡ true が成り立てば良かった</li>
-      <li><strong><em>⇒</em></strong> は事後条件が成り立つかどうか</li>
-      <li>impl⇒ は x ≡ true → y ≡ true の関数(Command)を受け取って x ⇒ y  ≡ true を返す関数</li>
-    </ul>
-  </li>
-  <li><strong>≡-Reasoning</strong> は Agda での等式変形
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre>  lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10})
-         (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
-  lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
-    begin
-      (Equal (varn env) c10 ) ∧ true
-    ≡⟨ ∧true ⟩
-      Equal (varn env) c10
-    ≡⟨ cond ⟩
-      true
-    ∎ )
-
-  stmt1Cond : {c10 : ℕ} → Cond
-  stmt1Cond {c10} env = Equal (varn env) c10
-
-  stmt2Cond : {c10 : ℕ} → Cond
-  stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
-</pre></div>
-</div>
-    </div>
-
-    <p><!-- lemma2 :  {c10 : Nat} → Tautology stmt2Cond whileInv --></p>
-
-    <p><!-- lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' --></p>
-
-    <p><!-- lemma4 :  {c10 : Nat} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv --></p>
-
-    <p><!-- lemma5 : {c10 : Nat} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond  --></p>
-  </li>
+  <li>ご清聴ありがとうございました。</li>
 </ul>
--- a/slide/slide.md	Tue Jan 15 17:59:14 2019 +0900
+++ b/slide/slide.md	Wed Jan 16 03:19:15 2019 +0900
@@ -1,5 +1,5 @@
 title: GearsOS の Hoare Logic を用いた検証
-author: 外間政尊 : 河野真治
+author: 外間政尊 , 河野真治
 profile: 琉球大学 : 並列信頼研究室
 lang: Japanese

@@ -35,38 +35,8 @@
 <!-- <p style="text-align:center;"><img src="./pic/cgdg.svg" alt=""  width="30%" height="30%"/></p> -->


-## Agda での Gears の記述(whileLoop)
-- Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数
-- 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す
-- **名前 : 引数 → (Code : fa → t) → t**
-- **t** は継続
-- **(Code : fa → t)** は次の継続先
-- DataGear は Agda での CodeGear に使われる引数
-```AGDA
-whileTest : {l : Level} {t : Set l} -> (c10 : ℕ)
-                     → (Code : Env -> t) -> t
-whileTest c10 next = next (record {varn = c10 ; vari = 0} )
-```
-
-## Agda での Gears の記述(whileLoop)
-- 関数の動作を条件で変えたいときはパターンマッチを行う
-- whileLoop は varn が 0 より大きい間ループする
-  - lt は Nat を２つ受け取って値の大小を比較
-```AGDA
-{-# TERMINATING #-}
-whileLoop : {l : Level} {t : Set l} -> Env
-              -> (Code : Env -> t) -> t
-whileLoop env next with lt 0 (varn env)
-whileLoop env next | false = next env
-whileLoop env next | true =
-     whileLoop (record {varn = (varn env) - 1
-                      ; vari = (vari env) + 1}) next
-
-lt : Nat → Nat → Bool
-```
-
 ## Agda での DataGear
-- **DataGear** は CodeGear の引数
+- **DataGear** は CodeGear でつかわれる引数
 - **データ型**と**レコード型**がある
 - データ型は一つのデータ
 ```AGDA
@@ -82,46 +52,176 @@
     vari : Nat
 ```

-## Agda での証明
-- 関数の型に証明すべき論理式
-- 関数自体にそれを満たす導出
-- 完成した関数は証明
+
+## Agda での Gears の記述(whileTest)
+- Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数
 - **{}** は暗黙的(推論される)
-- 下のコードは Bool型の x と true の and を取ったものは x と等しいことの証明
-  - **refl** は **x == x** の左右の項が等しいことの証明
+- 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す
+- CodeGear の型は**名前 : 引数 → (Code : fa → t) → t**
+- **t** は継続(最終的に返すもの)
+- **(Code : fa → t)** は次の継続先
+```AGDA
+whileTest : {t : Set} → (c10 : Nat)
+            → (Code : Env → t) → t
+whileTest c10 next = next (record {varn = c10
+                                 ; vari = 0} )
+```
+
+## Agda での Gears の記述(whileLoop)
+- 関数の動作を条件で変えたいときはパターンマッチを行う
+- whileLoop は varn が 0 より大きい間ループする
+- **lt** は Nat を２つ受け取って値の大小を比較する関数
+```AGDA
+whileLoop : {t : Set} → Env
+              → (Code : Env → t) → t
+whileLoop env next with lt 0 (varn env)
+whileLoop env next | false = next env
+whileLoop env next | true =
+     whileLoop (record {varn = (varn env) - 1
+                      ; vari = (vari env) + 1}) next
+```
+```AGDA
+lt : Nat → Nat → Bool
+lt x y with (suc x ) ≤? y
+lt x y | yes p = true
+lt x y | no ¬p = false
+```
+
+## Agda での証明
+- 証明の見た目関数と同じ
+- 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出**
+- **refl** は **x == x** で左右の項が等しいことの証明
+- 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明
+- **+zero** は任意の自然数の右から zero を足しても元の数と等しいことの証明
+  - **y = zero** のときは **zero ≡ zero** のため refl
+  - **y = suc y** のときは cong を使い y の数を減らして再帰的に**+zero**を行っている
+  - y の数を減らしても大丈夫なことを cong の関数として受け取った数を suc する関数で保証している
+```AGDA
++zero : { y : Nat } → y + zero ≡ y
++zero {zero} = refl
++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
+```
+
+## Agda での項変換による証明 1/3
+- 次は**x + y ≡ y + x** の証明 **+-sym**
+- 項変換の例として zero, suc y のパターンをみる
+- **zero + suc y**を変換して**suc y + zero**にする
+- begin の下の行に変形したい式を記述
+- **≡⟨  ⟩** に変形規則、その次の行に変換した結果、 **∎** が項変換終了
+- { }0, { }1 は ? で置いたあとコンパイルを通すと Agda が示してくれる
 ```AGDA
-∧true : { x : Bool } →  x  ∧  true  ≡ x
-∧true {x} with x
-∧true {x} | false = refl
-∧true {x} | true = refl
++-sym : { x y : Nat } → x + y ≡ y + x
++-sym {zero} {zero} = refl
++-sym {zero} {suc y} = let open ≡-Reasoning  in
+          begin
+            zero + suc y
+          ≡⟨ { }0 ⟩
+            { }1
+          ∎
+----------------------
+?0 : zero + suc y ≡ suc y + zero
+?1 : Nat
+```
+
+## Agda での証明(項変換) 2/3
+- はじめの変換規則は何も書かずに簡約
+- 次に右から zero を足しても等しくなる証明規則を使いたい
+```AGDA
++-sym {zero} {suc y} = let open ≡-Reasoning  in
+          begin
+            zero + suc y
+          ≡⟨⟩
+            suc y
+          ≡⟨ { }0  ⟩
+            { }1
+          ∎
+----------------------
+?0 : suc y ≡ suc y + zero
+?1 : Nat
+```
+
+## Agda での証明(項変換) 3/3
+- 証明の例で使用した**+zero**は**y + zero ≡ y**
+- これを使いたいが今回は**y + zero ≡ y**
+- Agda の StandartLibrary にある sym を用いて **+zero** を **y + zero ≡ y** として適応することで証明ができる
+```AGDA
+-- +zero : { y : Nat } → y + zero ≡ y
++-sym {zero} {suc y} = let open ≡-Reasoning  in
+          begin
+            zero + suc y
+          ≡⟨⟩
+            suc y
+          ≡⟨ sym +zero  ⟩
+            suc y + zero
+          ∎
+
+sym : Symmetric {A = A} _≡_
+sym refl = refl
+```
+
+## HoareLogicをベースとした Gears での検証手法
+- 今回 HoareLogic で証明する例の疑似コードを用意した
+- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
+- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。
+```C
+   n = 10;
+   i = 0;
+```
+```c
+   while (n>0)
+   {
+     i++;
+     n--;
+   }
+```
+
+## Gears をベースにしたプログラム
+- test は whileTest と whileLoop を使った Gears のプログラム
+- whileTest の継続先にDataGear を受け取って whileLoop に渡す
+  - **(λ 引数 → )**は無名関数で引数を受け取って継続する
+- 説明のため whileTest と whileLoop の型を載せておく
+```AGDA
+test : Env
+test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
+```
+```AGDA
+whileTest : {t : Set} → (c10 : Nat)
+            → (Code : Env → t) → t
+```
+```AGDA
+whileLoop : {t : Set} → Env
+              → (Code : Env → t) → t
 ```

 ## Gears をベースにした HoareLogic と証明(全体)
-- Gears をベースにした while Program で実行できる
-  - これは証明も持っている
-- whileループを任意の回数にするため**c10**は引数
+- proofGears は HoareLogic をベースとした証明
+  - 先程のプログラムと違い、引数として証明も持っている
 - whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい
 ```AGDA
+-- test = whileTest 10 (λ env → whileLoop env (λ env1 → env1))
 proofGears : {c10 :  Nat } → Set
-proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1
-         (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →
+         conversion1 n p1  (λ n1 p2 → whileLoop' n1 p2
+         (λ n2 →  ( vari n2 ≡ c10 ))))
 ```

 ## Gears と HoareLogic をベースにした証明(whileTest)
 - 最初の Command なので PreCondition がない
 - proof2は Post Condition が成り立つことの証明
   - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型
-  - ２つのものを引数に取り、両方が同時に成り立つことを示す
+  - ２つのものを引数に取り、両方が同時に成り立つことを表している
+  - **refl** は **x == x** で左右の項が等しいことの証明
 - Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t**
 ```AGDA
+-- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t
 whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } →
         (Code : (env : Env)  →
             ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-hileTest' {_} {_} {c10} next = next env proof2
+whileTest' {_} {_} {c10} next = next env proof2
   where
     env : Env
     env = record {vari = 0 ; varn = c10}
-    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)      <-- PostCondition
+    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
     proof2 = record {pi1 = refl ; pi2 = refl}
 ```

@@ -137,26 +237,38 @@
 conversion1 env {c10} p1 next = next env proof4
   where
     proof4 : varn env + vari env ≡ c10
-
 ```

-
-##  Agdaでの証明(≡-Reasoning)
-- Agda では証明の項を書き換える構文が用意されている
+##  HoareLogic の証明
+- HoareLogic の証明では基本的に項の書き換えを行って証明している
+- proof4 の証明部分では論理式の**varn env + vari env** を 書き換えて **c10** に変換している
+- 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明
+- 変換後の式を次の行に書いて変換を続ける
 ```AGDA
+-- precond : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+conversion1 env {c10} precond next = next env proof4
+  where
     proof4 : varn env + vari env ≡ c10
     proof4 = let open ≡-Reasoning  in
       begin
         varn env + vari env
-      ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
+      ≡⟨ cong ( λ n → n + vari env ) (pi2 precond ) ⟩
         c10 + vari env
-      ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
+      ≡⟨ cong ( λ n → c10 + n ) (pi1 precond ) ⟩
         c10 + 0
       ≡⟨ +-sym {c10} {0} ⟩
         c10
       ∎
+--  +-sym : { x y : Nat } → x + y ≡ y + x
 ```

+## Gears と HoareLogic をベースにした証明(whileLoop)
+- whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている
+```AGDA
+-- whileLoop : {t : Set} → Env → (Code : Env → t) → t
+whileLoop' : {t : Set} → (env : Env) → {c10 :  Nat } → ((varn env) + (vari env) ≡ c10) → (Code : Env → t) → t
+```
+
 ## Gears と HoareLogic をベースにした証明(全体)
 - 最終状態で返ってくる i の値は c10 と一致する
 - これにより証明が可能
@@ -167,209 +279,11 @@
 ```

 ## まとめと今後の課題
-- HoareLogic の while を使った例題を作成、証明を行った
 - Gears を用いた HoareLogic ベースの検証方法を導入した
   - 証明が引数として渡される記述のため証明とプログラムを一体化できた
 - 今後の課題
   - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)

-
-## Agda 上での HoareLogic
-* Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと
-それを Agda2 に書き写したものが存在している。
-* 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて Agda2上で HoareLogic を構築する
-
-## HoareLogic とは
-* Floyd-Hoare Logic (以下HoareLogic)は部分的な正当性を検証する
-* プログラムは事前条件(Pre Condition)、事後条件(Post Condition)を持ち、条件がコマンドで更新され、事後条件になる
-* 事前、事後条件には変数や論理式、コマンドには代入や、繰り返し、条件分岐などがある。
-* コマンドが正しく成り立つことを保証することで、このコマンドを用いて記述されたプログラムの部分的な正しさを検証できる
-
-## HoareLogic の理解
-- HoareLogic 例として疑似コードを用意した
-- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
-- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。
-- 次のスライドから Agda 上 HoareLogic を実装し、その上でこの whileProgram の検証を行う
-```C
-   n = 10;
-   i = 0;
-
-   while (n>0)
-   {
-     i++;
-     n--;
-   }
-```
-
-## Agda 上での HoareLogic(条件、変数の定義)
-- **Env** は while Program で必要な変数をまとめたもの
- - varn、vari はそれぞれ変数 n、 i
-- **Cond** は Pre、Post の Condition で Env を受け取って Bool 値(true か false)を返す
-```AGDA
-   record Env : Set where
-     field
-       varn : Nat
-       vari : Nat
-
-   Cond : Set
-   Cond = (Env → Bool)
-```
-
-## Agda 上での HoareLogic(コマンド定義)
-* **Comm** は Agda のデータ型で定義した HoareLogic のコマンド
-  * **PComm** は変数を代入のコマンド
-  * **Seq** はコマンドの推移、 Command を実行して次の Command に移す
-  * **If** は条件分岐のコマンド
-  * **while** は繰り返しのコマンド
-* 他にも何もしないコマンドやコマンドの停止などのコマンドもある
-- **PrimComm** は Env を受け取って Env を返す定義
-```AGDA
-     data Comm : Set where
-       PComm : PrimComm → Comm
-       Seq   : Comm → Comm → Comm
-       If    : Cond → Comm → Comm → Comm
-       While : Cond → Comm → Comm
-
-     PrimComm : Set
-     PrimComm = Env → Env
-```
-
-## Agda 上での HoareLogic(実際のプログラムの記述)
-* 先程定義したコマンドを使って while Program を記述した
-  - 任意の自然数を引数に取る形になっているが**c10 == 10**ということにする
-* **$** は **()** の糖衣で行頭から行末までを ( ) で囲う
-* 見やすさのため改行しているが 3~7 行は1行
-```AGDA
-   program : ℕ → Comm
-   program c10 =
-      Seq ( PComm (λ env → record env {varn = c10}))                -- n = 10;
-      $ Seq ( PComm (λ env → record env {vari = 0}))                -- i = 0;
-      $ While (λ env → lt zero (varn env ) )                         -- while (n>0) {
-        (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++;
-          $ PComm (λ env → record env {varn = ((varn env) - 1)} ))   -- n--;
-```
-
-## Agda 上での HoareLogic(コマンドの保証)1/3
-* 保証の規則は HTProof にまとめられてる
-* **PrimRule** は **PComm** で行う代入を保証する
-* 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述
-  * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す
-```AGDA
-   data HTProof : Cond → Comm → Cond → Set where
-     PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} →
-                  (pr : Axiom bPre pcm bPost) →
-                  HTProof bPre (PComm pcm) bPost
--- 次のスライドに続く
-```
-```AGDA
-   Axiom : Cond → PrimComm → Cond → Set
-   Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
-```
+## 発表終了
+- ご清聴ありがとうございました。

-## Agda 上での HoareLogic(コマンド保証)2/3
-* **SeqRule** は Command を推移させる Seq の保証
-* **IfRule** は If の Command が正しく動くことを保証
-```AGDA
--- HTProof の続き
-     SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} →
-             {cm2 : Comm} → {bPost : Cond} →
-             HTProof bPre cm1 bMid →
-             HTProof bMid cm2 bPost →
-             HTProof bPre (Seq cm1 cm2) bPost
-     IfRule : {cmThen : Comm} → {cmElse : Comm} →
-            {bPre : Cond} → {bPost : Cond} →
-            {b : Cond} →
-            HTProof (bPre /\ b) cmThen bPost →
-            HTProof (bPre /\ neg b) cmElse bPost →
-            HTProof bPre (If b cmThen cmElse) bPost
-```
-
-## Agda 上での HoareLogic(コマンド保証)3/3
-* **WeakeningRule** は通常の Condition からループ不変条件(Loop Invaliant)に変換
-* Tautology は Condition と不変条件が等しく成り立つ
-* **WhileRule** はループ不変条件が成り立つ間 Comm を繰り返す
-```AGDA
--- HTProof の続き
-     WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} →
-                 {bPost' : Cond} → {bPost : Cond} →
-                 Tautology bPre bPre' →
-                 HTProof bPre' cm bPost' →
-                 Tautology bPost' bPost →
-                 HTProof bPre cm bPost
-     WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} →
-                 HTProof (bInv /\ b) cm bInv →
-                 HTProof bInv (While b cm) (bInv /\ neg b)
-```
-```AGDA
-   Tautology : Cond → Cond → Set
-   Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true
-```
-
-
-## Agda 上での HoareLogic(証明)
-- **proof1** は while Program の証明
-- HTProof に 初期状態と先程コマンドで記述した whileProgram である **program** と終了状態を渡す
-- Condititon は initCond や termCond のようにそれぞれ定義する必要がある
-- program に近い形で証明を記述できる
-```AGDA
-   proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
-   proof1 c10 =
-         SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
-         $ SeqRule {λ e →  Equal (varn e) c10} ( PrimRule lemma1   )
-         $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)}  lemma2 (
-            WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
-            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
-               $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
-
-   initCond : Cond
-   initCond env = true
-
-   termCond : {c10 : Nat} → Cond
-   termCond {c10} env = Equal (vari env) c10
-```
-<!-- * lemma1~5は rule それぞれの証明 -->
-  <!-- program : Comm -->
-  <!-- program =  -->
-  <!--   Seq ( PComm (λ env → record env {varn = 10})) -->
-  <!--   $ Seq ( PComm (λ env → record env {vari = 0})) -->
-  <!--   $ While (λ env → lt zero (varn env ) ) -->
-  <!--     (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -->
-  <!--       $ PComm (λ env → record env {varn = ((varn env) - 1)} )) -->
-
-## 証明の一部(lemma1)
-- PComm の証明である lemma1 だけ解説
-- lemma1 は n に 10 を代入したあと、 i に 0 を代入するところ
-- 証明することは**事前条件の n ≡ 10 が成り立つか**
-- PreCondition が成り立つとき、Command を実行するとPostConditionが成り立つ
-  - Axiom は x ⇒ y  ≡ true が成り立てば良かった
-  - **_⇒_** は事後条件が成り立つかどうか
-  - impl⇒ は x ≡ true → y ≡ true の関数(Command)を受け取って x ⇒ y  ≡ true を返す関数
-- **≡-Reasoning** は Agda での等式変形
-```AGDA
-    lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10})
-           (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
-    lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
-      begin
-        (Equal (varn env) c10 ) ∧ true
-      ≡⟨ ∧true ⟩
-        Equal (varn env) c10
-      ≡⟨ cond ⟩
-        true
-      ∎ )
-
-    stmt1Cond : {c10 : ℕ} → Cond
-    stmt1Cond {c10} env = Equal (varn env) c10
-
-    stmt2Cond : {c10 : ℕ} → Cond
-    stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
-```
-
-
-    <!-- lemma2 :  {c10 : Nat} → Tautology stmt2Cond whileInv -->
-
-    <!-- lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' -->
-
-    <!-- lemma4 :  {c10 : Nat} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv -->
-
-    <!-- lemma5 : {c10 : Nat} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond  -->
-