-- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t
-whileTest' : {l : Level} {t : Set l}  → {c10 :  Nat } → 
+whileTest' : {t : Set}  → {c10 :  Nat } → 
       (Code : (env : Env)  → 
           ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
 whileTest' {_} {_} {c10} next = next env proof2
@@ -479,7 +495,7 @@
   proof4 は LoopInvaliant の証明
   Gears での HoareLogic の完全な記述は 引数 → PreCondition → (Code : fa → PostCondition → t) → t
     
-  conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  Nat } → 
+  conversion1 : {t : Set} → (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
@@ -552,7 +568,7 @@
 Gears と HoareLogic をベースにした証明(全体)
 
   最終状態で返ってくる i の値は c10 と一致する
-  これにより証明が可能
+  
これにより証明が完了
     
     proofGears : {c10 :  Nat } → Set
   proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
@@ -589,12 +605,53 @@
 
 
   
-発表終了
+Agda 上での HoareLogic 記述
 
-  ご清聴ありがとうございました。
+  Agda で構築した HoareLogic での whileProgram と Gears での whileProgram を見た目で比較
+  この他に証明にコマンド、コマンドの証明の定義を記述する必要がある
+    
+  -- HoareLogic でのwhileProgram
+program : ℕ → Comm
+program c10 = 
+  Seq ( PComm (λ env → record env {varn = c10}))
+  $ 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)} ))
+-- コマンドの証明部分
+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
+
+
+    
+  
 
 
 
+
+
+
+
+  
+Gears での HoareLogic 記述
+
+  
+    
+  proofGears : {c10 :  Nat } → Set
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
+               (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+
+
+    
+  
+
+
 
 
 
diff -r 07e1ccdfd844 -r 61117df82f51 slide/slide.md
--- a/slide/slide.md	Wed Jan 16 03:19:15 2019 +0900
+++ b/slide/slide.md	Wed Jan 16 12:42:49 2019 +0900
@@ -1,6 +1,6 @@
 title: GearsOS の Hoare Logic を用いた検証
 author: 外間政尊 , 河野真治
-profile: 琉球大学 : 並列信頼研究室
+profile: - 琉球大学 : 並列信頼研究室
 lang: Japanese
 
 
@@ -10,7 +10,7 @@
 - 信頼性を上げるために仕様を検証する必要
 - 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある
   - 事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす
-- OS の検証などで使われているが、実装の記述の他に関数型の記述が必要となる
+- OS の検証などで使われているが、実装の記述の他に実装に対応する証明が必要となる
 - HoareLogic の単位である代入や、WhileLoop に対応する分解が煩雑 
 
 ## GearsOS によるメタ計算としての HoareLogic の導入
@@ -19,12 +19,12 @@
 - この単位を用いて信頼性の高い OS として GearsOS を開発している
 - Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する
 - CodeGear は CbC により、C と同等の速度で実行可能かつ Agda の継続記述にもなっている
-- 変換を必要とせずに HoareLogic による証明をメタ計算として記述できる
+- 証明への変換を必要とせずに HoareLogic による証明をメタ計算として記述できるようになった
 
 
 ## Gears について
 - **Gears** は当研究室で提案しているプログラム記述手法
-- 計算の単位を **CodeGear** 、データの単位を **DataGear**
+- 処理の単位を **CodeGear** 、データの単位を **DataGear**
 - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
 - Output の DataGear は次の CodeGear の Input として接続される
 
@@ -34,37 +34,35 @@
 
 
 
-
 ## Agda での DataGear
 - **DataGear** は CodeGear でつかわれる引数
 - **データ型**と**レコード型**がある
 - データ型は一つのデータ
 ```AGDA
 data Nat : Set where
-  zero : Nat
-  suc  : Nat → Nat
+    zero : Nat
+    suc  : Nat → Nat
 ```
 - レコード型は複数のデータをまとめる
 ```AGDA
 record Env : Set where 
-  field
-    varn : Nat
-    vari : Nat
+    field
+      varn : Nat
+      vari : Nat
 ```
 
-
 ## Agda での Gears の記述(whileTest)
 - Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数
 - **{}** は暗黙的(推論される)
 - 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す
-- CodeGear の型は**名前 : 引数 → (Code : fa → t) → t**
+- CodeGear の型は**引数 → (Code : fa → t) → t**
 - **t** は継続(最終的に返すもの)
 - **(Code : fa → t)** は次の継続先
 ```AGDA
 whileTest : {t : Set} → (c10 : Nat) 
-            → (Code : Env → t) → t
+              → (Code : Env → t) → t
 whileTest c10 next = next (record {varn = c10 
-                                 ; vari = 0} )
+                                   ; vari = 0} )
 ```
 
 ## Agda での Gears の記述(whileLoop)
@@ -88,10 +86,9 @@
 ```
 
 ## Agda での証明
-- 証明の見た目関数と同じ
 - 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出**
-- **refl** は **x == x** で左右の項が等しいことの証明
-- 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明
+  - **refl** は **x == x** で左右の項が等しいことの証明
+  - **cong** は 関数と x ≡ y 受け取って、x ≡ y の両辺に関数を適応しても等しいことが変わらないことの証明
 - **+zero** は任意の自然数の右から zero を足しても元の数と等しいことの証明
   - **y = zero** のときは **zero ≡ zero** のため refl
   - **y = suc y** のときは cong を使い y の数を減らして再帰的に**+zero**を行っている
@@ -154,13 +151,12 @@
           ≡⟨ sym +zero  ⟩
             suc y + zero
           ∎
-
 sym : Symmetric {A = A} _≡_
 sym refl = refl
 ```
 
 ## HoareLogicをベースとした Gears での検証手法
-- 今回 HoareLogic で証明する例の疑似コードを用意した
+- 今回 HoareLogic で証明する次のようなコードを検証した
 - このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
 - n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。
 ```C
@@ -209,12 +205,12 @@
 - 最初の 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 } → 
+whileTest' : {t : Set}  → {c10 :  Nat } → 
         (Code : (env : Env)  → 
             ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
 whileTest' {_} {_} {c10} next = next env proof2
@@ -231,7 +227,7 @@
 - proof4 は LoopInvaliant の証明
 - Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t**
 ```AGDA
-conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  Nat } → 
+conversion1 : {t : Set} → (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
@@ -260,7 +256,7 @@
         c10
       ∎
 --  +-sym : { x y : Nat } → x + y ≡ y + x
-```      
+```
 
 ## Gears と HoareLogic をベースにした証明(whileLoop)
 - whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている
@@ -271,7 +267,7 @@
 
 ## Gears と HoareLogic をベースにした証明(全体)
 - 最終状態で返ってくる i の値は c10 と一致する
-- これにより証明が可能
+- これにより証明が完了
 ```AGDA
     proofGears : {c10 :  Nat } → Set
     proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
@@ -284,6 +280,33 @@
 - 今後の課題
   - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)
 
-## 発表終了
-- ご清聴ありがとうございました。
+## Agda 上での HoareLogic 記述
+- Agda で構築した HoareLogic での whileProgram と Gears での whileProgram を見た目で比較
+- この他に証明にコマンド、コマンドの証明の定義を記述する必要がある
+```AGDA
+-- HoareLogic でのwhileProgram
+program : ℕ → Comm
+program c10 = 
+    Seq ( PComm (λ env → record env {varn = c10}))
+    $ 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)} ))
+-- コマンドの証明部分
+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
+```
 
+## Gears での HoareLogic 記述
+- 
+```AGDA
+    proofGears : {c10 :  Nat } → Set
+    proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 
+                   (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+```