Mercurial > hg > Papers > 2019 > ryokka-sigss

changeset 12:e8fe28afe61e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix slide
author ryokka
date Tue, 15 Jan 2019 15:56:33 +0900
parents 17b7605a5deb
children fde9ee0cc8ae
files slide/Makefile slide/slide.html slide/slide.md
diffstat 3 files changed, 649 insertions(+), 480 deletions(-) [+]
line wrap: on
line diff
--- a/slide/Makefile	Sun Jan 13 23:42:16 2019 +0900
+++ b/slide/Makefile	Tue Jan 15 15:56:33 2019 +0900
@@ -6,11 +6,11 @@
 	slideshow b $< -t s6cr --h2
 
 all: $(TARGET).html
-
 	open $(TARGET).html -a Google\ Chrome
-
 clean:
 	rm -f *.html
 
 
 	# ls -lt ~/cr/lab-slides/slides/* | head -1 | awk -F ':' '{ print $1 }' | xargs -I slide_dir slideshow build slide_dir"/slide.md" --h2
+    # 
+# open /Applications/Google\ Chrome.app --args --app=$(TARGET).html	
--- a/slide/slide.html	Sun Jan 13 23:42:16 2019 +0900
+++ b/slide/slide.html	Tue Jan 15 15:56:33 2019 +0900
@@ -7,7 +7,7 @@
 <html>
 <head>
    <meta http-equiv="content-type" content="text/html;charset=utf-8">
-   <title>GearsOS の Hoare triple を用いた検証</title>
+   <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" >
@@ -70,7 +70,7 @@
       <tr>
         <td>
           <div align="center">
-              <h1><font color="#808db5">GearsOS の Hoare triple を用いた検証</font></h1>
+              <h1><font color="#808db5">GearsOS の Hoare Logic を用いた検証</font></h1>
           </div>
         </td>
       </tr>
@@ -99,10 +99,10 @@
   <li>信頼性を上げるために仕様を検証する必要</li>
   <li>仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある
     <ul>
-      <li>事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす</li>
+      <li>事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす</li>
     </ul>
   </li>
-  <li>既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい…?)</li>
+  <li>既存の言語ではあまり利用されていない</li>
 </ul>
 
 
@@ -114,17 +114,13 @@
 <h2 id="背景">背景</h2>
 <ul>
   <li>当研究室では 処理の単位を <strong>CodeGear</strong>、データの単位を <strong>DataGear</strong> としてプログラムを記述する手法を提案</li>
-  <li>CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む</li>
-  <li>Gear 間の接続処理はメタ計算として定義
-    <ul>
-      <li>メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証</li>
-    </ul>
-  </li>
-  <li>本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する</li>
+  <li>CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
+<!-- - Gear 間の接続処理はメタ計算として定義 -->
+<!--   - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証 --></li>
+  <li>この単位を用いて信頼性の高い OS として GearsOS を開発している</li>
+  <li>本発表では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する</li>
 </ul>
 
-<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt="" width="75%" height="75%" /></p>
-
 
 
 </div>
@@ -144,9 +140,9 @@
     </ul>
   </li>
 </ul>
-
+<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt="" width="75%" height="75%" /></p>
 <!-- ![cgdg](./pic/codeGear_dataGear.pdf){} -->
-<p style="text-align:center;"><img src="./pic/cgdg.svg" alt="" width="30%" height="30%" /></p>
+<!-- <p style="text-align:center;"><img src="./pic/cgdg.svg" alt=""  width="30%" height="30%"/></p> -->
 
 
 
@@ -156,10 +152,14 @@
   <!-- _S9SLIDE_ -->
 <h2 id="cbc-について">CbC について</h2>
 <ul>
-  <li>Gears の単位でプログラミングできる言語として CbC (Continuation based C) が存在</li>
-  <li>現在の CbC では assert での検証ができる</li>
+  <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>
+  <li>そのため Gears の単位を定理証明支援系の言語である <strong>Agda</strong> で記述し、 Agda で証明している</li>
 </ul>
 
 
@@ -168,7 +168,7 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda">Agda</h2>
+<h2 id="agda-とは">Agda とは</h2>
 <ul>
   <li>Agda は定理証明支援系の言語</li>
   <li>依存型を持つ関数型言語</li>
@@ -185,22 +185,21 @@
 <h2 id="agda-のデータ型">Agda のデータ型</h2>
 <ul>
   <li>データ型は代数的なデータ構造</li>
-  <li><strong>data</strong> キーワードの後に、<strong>名前 : 型</strong>、 where 句</li>
+  <li><strong>data</strong> キーワードの後に、<strong>名前 : 型</strong></li>
   <li>次の行以降は<strong>コンストラクタ名 : 型</strong></li>
-  <li>型は<strong>-&gt;</strong>または<strong>→</strong>で繋げる</li>
-  <li>例えば、型<strong>PrimComm -&gt; Comm</strong>は<strong>PrimComm</strong> を受け取り<strong>Comm</strong>を返す型</li>
-  <li>再帰的な定義も可能
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  data Comm : Set where
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    Skip : Comm
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    Abort : Comm
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>    PComm : PrimComm -&gt; Comm
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>    Seq : Comm -&gt; Comm -&gt; Comm
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>    If : Cond -&gt; Comm -&gt; Comm -&gt; Comm 
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>    While : Cond -&gt; Comm -&gt; Comm
+  <li>型は<strong>-&gt;</strong>または<strong>→</strong>で繋げる
+    <ul>
+      <li>例えば、suc の型<strong>Nat → Nat*は</strong>Nat** を受け取り<strong>Nat</strong>を返す型</li>
+      <li>これにより 3 を suc (suc (suc zero)) のように表せる
+        <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Nat : Set where
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>   zero : Nat
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>   suc  : Nat → Nat
 </pre></div>
 </div>
-    </div>
+        </div>
+      </li>
+    </ul>
   </li>
 </ul>
 
@@ -217,15 +216,70 @@
   <li>C 言語での構造体に近い</li>
   <li>複数のデータをまとめる</li>
   <li>関数内で構築できる</li>
-  <li>構築時は<strong>レコード名 {フィールド名 = 値}</strong></li>
-  <li>複数ある場合は <strong>{フィールド1 = 1 ; フィールド2 = 2}</strong>のように <strong>;</strong> を使って列挙
+  <li>構築時は<strong>record レコード名 {フィールド名 = 値}</strong></li>
+  <li>複数ある場合は <strong>record Env {varn = 1 ; varn = 2}</strong>のように <strong>;</strong> を使って列挙
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record Env : Set where 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>   field
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>     varn : Nat
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>     vari : Nat
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="agda-の関数">Agda の関数</h2>
+<ul>
+  <li>関数にも型が必要(1行目)
     <ul>
-      <li>(varn,vari の型 <strong>ℕ</strong> は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -&gt; ℕ で定義されてる)
+      <li>引き算はは自然数を２つ取って結果の自然数を返す</li>
+      <li><strong>_</strong> は任意の値、名前で使うと受け取った引数が順番に入る</li>
+    </ul>
+  </li>
+  <li>関数本体は <strong>関数名 = 値</strong></li>
+  <li>関数ではパターンマッチがかける
+    <ul>
+      <li>ここでは関数名に <strong>_</strong> を使っているため<strong>Nat</strong>の定義にから zero かそれ以外でパターンマッチ
         <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>record Env : Set where 
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  field
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    varn : ℕ
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>    vari : ℕ
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> _-_ : Nat → Nat → Nat 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span> x - zero  = x
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span> zero - _  = zero
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span> (suc x) - (suc y)  = x - y
+</pre></div>
+</div>
+        </div>
+      </li>
+    </ul>
+  </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 と等しいことの証明
+    <ul>
+      <li><strong>refl</strong> は <strong>x == x</strong> の左右の項が等しいことの証明
+        <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> ∧true : { x : Bool } →  x  ∧  true  ≡ x
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span> ∧true {x} with x
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span> ∧true {x} | false = refl
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ∧true {x} | true = refl
 </pre></div>
 </div>
         </div>
@@ -240,17 +294,48 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-の関数">Agda の関数</h2>
+<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>関数にも型が必要</li>
-  <li>関数は <strong>関数名 = 値</strong></li>
-  <li>関数ではパターンマッチがかける</li>
-  <li><strong>_</strong> は任意の引数
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  _-_ : ℕ → ℕ → ℕ 
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  x - zero  = x
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  zero - _  = zero
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  (suc x) - (suc y)  = x - y
+  <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><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>;
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>;
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n&gt;<span style="color:#00D">0</span>)
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span> {
+<span class="line-numbers"><a href="#n6" name="n6">6</a></span>   i++;
+<span class="line-numbers"><a href="#n7" name="n7">7</a></span>   n--;
+<span class="line-numbers"><a href="#n8" name="n8">8</a></span> }
 </pre></div>
 </div>
     </div>
@@ -263,17 +348,19 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-での証明">Agda での証明</h2>
+<h2 id="agda-上での-hoarelogic条件変数の定義">Agda 上での HoareLogic(条件、変数の定義)</h2>
 <ul>
-  <li>関数の型に論理式</li>
-  <li>関数自体にそれを満たす導出</li>
-  <li>完成した関数は証明</li>
-  <li><strong>{}</strong> は暗黙的(推論される)</li>
-  <li>下のコードは自然数に 0 を足したとき値が変わらないことの証明
+  <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><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  +zero : { y : ℕ } → y + zero  ≡ y
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  +zero {zero} = refl
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record Env : Set where
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>   field
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>     varn : Nat
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>     vari : Nat
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>
+<span class="line-numbers"><a href="#n6" name="n6">6</a></span> Cond : Set
+<span class="line-numbers"><a href="#n7" name="n7">7</a></span> Cond = (Env → Bool) 
 </pre></div>
 </div>
     </div>
@@ -286,75 +373,27 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogic">Agda 上での HoareLogic</h2>
-<ul>
-  <li>現在 Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと
-それを Agda2 に書き写したものが存在している。</li>
-  <li>今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて説明を行う。</li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-での-hoarelogic-の理解">Agda での HoareLogic の理解</h2>
-<ul>
-  <li>HoareLogic を用いて次のようなプログラム(while Program)を検証した。
-    <div class="language-C highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  n = <span style="color:#00D">10</span>;
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  i = <span style="color:#00D">0</span>;
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  <span style="color:#080;font-weight:bold">while</span> (n&gt;<span style="color:#00D">0</span>)
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>  {
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>    i++;
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>    n--;
-<span class="line-numbers"><a href="#n8" name="n8">8</a></span>  }
-</pre></div>
-</div>
-    </div>
-  </li>
-  <li>このプログラムは変数iとnをもち、 n&gt;0 の間nの値を減らし、i の値を増やす</li>
-  <li>n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。</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="agda-上での-hoarelogicコマンド定義">Agda 上での HoareLogic(コマンド定義)</h2>
 <ul>
-  <li>Env は while Program の変数である var n, i</li>
-  <li><strong>PrimComm</strong> は代入時に使用される</li>
-  <li><strong>Cond</strong> は Condition で Env を受け取って Boolean の値を返す
+  <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><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>  record Env : Set where
-<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>    field
-<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>      varn : ℕ
-<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>      vari : ℕ
-<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>
-<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>  PrimComm : Set
-<span class="line-numbers"> <a href="#n7" name="n7">7</a></span>  PrimComm = Env → Env
-<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>
-<span class="line-numbers"> <a href="#n9" name="n9">9</a></span>  Cond : Set
-<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>  Cond = (Env → Bool) 
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>   data Comm : Set where
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>     PComm : PrimComm → Comm
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>     Seq   : Comm → Comm → Comm
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>     If    : Cond → Comm → Comm → Comm
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>     While : Cond → Comm → Comm
+<span class="line-numbers"><a href="#n6" name="n6">6</a></span>       
+<span class="line-numbers"><a href="#n7" name="n7">7</a></span>   PrimComm : Set
+<span class="line-numbers"><a href="#n8" name="n8">8</a></span>   PrimComm = Env → Env
 </pre></div>
 </div>
     </div>
@@ -367,23 +406,54 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogicコマンド定義-1">Agda 上での HoareLogic(コマンド定義)</h2>
+<h2 id="agda-上での-hoarelogic実際のプログラムの記述">Agda 上での HoareLogic(実際のプログラムの記述)</h2>
 <ul>
-  <li><strong>Comm</strong> は Agda のデータ型で定義した HoareLogic の Command
+  <li>先程定義したコマンドを使って while Program を記述した
     <ul>
-      <li><strong>Skip</strong> は何も変更しない</li>
-      <li><strong>PComm</strong> は変数を代入する</li>
-      <li><strong>Seq</strong> は Command を実行して次の Command に移す</li>
-      <li><strong>If</strong> は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える</li>
-      <li><strong>while</strong> は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す
+      <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><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : ℕ → Comm
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span> program c10 = 
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    Seq ( PComm (λ env → record env {varn = c10}))                -- n = 10;
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>    $ Seq ( PComm (λ env → record env {vari = 0}))                -- i = 0;
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>    $ While (λ env → lt zero (varn env ) )                         -- while (n&gt;0) {
+<span class="line-numbers"><a href="#n6" name="n6">6</a></span>      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++;
+<span class="line-numbers"><a href="#n7" name="n7">7</a></span>        $ 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>
+<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><span class="line-numbers"><a href="#n1" name="n1">1</a></span>data Comm : Set where
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  Skip  : Comm
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  Abort : Comm
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>  PComm : PrimComm -&gt; Comm
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>  Seq   : Comm -&gt; Comm -&gt; Comm
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>  If    : Cond -&gt; Comm -&gt; Comm -&gt; Comm
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>  While : Cond -&gt; Comm -&gt; Comm
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data HTProof : Cond → Comm → Cond → Set where
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span> PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} →
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>              (pr : Axiom bPre pcm bPost) →
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>              HTProof bPre (PComm pcm) bPost
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>-- 次のスライドに続く
+</pre></div>
+</div>
+        </div>
+        <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> Axiom : Cond → PrimComm → Cond → Set
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
 </pre></div>
 </div>
         </div>
@@ -398,23 +468,23 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogic実際のプログラムの記述">Agda 上での HoareLogic(実際のプログラムの記述)</h2>
+<h2 id="agda-上での-hoarelogicコマンド保証23">Agda 上での HoareLogic(コマンド保証)2/3</h2>
 <ul>
-  <li>Command を使って while Program を記述した。</li>
-  <li><strong>$</strong> は <strong>()</strong> の糖衣で行頭から行末までを ( ) で囲う
-    <ul>
-      <li>見やすさのため改行しているため 3~7 行はまとまっている</li>
-    </ul>
-  </li>
-  <li>Seq は Comm を2つ取って次の Comm に移行する
+  <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><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  program : Comm
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  program = 
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>    Seq ( PComm (λ env → record env {varn = 10}))
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>    $ Seq ( PComm (λ env → record env {vari = 0}))
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>    $ While (λ env → lt zero (varn env ) )
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
+  <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- HTProof の続き
+<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>   SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} →
+<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>           {cm2 : Comm} → {bPost : Cond} →
+<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>           HTProof bPre cm1 bMid →
+<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>           HTProof bMid cm2 bPost →
+<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>           HTProof bPre (Seq cm1 cm2) bPost
+<span class="line-numbers"> <a href="#n7" name="n7">7</a></span>   IfRule : {cmThen : Comm} → {cmElse : Comm} →
+<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>          {bPre : Cond} → {bPost : Cond} →
+<span class="line-numbers"> <a href="#n9" name="n9">9</a></span>          {b : Cond} →
+<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>          HTProof (bPre /\ b) cmThen bPost →
+<span class="line-numbers"><a href="#n11" name="n11">11</a></span>          HTProof (bPre /\ neg b) cmElse bPost →
+<span class="line-numbers"><a href="#n12" name="n12">12</a></span>          HTProof bPre (If b cmThen cmElse) bPost
 </pre></div>
 </div>
     </div>
@@ -427,95 +497,28 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogicの理解">Agda 上での HoareLogicの理解</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 を返す関数</li>
-    </ul>
-  </li>
-  <li>SkipRule は PreCondition を変更しないことの保証</li>
-  <li>AbortRule は プログラムが停止するときのルール
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  data HTProof : Cond -&gt; Comm -&gt; Cond -&gt; Set where
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>    PrimRule : {bPre : Cond} -&gt; {pcm : PrimComm} -&gt; {bPost : Cond} -&gt;
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>                 (pr : Axiom bPre pcm bPost) -&gt;
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>                 HTProof bPre (PComm pcm) bPost
-<span class="line-numbers"><a href="#n5" name="n5">5</a></span>    SkipRule : (b : Cond) -&gt; HTProof b Skip b
-<span class="line-numbers"><a href="#n6" name="n6">6</a></span>    AbortRule : (bPre : Cond) -&gt; (bPost : Cond) -&gt;
-<span class="line-numbers"><a href="#n7" name="n7">7</a></span>                 HTProof bPre Abort bPost
-<span class="line-numbers"><a href="#n8" name="n8">8</a></span>-- 次のスライドに続く
-</pre></div>
-</div>
-    </div>
-    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  Axiom : Cond -&gt; PrimComm -&gt; Cond -&gt; Set
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogicの理解-1">Agda 上での HoareLogicの理解</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><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- HTProof の続き
-<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>    SeqRule : {bPre : Cond} -&gt; {cm1 : Comm} -&gt; {bMid : Cond} -&gt;
-<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>            {cm2 : Comm} -&gt; {bPost : Cond} -&gt;
-<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>            HTProof bPre cm1 bMid -&gt;
-<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>            HTProof bMid cm2 bPost -&gt;
-<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>            HTProof bPre (Seq cm1 cm2) bPost
-<span class="line-numbers"> <a href="#n7" name="n7">7</a></span>    IfRule : {cmThen : Comm} -&gt; {cmElse : Comm} -&gt;
-<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>           {bPre : Cond} -&gt; {bPost : Cond} -&gt;
-<span class="line-numbers"> <a href="#n9" name="n9">9</a></span>           {b : Cond} -&gt;
-<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>           HTProof (bPre /\ b) cmThen bPost -&gt;
-<span class="line-numbers"><a href="#n11" name="n11">11</a></span>           HTProof (bPre /\ neg b) cmElse bPost -&gt;
-<span class="line-numbers"><a href="#n12" name="n12">12</a></span>           HTProof bPre (If b cmThen cmElse) bPost
-</pre></div>
-</div>
-    </div>
-  </li>
-</ul>
-
-
-
-</div>
-
-<div class='slide'>
-  <!-- _S9SLIDE_ -->
-<h2 id="agda-上での-hoarelogicの理解-2">Agda 上での HoareLogicの理解</h2>
+<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><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- HTProof の続き
-<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>    WeakeningRule : {bPre : Cond} -&gt; {bPre' : Cond} -&gt; {cm : Comm} -&gt;
-<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>                {bPost' : Cond} -&gt; {bPost : Cond} -&gt;
-<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>                Tautology bPre bPre' -&gt;
-<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>                HTProof bPre' cm bPost' -&gt;
-<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>                Tautology bPost' bPost -&gt;
-<span class="line-numbers"> <a href="#n7" name="n7">7</a></span>                HTProof bPre cm bPost
-<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>    WhileRule : {cm : Comm} -&gt; {bInv : Cond} -&gt; {b : Cond} -&gt;
-<span class="line-numbers"> <a href="#n9" name="n9">9</a></span>                HTProof (bInv /\ b) cm bInv -&gt;
-<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>                HTProof bInv (While b cm) (bInv /\ neg b)
+<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>   WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} →
+<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>               {bPost' : Cond} → {bPost : Cond} →
+<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>               Tautology bPre bPre' →
+<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>               HTProof bPre' cm bPost' →
+<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>               Tautology bPost' bPost →
+<span class="line-numbers"> <a href="#n7" name="n7">7</a></span>               HTProof bPre cm bPost
+<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>   WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} →
+<span class="line-numbers"> <a href="#n9" name="n9">9</a></span>               HTProof (bInv /\ b) cm bInv →
+<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>               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><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  Tautology : Cond -&gt; Cond -&gt; Set
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> Tautology : Cond → Cond → Set
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true
 </pre></div>
 </div>
     </div>
@@ -531,70 +534,85 @@
 <h2 id="agda-上での-hoarelogic証明">Agda 上での HoareLogic(証明)</h2>
 <ul>
   <li><strong>proof1</strong> は while Program の証明</li>
-  <li>HTProof に 初期状態とコマンドで書かれた <strong>program</strong>  と終了状態を渡す</li>
-  <li>lemma1~5は rule それぞれの証明</li>
-  <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><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>proof1 : HTProof initCond program termCond
-<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>proof1 =
-<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>    SeqRule {λ e → true} ( PrimRule empty-case )
-<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>      $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
-<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>      $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
-<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>          WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
+  <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
+<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> proof1 c10 =
+<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>       SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
+<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>       $ SeqRule {λ e →  Equal (varn e) c10} ( PrimRule lemma1   )
+<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>       $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)}  lemma2 (
+<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>          WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
 <span class="line-numbers"> <a href="#n7" name="n7">7</a></span>          $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
-<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>                 $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
+<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>             $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
 <span class="line-numbers"> <a href="#n9" name="n9">9</a></span>
-<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>initCond : Cond
-<span class="line-numbers"><a href="#n11" name="n11">11</a></span>initCond env = true
+<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> initCond : Cond
+<span class="line-numbers"><a href="#n11" name="n11">11</a></span> initCond env = true
 <span class="line-numbers"><a href="#n12" name="n12">12</a></span>
-<span class="line-numbers"><a href="#n13" name="n13">13</a></span>termCond : {c10 : ℕ} → Cond
-<span class="line-numbers"><a href="#n14" name="n14">14</a></span>termCond {c10} env = Equal (vari env) c10
+<span class="line-numbers"><a href="#n13" name="n13">13</a></span> termCond : {c10 : Nat} → Cond
+<span class="line-numbers"><a href="#n14" name="n14">14</a></span> 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>
 
-<p><!-- 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)} )) --></p>
-
 
 
 </div>
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="証明の一部">証明の一部</h2>
+<h2 id="証明の一部lemma1">証明の一部(lemma1)</h2>
 <ul>
-  <li>型だけ載せる</li>
-  <li>基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する</li>
-  <li>impl⇒
+  <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><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>  lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
-<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>  lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
-<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>    begin
-<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>      (Equal (varn env) c10 ) ∧ true
-<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>    ≡⟨ ∧true ⟩
-<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>      Equal (varn env) c10 
-<span class="line-numbers"> <a href="#n7" name="n7">7</a></span>    ≡⟨ cond ⟩
-<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>      true
-<span class="line-numbers"> <a href="#n9" name="n9">9</a></span>    ∎ )
+  <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>  lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10}) 
+<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>         (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>  lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
+<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>    begin
+<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>      (Equal (varn env) c10 ) ∧ true
+<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>    ≡⟨ ∧true ⟩
+<span class="line-numbers"> <a href="#n7" name="n7">7</a></span>      Equal (varn env) c10 
+<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>    ≡⟨ cond ⟩
+<span class="line-numbers"> <a href="#n9" name="n9">9</a></span>      true
+<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>    ∎ )
+<span class="line-numbers"><a href="#n11" name="n11">11</a></span>      
+<span class="line-numbers"><a href="#n12" name="n12">12</a></span>  stmt1Cond : {c10 : ℕ} → Cond
+<span class="line-numbers"><a href="#n13" name="n13">13</a></span>  stmt1Cond {c10} env = Equal (varn env) c10
+<span class="line-numbers"><a href="#n14" name="n14">14</a></span>   
+<span class="line-numbers"><a href="#n15" name="n15">15</a></span>  stmt2Cond : {c10 : ℕ} → Cond
+<span class="line-numbers"><a href="#n16" name="n16">16</a></span>  stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
 </pre></div>
 </div>
     </div>
 
-    <p><!-- lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv --></p>
+    <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 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv --></p>
+    <p><!-- lemma4 :  {c10 : Nat} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv --></p>
 
-    <p><!-- lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond  --></p>
+    <p><!-- lemma5 : {c10 : Nat} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond  --></p>
   </li>
 </ul>
 
@@ -608,15 +626,40 @@
 <ul>
   <li>Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数</li>
   <li>CPS の関数は引数として継続を受け取って継続に計算結果を渡す</li>
-  <li><strong>名前 : 引数 -&gt; (Code : fa -&gt; t) -&gt; t</strong></li>
+  <li><strong>名前 : 引数 → (Code : fa → t) → t</strong></li>
   <li><strong>t</strong> は継続</li>
-  <li><strong>(Code : fa -&gt; t)</strong> は次の継続先</li>
+  <li><strong>(Code : fa → t)</strong> は次の継続先</li>
   <li>DataGear は Agda での CodeGear に使われる引数
     <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>_g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>x g- zero next = next x
-<span class="line-numbers"><a href="#n3" name="n3">3</a></span>zero g- _  = next zero
-<span class="line-numbers"><a href="#n4" name="n4">4</a></span>(suc x) g- (suc y)  = next (x g- y)
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>_-_ : {t : Set} → Nat → Nat → (Code : Nat → t) → t
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>x - zero = (λ next → next x)
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>zero - _ = (λ next → next zero)
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>(suc x) - (suc y) = (x - y)
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gears-をベースにした-hoarelogic-と証明全体">Gears をベースにした HoareLogic と証明(全体)</h2>
+<ul>
+  <li>Gears をベースにした while Program
+    <ul>
+      <li>これは証明でもある</li>
+    </ul>
+  </li>
+  <li>whileループを任意の回数にするため<strong>c10</strong>は引数</li>
+  <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  proofGears : {c10 :  Nat } → Set
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>                 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 </pre></div>
 </div>
     </div>
@@ -629,13 +672,81 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gears-をベースにした-hoarelogic">Gears をベースにした HoareLogic</h2>
+<h2 id="gears-と-hoarelogic-をベースにした証明whiletest">Gears と HoareLogic をベースにした証明(whileTest)</h2>
+<ul>
+  <li>ここは代入する Command</li>
+  <li>最初の Command なので PreCondition がない</li>
+  <li>もとの whileProgram では PComm を2回していたがまとめた</li>
+  <li>proof2は Post Condition が成り立つことの証明
+    <ul>
+      <li><strong><em>/\</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li>
+      <li>２つのものを引数に取り、両方が同時に成り立つことを示す</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><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } → 
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>              (Code : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+<span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileTest' {_} {_} {c10} next = next env proof2
+<span class="line-numbers"><a href="#n4" name="n4">4</a></span>    where
+<span class="line-numbers"><a href="#n5" name="n5">5</a></span>      env : Env
+<span class="line-numbers"><a href="#n6" name="n6">6</a></span>      env = record {vari = 0 ; varn = c10}
+<span class="line-numbers"><a href="#n7" name="n7">7</a></span>      proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)      &lt;-- PostCondition
+<span class="line-numbers"><a href="#n8" name="n8">8</a></span>      proof2 = record {pi1 = refl ; pi2 = refl}
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gears-と-hoarelogic-をベースにした証明conversion">Gears と HoareLogic をベースにした証明(conversion)</h2>
 <ul>
-  <li>次に Gears をベースにした while Program をみる。</li>
-  <li>このプログラムは自然数と継続先を受け取って t を返す
+  <li>conversion は Condition から LoopInvaliant への変換を行う CodeGear</li>
+  <li>proof4 は LoopInvaliant の証明</li>
+  <li>Gears での HoareLogic の完全な記述は <strong>引数 → PreCondition → (Code : fa → PostCondition → t) → t</strong>
+    <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
+  <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>  conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  Nat } → 
+<span class="line-numbers"> <a href="#n2" name="n2">2</a></span>                     ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+<span class="line-numbers"> <a href="#n3" name="n3">3</a></span>                     → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
+<span class="line-numbers"> <a href="#n4" name="n4">4</a></span>  conversion1 env {c10} p1 next = next env proof4
+<span class="line-numbers"> <a href="#n5" name="n5">5</a></span>    where
+<span class="line-numbers"> <a href="#n6" name="n6">6</a></span>      proof4 : varn env + vari env ≡ c10
+<span class="line-numbers"> <a href="#n7" name="n7">7</a></span>      proof4 = let open ≡-Reasoning  in
+<span class="line-numbers"> <a href="#n8" name="n8">8</a></span>        begin
+<span class="line-numbers"> <a href="#n9" name="n9">9</a></span>          varn env + vari env
+<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span>        ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
+<span class="line-numbers"><a href="#n11" name="n11">11</a></span>          c10 + vari env
+<span class="line-numbers"><a href="#n12" name="n12">12</a></span>        ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
+<span class="line-numbers"><a href="#n13" name="n13">13</a></span>          c10 + 0
+<span class="line-numbers"><a href="#n14" name="n14">14</a></span>        ≡⟨ +-sym {c10} {0} ⟩
+<span class="line-numbers"><a href="#n15" name="n15">15</a></span>          c10
+<span class="line-numbers"><a href="#n16" name="n16">16</a></span>        ∎
+</pre></div>
+</div>
+    </div>
+  </li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gears-と-hoarelogic-をベースにした証明whileloop">Gears と HoareLogic をベースにした証明(whileLoop)</h2>
+<ul>
+  <li>whileLoop は loopInvaliant が true の間 WhileLoop を回し続けるCodeGear</li>
+  <li>この CodeGear は Agda がループが終わることが証明できてないため <strong>{-# TERMINATING #-}</strong> で明示</li>
+  <li>false になると次の CodeGear へ
     <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
   <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  {-# TERMINATING #-}
-<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  whileLoop : {l : Level} {t : Set l} -&gt; Env -&gt; (Code : Env -&gt; t) -&gt; t
+<span class="line-numbers"><a href="#n2" name="n2">2</a></span>  whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
 <span class="line-numbers"><a href="#n3" name="n3">3</a></span>  whileLoop env next with lt 0 (varn env)
 <span class="line-numbers"><a href="#n4" name="n4">4</a></span>  whileLoop env next | false = next env
 <span class="line-numbers"><a href="#n5" name="n5">5</a></span>  whileLoop env next | true =
@@ -652,11 +763,12 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gears-と-hoarelogic-をベースにした証明">Gears と HoareLogic をベースにした証明</h2>
+<h2 id="gears-と-hoarelogic-をベースにした証明全体">Gears と HoareLogic をベースにした証明(全体)</h2>
 <ul>
-  <li>ここでは
+  <li>最終状態で返ってくる i の値は c10 と一致する</li>
+  <li>これにより証明が可能
     <div class="language-AGDA highlighter-coderay"><div class="CodeRay">
-  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  proofGears : {c10 :  ℕ } → Set
+  <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>  proofGears : {c10 :  Nat } → Set
 <span class="line-numbers"><a href="#n2" name="n2">2</a></span>  proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
 <span class="line-numbers"><a href="#n3" name="n3">3</a></span>                 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 </pre></div>
@@ -665,27 +777,26 @@
   </li>
 </ul>
 
-<p>&lt;–!
-[論文目次]
-まえがき</p>
+
 
-<p>現状</p>
-
-<p>Agda</p>
-
-<p>GearsOS</p>
+</div>
 
-<p>CodeGear DataGear</p>
-
-<p>Gears と Agda</p>
-
-<p>Agda での HoareLogic</p>
-
-<p>Gears ベースの HoareLogic</p>
-
-<p>まとめと課題</p>
-
-<p>–&gt;</p>
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="まとめと今後の課題">まとめと今後の課題</h2>
+<ul>
+  <li>HoareLogic の while を使った例題を作成、証明を行った</li>
+  <li>Gears を用いた HoareLogic ベースの検証方法を導入した
+    <ul>
+      <li>証明が引数として渡される記述のため証明とプログラムを一体化できた</li>
+    </ul>
+  </li>
+  <li>今後の課題
+    <ul>
+      <li>RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)</li>
+    </ul>
+  </li>
+</ul>
 
 </div>
 
--- a/slide/slide.md	Sun Jan 13 23:42:16 2019 +0900
+++ b/slide/slide.md	Tue Jan 15 15:56:33 2019 +0900
@@ -1,4 +1,4 @@
-title: GearsOS の Hoare triple を用いた検証
+title: GearsOS の Hoare Logic を用いた検証
 author: Masataka Hokama
 profile: 琉球大学 : 並列信頼研究室
 lang: Japanese
@@ -9,17 +9,17 @@
 - OS やアプリケーションなどの信頼性は重要な課題
 - 信頼性を上げるために仕様を検証する必要
 - 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある
-  - 事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす
-- 既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい...?)
+  - 事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす
+- 既存の言語ではあまり利用されていない
 
 ## 背景
 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案
 - CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
-- Gear 間の接続処理はメタ計算として定義
-  - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証
-- 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する
+<!-- - Gear 間の接続処理はメタ計算として定義 -->
+<!--   - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証 -->
+- この単位を用いて信頼性の高い OS として GearsOS を開発している
+- 本発表では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する
 
-<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt=""  width="75%" height="75%"/></p>
 
 ## Gears について
 - **Gears** は当研究室で提案しているプログラム記述手法
@@ -29,19 +29,18 @@
 <!-- [fig1](file://./fig/cgdg.pdf) -->
 - CodeGear の接続処理は通常の計算とは異なるメタ計算として定義
   - メタ計算で信頼性の検証を行う
-
+<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt=""  width="75%" height="75%"/></p>
 <!-- ![cgdg](./pic/codeGear_dataGear.pdf){} -->
-<p style="text-align:center;"><img src="./pic/cgdg.svg" alt=""  width="30%" height="30%"/></p>
+<!-- <p style="text-align:center;"><img src="./pic/cgdg.svg" alt=""  width="30%" height="30%"/></p> -->
 
 ## CbC について
 - Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在
-  - これは C からループ制御構造と関数呼び出しを取り除き継続を導入したもの
-  - 環境を継続に含めない
-- 現在の CbC ではメタ計算での検証
+  - これは C からループ制御構造と関数呼び出しを取り除き、代わりに継続を導入したもの
+- 現在の CbC でもメタ計算での検証は可能
 - 将来的には証明も扱えるようにしたいが現段階では未実装
 - そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している
 
-## Agda
+## Agda とは
 - Agda は定理証明支援系の言語
 - 依存型を持つ関数型言語
 - 型を明記する必要がある
@@ -49,19 +48,15 @@
 
 ## Agda のデータ型
 - データ型は代数的なデータ構造
-- **data** キーワードの後に、**名前 : 型**、 where 句
+- **data** キーワードの後に、**名前 : 型**
 - 次の行以降は**コンストラクタ名 : 型**
 - 型は**->**または**→**で繋げる
-- 例えば、型**PrimComm −> Comm**は**PrimComm** を受け取り**Comm**を返す型
-- 再帰的な定義も可能
+  - 例えば、suc の型**Nat → Nat*は**Nat** を受け取り**Nat**を返す型
+  - これにより 3 を suc (suc (suc zero)) のように表せる
 ```AGDA
-    data Comm : Set where
-      Skip : Comm
-      Abort : Comm
-      PComm : PrimComm −> Comm
-      Seq : Comm −> Comm −> Comm
-      If : Cond −> Comm −> Comm −> Comm 
-      While : Cond −> Comm −> Comm
+     data Nat : Set where
+       zero : Nat
+       suc  : Nat → Nat
 ```
 
 <!-- - where は宣言した部分に束縛する -->
@@ -70,201 +65,197 @@
 - C 言語での構造体に近い
 - 複数のデータをまとめる
 - 関数内で構築できる
-- 構築時は**レコード名 {フィールド名 = 値}**
-- 複数ある場合は **{フィールド1 = 1 ; フィールド2 = 2}**のように **;** を使って列挙
-  - (varn,vari の型 **ℕ** は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -> ℕ で定義されてる)
+- 構築時は**record レコード名 {フィールド名 = 値}**
+- 複数ある場合は **record Env {varn = 1 ; varn = 2}**のように **;** を使って列挙
 ```AGDA
-    record Env : Set where 
-      field
-        varn : ℕ
-        vari : ℕ
+   record Env : Set where 
+     field
+       varn : Nat
+       vari : Nat
 ```
 
 ## Agda の関数
-- 関数にも型が必要
-- 関数は **関数名 = 値**
+- 関数にも型が必要(1行目)
+  - 引き算はは自然数を２つ取って結果の自然数を返す
+  - **_** は任意の値、名前で使うと受け取った引数が順番に入る
+- 関数本体は **関数名 = 値**
 - 関数ではパターンマッチがかける
-- **_** は任意の引数
+  - ここでは関数名に **_** を使っているため**Nat**の定義にから zero かそれ以外でパターンマッチ
 ```AGDA
-    _-_ : ℕ → ℕ → ℕ 
-    x - zero  = x
-    zero - _  = zero
-    (suc x) - (suc y)  = x - y
+   _-_ : Nat → Nat → Nat 
+   x - zero  = x
+   zero - _  = zero
+   (suc x) - (suc y)  = x - y
 ```
 
 ## Agda での証明
-- 関数の型に論理式
+- 関数の型に証明すべき論理式
 - 関数自体にそれを満たす導出
 - 完成した関数は証明
 - **{}** は暗黙的(推論される)
-- 下のコードは自然数に 0 を足したとき値が変わらないことの証明
+- 下のコードは Bool型の x と true の and を取ったものは x と等しいことの証明
+  - **refl** は **x == x** の左右の項が等しいことの証明
 ```AGDA
-    +zero : { y : ℕ } → y + zero  ≡ y
-    +zero {zero} = refl
-    +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
+   ∧true : { x : Bool } →  x  ∧  true  ≡ x
+   ∧true {x} with x
+   ∧true {x} | false = refl
+   ∧true {x} | true = refl
 ```
 
 ## Agda 上での HoareLogic
-* 現在 Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと
+* Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと
 それを Agda2 に書き写したものが存在している。
-* 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて説明を行う。
-
-
-## Agda での HoareLogic の理解
-* HoareLogic を用いて次のようなプログラム(while Program)を検証した。
-```C
-    n = 10;
-    i = 0;
+* 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて Agda2上で HoareLogic を構築する
 
-    while (n>0)
-    {
-      i++;
-      n--;
-    }
-```
-* このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
-* n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。
-
-## 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;
 
-## Agda 上での HoareLogic(コマンド定義)
-* Env は while Program の変数である var n, i
-* **PrimComm** は代入時に使用される
-* **Cond** は Condition で Env を受け取って Boolean の値を返す
+   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 : ℕ
-        vari : ℕ
+   record Env : Set where
+     field
+       varn : Nat
+       vari : Nat
 
-    PrimComm : Set
-    PrimComm = Env → Env
-
-    Cond : Set
-    Cond = (Env → Bool) 
+   Cond : Set
+   Cond = (Env → Bool) 
 ```
 
 ## Agda 上での HoareLogic(コマンド定義)
-* **Comm** は Agda のデータ型で定義した HoareLogic の Command
-  * **Skip** は何も変更しない
-  * **PComm** は変数を代入する
-  * **Seq** は Command を実行して次の Command に移す
-  * **If** は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える
-  * **while** は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す
+* **Comm** は Agda のデータ型で定義した HoareLogic のコマンド
+  * **PComm** は変数を代入のコマンド
+  * **Seq** はコマンドの推移、 Command を実行して次の Command に移す
+  * **If** は条件分岐のコマンド
+  * **while** は繰り返しのコマンド
+* 他にも何もしないコマンドやコマンドの停止などのコマンドもある
+- **PrimComm** は Env を受け取って Env を返す定義
 ```AGDA
-    data Comm : Set where
-      Skip  : Comm
-      Abort : Comm
-      PComm : PrimComm -> Comm
-      Seq   : Comm -> Comm -> Comm
-      If    : Cond -> Comm -> Comm -> Comm
-      While : Cond -> Comm -> Comm
+     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(実際のプログラムの記述)
-* Command を使って while Program を記述した。
+* 先程定義したコマンドを使って while Program を記述した
+  - 任意の自然数を引数に取る形になっているが**c10 == 10**ということにする
 * **$** は **()** の糖衣で行頭から行末までを ( ) で囲う
-  * 見やすさのため改行しているため 3~7 行はまとまっている
-* Seq は Comm を2つ取って次の Comm に移行する
+* 見やすさのため改行しているが 3~7 行は1行
 ```AGDA
-    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)} ))
+   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の理解
-* 規則は HTProof にまとめられてる
+## Agda 上での HoareLogic(コマンドの保証)1/3
+* 保証の規則は HTProof にまとめられてる
 * **PrimRule** は **PComm** で行う代入を保証する 
 * 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述
-  * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す関数
-* SkipRule は PreCondition を変更しないことの保証
-* AbortRule は プログラムが停止するときのルール
+  * **_⇒_** は 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
-      SkipRule : (b : Cond) -> HTProof b Skip b
-      AbortRule : (bPre : Cond) -> (bPost : Cond) ->
-                   HTProof bPre Abort bPost
+   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
+   Axiom : Cond → PrimComm → Cond → Set
+   Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
 ```
 
-## Agda 上での HoareLogicの理解
+## 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
+     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の理解
+## 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)
+     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
+   Tautology : Cond → Cond → Set
+   Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true
 ```
 
+
 ## Agda 上での HoareLogic(証明)
-* **proof1** は while Program の証明
-* HTProof に 初期状態とコマンドで書かれた **program**  と終了状態を渡す
-* lemma1~5は rule それぞれの証明
-* 
+- **proof1** は while Program の証明
+- HTProof に 初期状態と先程コマンドで記述した whileProgram である **program** と終了状態を渡す
+- Condititon は initCond や termCond のようにそれぞれ定義する必要がある
+- program に近い形で証明を記述できる
 ```AGDA
-    proof1 : HTProof initCond program termCond
-    proof1 =
-        SeqRule {λ e → true} ( PrimRule empty-case )
-          $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
-          $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
-              WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
-              $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
-                     $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
+   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
+   initCond : Cond
+   initCond env = true
 
-    termCond : {c10 : ℕ} → Cond
-    termCond {c10} env = Equal (vari env) c10
+   termCond : {c10 : Nat} → Cond
+   termCond {c10} env = Equal (vari env) c10
 ```
-
+<!-- * lemma1~5は rule それぞれの証明 -->
   <!-- program : Comm -->
   <!-- program =  -->
   <!--   Seq ( PComm (λ env → record env {varn = 10})) -->
@@ -273,12 +264,19 @@
   <!--     (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -->
   <!--       $ PComm (λ env → record env {varn = ((varn env) - 1)} )) -->
 
-## 証明の一部
-- 基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する
-- impl⇒ 
+## 証明の一部(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 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
-    lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+    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 ⟩
@@ -286,52 +284,112 @@
       ≡⟨ 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 : ℕ} → Tautology stmt2Cond whileInv -->
+    <!-- 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 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv -->
+    <!-- lemma4 :  {c10 : Nat} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv -->
     
-    <!-- lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond  -->
+    <!-- lemma5 : {c10 : Nat} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond  -->
 
 ## Agda での Gears
 - Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数
 - CPS の関数は引数として継続を受け取って継続に計算結果を渡す
-- **名前 : 引数 -> (Code : fa -> t) -> t**
+- **名前 : 引数 → (Code : fa → t) → t**
 - **t** は継続
-- **(Code : fa -> t)** は次の継続先
+- **(Code : fa → t)** は次の継続先
 - DataGear は Agda での CodeGear に使われる引数
 ```AGDA
-_g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t
-x g- zero next = next x
-zero g- _  = next zero
-(suc x) g- (suc y)  = next (x g- y)
+_-_ : {t : Set} → Nat → Nat → (Code : Nat → t) → t
+x - zero = (λ next → next x)
+zero - _ = (λ next → next zero)
+(suc x) - (suc y) = (x - y)
+```
+
+## Gears をベースにした HoareLogic と証明(全体)
+- Gears をベースにした while Program 
+  - これは証明でもある
+- whileループを任意の回数にするため**c10**は引数
+- whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい
+```AGDA
+    proofGears : {c10 :  Nat } → Set
+    proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
+                   (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 ```
 
-## Gears をベースにした HoareLogic
-* 次に Gears をベースにした while Program をみる。
-* このプログラムは自然数と継続先を受け取って t を返す
+## Gears と HoareLogic をベースにした証明(whileTest)
+- ここは代入する Command
+- 最初の Command なので PreCondition がない
+- もとの whileProgram では PComm を2回していたがまとめた
+- proof2は Post Condition が成り立つことの証明
+  - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型
+  - ２つのものを引数に取り、両方が同時に成り立つことを示す
+- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t**
+```AGDA
+    whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } → 
+                (Code : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+    whileTest' {_} {_} {c10} next = next env proof2
+      where
+        env : Env
+        env = record {vari = 0 ; varn = c10}
+        proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)      <-- PostCondition
+        proof2 = record {pi1 = refl ; pi2 = refl}
+```
+
+## Gears と HoareLogic をベースにした証明(conversion)
+- conversion は Condition から LoopInvaliant への変換を行う CodeGear
+- proof4 は LoopInvaliant の証明
+- Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t**
+```AGDA
+    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
+        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
+          ∎
+```
+
+## Gears と HoareLogic をベースにした証明(whileLoop)
+- whileLoop は loopInvaliant が true の間 WhileLoop を回し続けるCodeGear
+- この CodeGear は Agda がループが終わることが証明できてないため **{-# TERMINATING #-}** で明示
+- false になると次の CodeGear へ
 ```AGDA
     {-# TERMINATING #-}
-    whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t
+    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
 ```
 
-## Gears と HoareLogic をベースにした証明
-* ここでは
+## Gears と HoareLogic をベースにした証明(全体)
+- 最終状態で返ってくる i の値は c10 と一致する
+- これにより証明が可能
 ```AGDA
-    proofGears : {c10 :  ℕ } → Set
+    proofGears : {c10 :  Nat } → Set
     proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
                    (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 ```
 
-
 ## まとめと今後の課題
 - HoareLogic の while を使った例題を作成、証明を行った
 - Gears を用いた HoareLogic ベースの検証方法を導入した