Binary file paper/final_thesis.pdf has changed

--- a/paper/final_thesis.tex	Tue Feb 09 18:44:53 2021 +0900
+++ b/paper/final_thesis.tex	Thu Feb 11 17:03:31 2021 +0900
@@ -104,8 +104,8 @@
 \input{tex/intro.tex} % はじめに
 \input{tex/cbc.tex} % CbC の説明
 \input{tex/agda.tex} % agda の説明
+\input{tex/cbc_agda.tex}% continuation 形式で書くagda
 \input{tex/hoare.tex} % Hoare Logic の説明
-\input{tex/cbc_agda.tex}% continuation 形式で書くagda
 \input{tex/rbt_intro.tex} % 赤黒木の説明
 \input{tex/rbt_imple.tex}% 手法
 \input{tex/rbt_verif.tex}% 検証

--- a/paper/src/agda/hoare-test.agda	Tue Feb 09 18:44:53 2021 +0900
+++ b/paper/src/agda/hoare-test.agda	Thu Feb 11 17:03:31 2021 +0900
@@ -70,8 +70,6 @@
 plus-mcg : (x y : ℕ) → Env
 plus-mcg x y = plus-init-mcg x y (λ env s → plus-p-mcg env (λ env s → env))
 
-
-
 test1 = plus-mcg 3 4
 
 {-

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/hoare-while.agda	Thu Feb 11 17:03:31 2021 +0900
@@ -0,0 +1,98 @@
+module hoare-while where
+
+open import Data.Nat
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat.Properties as NatProp -- <-cmp
+open import Relation.Binary
+
+record Envc : Set (succ Zero) where
+  field
+    c10 : ℕ
+    varn : ℕ
+    vari : ℕ
+open Envc
+
+whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (next : Envc → t) → t
+whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+
+whileLoopP : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
+whileLoopP env next exit with (varn env)
+... | zero = exit env
+... | suc n = exit (record env { varn = n ; vari = (suc n) })
+
+
+{-# TERMINATING #-}
+loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
+loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
+
+whileTestPCall : (c10 :  ℕ ) → Envc
+whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  env))
+
+---
+open import Data.Empty
+--open import Relation.Nullary using (¬_; Dec; yes; no)
+
+--open import Agda.Builtin.Unit
+open import utilities
+
+open import Relation.Binary.PropositionalEquality
+
+open _/\_
+
+data whileTestState  : Set where
+  s1 : whileTestState
+  s2 : whileTestState
+  sf : whileTestState
+
+whileTestStateP : whileTestState → Envc →  Set
+whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env)
+whileTestStateP s2 env = (varn env + vari env ≡ c10 env)
+whileTestStateP sf env = (vari env ≡ c10 env)
+
+whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
+whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
+   env : Envc
+   env = whileTestP c10 ( λ env → env )
+
+whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
+    → (next : (env : Envc ) → whileTestStateP s2 env  → t)
+    → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
+whileLoopPwP env s next exit with <-cmp 0 (varn env)
+whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
+  where
+    lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
+    lem refl refl = refl
+whileLoopPwP env s next exit | tri< a ¬b ¬c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
+  where
+    1<0 : 1 ≤ zero → ⊥
+    1<0 ()
+    proof5 : (suc zero  ≤ (varn  env))  → ((varn env ) - 1) + (vari env + 1) ≡ c10 env
+    proof5 (s≤s lt) with varn  env
+    proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a)
+    proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in
+      begin
+        n' + (vari env + 1)
+      ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+        n' + (1 + vari env )
+      ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+        (n' + 1) + vari env
+      ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+        (suc n' ) + vari env
+      ≡⟨⟩
+        varn env + vari env
+      ≡⟨ s  ⟩
+         c10 env
+      ∎
+
+
+whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
+  → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
+  → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
+whileLoopPwP' zero env refl refl next exit = exit env refl
+whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
+
+
+
+whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
+whileTestPSemSound c output refl = whileTestPSem c
+

Binary file paper/src/agda/hoare-while.agdai has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/hoare-while1.agda	Thu Feb 11 17:03:31 2021 +0900
@@ -0,0 +1,41 @@
+module hoare-while1 where
+
+open import Level renaming (suc to Suc ; zero to Zero )
+module WhileTest  where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat hiding (compare)
+open import Data.Maybe
+open import Data.List
+open import Function
+open import logic
+
+record Env : Set (Suc Zero) where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
+
+record WhileTest {m : Level }  {t : Set m }  : Set (Suc m) where
+  field
+    env : Env
+  whileInit : (c10 : ℕ) → (Env → t) → t
+  whileInit c10 next = next (record {varn = c10 ; vari = 0 } )
+  whileLoop : Env → (Code : Env → t) → t
+  whileLoop env next = whileLoop1 (varn env) env where
+      whileLoop1 : ℕ → Env → t
+      whileLoop1 zero env =  next env
+      whileLoop1 (suc t ) env = 
+          whileLoop1 t (record env {varn = t ; vari = (vari env) + 1}) 
+  whileTest : (c10 : ℕ) → (Env → t) → t
+  whileTest c10 next = whileInit c10 $ λ env → whileLoop env next
+
+open WhileTest
+
+createWhileTest : {m : Level} {t : Set m }  → WhileTest {m} {t}
+createWhileTest  = record { env = record { varn = 0; vari = 0 } }
+
+test2 : ℕ
+test2 = whileTest createWhileTest 10 $ λ e → vari e
+

Binary file paper/src/agda/hoare-while1.agdai has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/logic.agda	Thu Feb 11 17:03:31 2021 +0900
@@ -0,0 +1,152 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool → Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _/\_
+
+open import Relation.Binary.PropositionalEquality
+
+
+≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
+≡-Bool-func {true} {true} a→b b→a = refl
+≡-Bool-func {false} {true} a→b b→a with b→a refl
+... | ()
+≡-Bool-func {true} {false} a→b b→a with a→b refl
+... | ()
+≡-Bool-func {false} {false} a→b b→a = refl
+
+bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
+bool-≡-? true true = yes refl
+bool-≡-? true false = no (λ ())
+bool-≡-? false true = no (λ ())
+bool-≡-? false false = yes refl
+
+¬-bool-t : {a : Bool} →  ¬ ( a ≡ true ) → a ≡ false
+¬-bool-t {true} ne = ⊥-elim ( ne refl )
+¬-bool-t {false} ne = refl
+
+¬-bool-f : {a : Bool} →  ¬ ( a ≡ false ) → a ≡ true
+¬-bool-f {true} ne = refl
+¬-bool-f {false} ne = ⊥-elim ( ne refl )
+
+¬-bool : {a : Bool} →  a ≡ false  → a ≡ true → ⊥
+¬-bool refl ()
+
+lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
+lemma-∧-0 {true} {true} refl ()
+lemma-∧-0 {true} {false} ()
+lemma-∧-0 {false} {true} ()
+lemma-∧-0 {false} {false} ()
+
+lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
+lemma-∧-1 {true} {true} refl ()
+lemma-∧-1 {true} {false} ()
+lemma-∧-1 {false} {true} ()
+lemma-∧-1 {false} {false} ()
+
+bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
+bool-and-tt refl refl = refl
+
+bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 
+bool-∧→tt-0 {true} {true} refl = refl
+bool-∧→tt-0 {false} {_} ()
+
+bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 
+bool-∧→tt-1 {true} {true} refl = refl
+bool-∧→tt-1 {true} {false} ()
+bool-∧→tt-1 {false} {false} ()
+
+bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
+bool-or-1 {false} {true} refl = refl
+bool-or-1 {false} {false} refl = refl
+bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 
+bool-or-2 {true} {false} refl = refl
+bool-or-2 {false} {false} refl = refl
+
+bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 
+bool-or-3 {true} = refl
+bool-or-3 {false} = refl
+
+bool-or-31 : {a b : Bool} → b ≡ true  → ( a \/ b ) ≡ true 
+bool-or-31 {true} {true} refl = refl
+bool-or-31 {false} {true} refl = refl
+
+bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 
+bool-or-4 {true} = refl
+bool-or-4 {false} = refl
+
+bool-or-41 : {a b : Bool} → a ≡ true  → ( a \/ b ) ≡ true 
+bool-or-41 {true} {b} refl = refl
+
+bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
+bool-and-1 {false} {b} refl = refl
+bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
+bool-and-2 {true} {false} refl = refl
+bool-and-2 {false} {false} refl = refl
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda/utilities.agda	Thu Feb 11 17:03:31 2021 +0900
@@ -0,0 +1,171 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module utilities where
+
+open import Function
+open import Data.Nat
+open import Data.Product
+open import Data.Bool hiding ( _≟_  ; _≤?_)
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+
+Pred : Set -> Set₁
+Pred X = X -> Set
+
+Imply : Set -> Set -> Set
+Imply X Y = X -> Y
+
+Iff : Set -> Set -> Set
+Iff X Y = Imply X Y × Imply Y X
+
+record _/\_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+
+open  _/\_
+
+_-_ : ℕ → ℕ → ℕ 
+x - zero  = x
+zero - _  = zero
+(suc x) - (suc y)  = x - y
+
++zero : { y : ℕ } → y + zero  ≡ y
++zero {zero} = refl
++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
+
+
++-sym : { x y : ℕ } → x + y ≡ y + x
++-sym {zero} {zero} = refl
++-sym {zero} {suc y} = let open ≡-Reasoning  in
+          begin
+            zero + suc y 
+          ≡⟨⟩
+            suc y
+          ≡⟨ sym +zero ⟩
+            suc y + zero
+          ∎
++-sym {suc x} {zero} =  let open ≡-Reasoning  in
+          begin
+            suc x + zero
+          ≡⟨ +zero  ⟩
+            suc x
+          ≡⟨⟩
+            zero + suc x
+          ∎
++-sym {suc x} {suc y} = cong ( λ z → suc z ) (  let open ≡-Reasoning  in
+          begin
+            x + suc y
+          ≡⟨ +-sym {x} {suc y} ⟩
+            suc (y + x)
+          ≡⟨ cong ( λ z → suc z )  (+-sym {y} {x}) ⟩
+            suc (x + y)
+          ≡⟨ sym ( +-sym {y} {suc x}) ⟩
+            y + suc x
+          ∎ )
+
+
+minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y
+minus-plus {zero} {y} = +-sym {y} {1}
+minus-plus {suc x} {y} =  cong ( λ z → suc z ) (minus-plus {x} {y})
+
++1≡suc : { x : ℕ } → x + 1 ≡ suc x
++1≡suc {zero} = refl
++1≡suc {suc x} = cong ( λ z → suc z ) ( +1≡suc {x} )
+
+lt : ℕ → ℕ → Bool
+lt x y with (suc x ) ≤? y
+lt x y | yes p = true
+lt x y | no ¬p = false
+
+predℕ : {n :  ℕ } → lt 0 n ≡ true  →  ℕ
+predℕ {zero} ()
+predℕ {suc n} refl = n
+
+predℕ+1=n : {n :  ℕ } → (less : lt 0 n ≡ true ) → (predℕ less) + 1 ≡ n
+predℕ+1=n {zero} ()
+predℕ+1=n {suc n} refl = +1≡suc
+
+suc-predℕ=n : {n :  ℕ } → (less : lt 0 n ≡ true ) → suc (predℕ less) ≡ n
+suc-predℕ=n {zero} ()
+suc-predℕ=n {suc n} refl = refl
+
+Equal : ℕ → ℕ → Bool
+Equal x y with x ≟ y
+Equal x y | yes p = true
+Equal x y | no ¬p = false
+
+_⇒_ : Bool → Bool → Bool
+false  ⇒  _ = true
+true  ⇒  true = true
+true  ⇒  false = false
+
+⇒t : {x : Bool} → x  ⇒ true  ≡ true
+⇒t {x} with x
+⇒t {x} | false = refl
+⇒t {x} | true = refl
+
+f⇒ : {x : Bool} → false  ⇒ x  ≡ true
+f⇒ {x} with x
+f⇒ {x} | false = refl
+f⇒ {x} | true = refl
+
+∧-pi1 : { x y : Bool } → x  ∧  y  ≡ true  → x  ≡ true
+∧-pi1 {x} {y} eq with x | y | eq
+∧-pi1 {x} {y} eq | false | b | ()
+∧-pi1 {x} {y} eq | true | false | ()
+∧-pi1 {x} {y} eq | true | true | refl = refl
+
+∧-pi2 : { x y : Bool } →  x  ∧  y  ≡ true  → y  ≡ true
+∧-pi2 {x} {y} eq with x | y | eq
+∧-pi2 {x} {y} eq | false | b | ()
+∧-pi2 {x} {y} eq | true | false | ()
+∧-pi2 {x} {y} eq | true | true | refl = refl
+
+∧true : { x : Bool } →  x  ∧  true  ≡ x
+∧true {x} with x
+∧true {x} | false = refl
+∧true {x} | true = refl
+
+true∧ : { x : Bool } →  true  ∧  x  ≡ x
+true∧ {x} with x
+true∧ {x} | false = refl
+true∧ {x} | true = refl
+bool-case : ( x : Bool ) { p : Set } → ( x ≡ true  → p ) → ( x ≡ false  → p ) → p
+bool-case x T F with x
+bool-case x T F | false = F refl
+bool-case x T F | true = T refl
+
+impl⇒ :  {x y : Bool} → (x  ≡ true → y  ≡ true ) → x  ⇒ y  ≡ true
+impl⇒ {x} {y} p = bool-case x (λ x=t →   let open ≡-Reasoning  in
+          begin
+            x  ⇒ y
+          ≡⟨  cong ( λ z → x  ⇒ z ) (p x=t ) ⟩
+            x  ⇒  true
+          ≡⟨ ⇒t ⟩
+            true
+          ∎
+    ) ( λ x=f →  let open ≡-Reasoning  in
+          begin
+            x  ⇒  y
+          ≡⟨  cong ( λ z → z  ⇒  y ) x=f ⟩
+            true
+          ∎
+  )
+ 
+Equal→≡ : { x y : ℕ } →  Equal x y ≡ true → x ≡ y
+Equal→≡ {x} {y} eq with x ≟ y
+Equal→≡ {x} {y} refl | yes refl = refl
+Equal→≡ {x} {y} () | no ¬p 
+
+Equal+1 : { x y : ℕ } →  Equal x y ≡ Equal (suc x) (suc y)
+Equal+1 {x} {y} with  x ≟ y
+Equal+1 {x} {.x} | yes refl = {!!}
+Equal+1 {x} {y} | no ¬p = {!!}
+
+open import Data.Empty 
+
+≡→Equal : { x y : ℕ } → x ≡ y →  Equal x y ≡ true 
+≡→Equal {x} {.x} refl with x ≟ x
+≡→Equal {x} {.x} refl | yes refl = refl
+≡→Equal {x} {.x} refl | no ¬p = ⊥-elim ( ¬p refl )

Binary file paper/src/agda/utilities.agdai has changed

--- a/paper/tex/cbc.tex	Tue Feb 09 18:44:53 2021 +0900
+++ b/paper/tex/cbc.tex	Thu Feb 11 17:03:31 2021 +0900
@@ -17,7 +17,6 @@
 継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻れず、次の CodeGear へ継続を行う。
 これは、関数型プログラミングでは末尾再帰をしていることと同義である。
 
-
 \section{Meta Code Gear / Meta Data Gear}
 プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、
 資源管理等を記述しなければならない処理が存在する。これらの処理をメタ計算と呼ぶ。
@@ -41,7 +40,5 @@
 
 軽量実装になっているのか、上記のコードをアセンブラ変換した結果を見て確認する。
 
-\lstinputlisting[label=plus, caption=plus] {src/cbc/c.out}
-\lstinputlisting[label=plus, caption=plus] {src/cbc/cbc.out}
-
-
+\lstinputlisting[label=c-ass, caption=cで記述した際のfib()のアセンブラ] {src/cbc/c.out}
+\lstinputlisting[label=cbc-ass, caption=cbcで記述した際のfib()のアセンブラ] {src/cbc/cbc.out}

--- a/paper/tex/hoare.tex	Tue Feb 09 18:44:53 2021 +0900
+++ b/paper/tex/hoare.tex	Thu Feb 11 17:03:31 2021 +0900
@@ -17,7 +17,7 @@
 これらを満たし、
 事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
 
-\section{Hoare による Code Gear の検証 }
+\section{Hoare Logic による Code Gear の検証手法 }
 
 \figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。
 input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、
@@ -26,11 +26,30 @@
 各 Condition を Meta DataGear で定義し、
 条件を満たしているのかをMeta CodeGear で検証する。
 
-\begin{center}
-\includegraphics[height=3.4cm]{pic/hoare_cg_dg.pdf}
-%\caption{CodeGear、DataGear での Hoare Logic}
-\label{hoare}
-\end{center}
+\begin{figure}[H]
+  \begin{center}
+    \includegraphics[height=3.4cm]{pic/hoare_cg_dg.pdf}
+  \end{center}
+  \caption{CodeGear、DataGear での Hoare Logic}
+  \label{hoare}
+\end{figure}
+
+\section{CbCでの Hoare Logic を用いた検証}
+先行研究で行われている While Loop の Hoare Logic での検証を元に、
+実際の Hoare Logic を用いた検証手法について解説する。
+
+\subsection{CbC でのコードとそれに対応したAgdaのコード}
+
+元となる CbC での コードとそれと対応した Agda のコードを以下に示す。
+
+\subsection{}
+
+実装の際には、(next : Env → t)で Continuation に対応していた。
+これに加えてHoare Triple に対応する。
+そのため Env → t の間に Meta Data Gear を記述する
+以下は Meta Data Gear の記述
+% Meta Data Gearのソースコードを貼る
+
+s1 が初期状態、
 
 
-

--- a/paper/tex/rbt_verif.tex	Tue Feb 09 18:44:53 2021 +0900
+++ b/paper/tex/rbt_verif.tex	Thu Feb 11 17:03:31 2021 +0900
@@ -7,5 +7,5 @@
 
 そして、 Meta Code Gear から 生成される Meta Data Gear が Pre / Post Conditionを
 満たしているのか確認することで、関数一つ一つに対して Hoare Logic を用いた検証を行う
+%
 
-