--- a/final_main/chapter2.tex	Sun Feb 18 21:43:41 2018 +0900
+++ b/final_main/chapter2.tex	Mon Feb 19 18:44:59 2018 +0900
@@ -208,7 +208,7 @@
 
 \lstinputlisting[label=src:interface, caption=CbCでのStack-Interfaceの記述] {src/interface.cbc}
 
-\lstinputlisting[label=src:interface-real, caption=CbCでのStack-Interfaceの実部] {src/singleLinkedStackInterface.cbc}
+\lstinputlisting[label=src:interface-real, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc}
 
 % そのへんのSourceをたくさんばらまく。
 

--- a/final_main/chapter4.tex	Sun Feb 18 21:43:41 2018 +0900
+++ b/final_main/chapter4.tex	Mon Feb 19 18:44:59 2018 +0900
@@ -61,7 +61,42 @@
 
 \section{Agda での Stack、 Tree の実装}
 
+ここでは Agda での Stack 、 Tree の実装を示す。
 
+Stack の実装を以下のソースコード\ref{src:stack-impl}で示す。
+実装は SingleLinkedStack という名前で定義されている。
+定義されている API は push を例に残りは省略する。残りのの実装は付録に示す。 %~\
+
+\lstinputlisting[label=src:stack-impl, caption=Agdaにおける Stack の実装] {src/AgdaStackImpl.agda.replaced}
+
+Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー
+タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。
+Maybe 型では値が存在する場合は Just 、 存在しない場合は　Nothing を返す。
+
+SingleLinkedStack 型では、この Element の top 部分のみを定義している。
+
+Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum
+の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい
+stack を返すというような実装をしている。
+
+Tree の実装(以下のソースコード\ref{src:tree-impl})は RedBlackTree という名前で定義されている。
+定義されている API は put 以後省略する。残りのの実装は付録に示す。 %~\
+
+\lstinputlisting[label=src:tree-impl, caption=Agdaにおける Tree の実装] {src/AgdaTreeImpl.agda.replaced}
+
+Node 型は key と value 、 Color と Node の rihgt 、 left の情報を持っている。
+Tree を構成する末端の Node は leafNode 型で定義されている。
+
+RedBlackTree 型は root の Node 情報と Tree に関する計算をする際に、そこまでの
+Node の経路情報を保持するための nodeStack と 比較するための compare を持っている。
+
+Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け
+取り、Tree の root に Node が存在しているかどうかで場合分けしている。
+Nothing が返ってきたときは RedBlackTree 型の tree 内に定義されている root に受け
+取ったキーと値を新しいノードとして追加する。
+Just が返ってきたときは root が存在するので、経路情報を積むために nodeStack を初
+期化し、受け取ったキーと値で新たなノードを作成した後、ノードが追加されるべき位置
+までキーの値を比べて新しい Tree を返すというような実装になっている。
 
 \section{Agda における Interface の実装}
 

--- a/final_main/chapter5.tex	Sun Feb 18 21:43:41 2018 +0900
+++ b/final_main/chapter5.tex	Mon Feb 19 18:44:59 2018 +0900
@@ -75,7 +75,6 @@
 
 ${!!}$ と書かれているところはまだ記述できていない部分で $?$ としている部分である。
 
-
 \lstinputlisting[label=src:agda-tree-proof, caption=Tree Interface の証
 明]{src/AgdaTreeProof.agda.replaced}
 
@@ -113,7 +112,7 @@
 
 % Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
 % 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
-
+pp
 %%
 % 部分正当性がプログラムに関する構造機能法によって合成的に証明できるという考えを導
 % 入した。

Binary file final_main/main.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaSingleLinkedStack.agda	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,63 @@
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+push = pushSingleLinkedStack
+; pop  = popSingleLinkedStack
+; pop2 = pop2SingleLinkedStack
+; get  = getSingleLinkedStack
+; get2 = get2SingleLinkedStack
+; clear = clearSingleLinkedStack
+}
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+stack = emptySingleLinkedStack ;
+stackMethods = singleLinkedStackSpec
+}
+
+-- Implementation
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+
+pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
+  where
+    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    pop2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
+
+
+getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+getSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack (Just data1)
+  where
+    data1  = datum d
+
+get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
+  where
+    get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    get2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
+
+clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t
+clearSingleLinkedStack stack next = next (record {top = Nothing})

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaStackImpl.agda	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,28 @@
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+  top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+-- Basic stack implementations are specifications of a Stack
+
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                               }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                            stack = emptySingleLinkedStack ;
+                            stackMethods = singleLinkedStackSpec
+                          }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaStackImpl.agda.replaced	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,28 @@
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+  top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+-- Basic stack implementations are specifications of a Stack
+
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                               }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                            stack = emptySingleLinkedStack ;
+                            stackMethods = singleLinkedStackSpec
+                          }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaTree.Agda	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,17 @@
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    putImpl : treeImpl -> a -> (treeImpl -> t) -> t
+    getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+    putTree : a -> (Tree treeImpl -> t) -> t
+    putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
+    getTree : (Tree treeImpl -> Maybe a -> t) -> t
+    getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+
+open Tree
+

--- a/final_main/src/AgdaTree.agda.replaced	Sun Feb 18 21:43:41 2018 +0900
+++ b/final_main/src/AgdaTree.agda.replaced	Mon Feb 19 18:44:59 2018 +0900
@@ -15,56 +15,3 @@
 
 open Tree
 
-data Color {n : Level } : Set n where
-  Red   : Color
-  Black : Color
-
-data CompareResult {n : Level } : Set n where
-  LT : CompareResult
-  GT : CompareResult
-  EQ : CompareResult
-
-record Node {n : Level } (a k : Set n) : Set n where
-  inductive
-    field
-      key   : k
-      value : a
-      right : Maybe (Node a k)
-      left  : Maybe (Node a k)
-      color : Color {n}
-open Node
-
-record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where
-  field
-    root : Maybe (Node a k)
-    nodeStack : SingleLinkedStack  (Node a k)
-    compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n}
-
-open RedBlackTree
-
-
-leafNode : {n : Level } {a k : Set n}  @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k
-leafNode k1 value = record {
-    key   = k1 ;
-    value = value ;
-    right = Nothing ;
-    left  = Nothing ;
-    color = Red
-  }
-
-putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
-putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
-...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
-...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next))
-
-getRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ (Maybe (Node a k)) @$\rightarrow$@ t) @$\rightarrow$@ t
-getRedBlackTree {_} {_} {a} {k} {t} tree k1 cs = checkNode (root tree)
-  module GetRedBlackTree where 
-    search : Node a k @$\rightarrow$@ t
-    checkNode : Maybe (Node a k) @$\rightarrow$@ t
-    checkNode Nothing = cs tree Nothing
-    checkNode (Just n) = search n
-    search n with compare tree k1 (key n) 
-    search n | LT = checkNode (left n)
-    search n | GT = checkNode (right n)
-    search n | EQ = cs tree (Just n)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaTreeImpl.agda	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,33 @@
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+  field
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+leafNode : {n : Level } {a k : Set n}  -> k -> a -> Node a k
+leafNode k1 value = record {
+  key   = k1 ;
+  value = value ;
+  right = Nothing ;
+  left  = Nothing ;
+  color = Red
+  }
+open leafNode
+
+record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.⊔ n) where
+  field
+    root : Maybe (Node a k)
+    nodeStack : SingleLinkedStack  (Node a k)
+    compare : k -> k -> CompareResult {n}
+open RedBlackTree
+
+putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
+putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next))
+
+-- 以下省略

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/AgdaTreeImpl.agda.replaced	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,47 @@
+record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    getImpl  : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+open TreeMethods
+
+record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    tree : treeImpl
+    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
+    putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
+    getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
+open Tree
+
+record Node {n : Level } (a k : Set n) : Set n where
+  inductive
+  field
+    key   : k
+    value : a
+    right : Maybe (Node a k)
+    left  : Maybe (Node a k)
+    color : Color {n}
+open Node
+
+leafNode : {n : Level } {a k : Set n}  @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k
+leafNode k1 value = record {
+  key   = k1 ;
+  value = value ;
+  right = Nothing ;
+  left  = Nothing ;
+  color = Red
+  }
+record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where
+  field
+    root : Maybe (Node a k)
+    nodeStack : SingleLinkedStack  (Node a k)
+    compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n}
+open RedBlackTree
+
+putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
+putRedBlackTree {n} {m} {a} {k}  {t} tree k1 value next with (root tree)
+...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
+...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next))
+
+-- 以下省略

--- a/final_main/src/AgdaTreeProof.agda	Sun Feb 18 21:43:41 2018 +0900
+++ b/final_main/src/AgdaTreeProof.agda	Mon Feb 19 18:44:59 2018 +0900
@@ -1,39 +1,3 @@
-module AgdaTreeProof where
-
-open import RedBlackTree
-open import stack
-open import Level hiding (zero)
-
-open import Data.Nat
-
-open Tree
-open Node
-open RedBlackTree.RedBlackTree
-open Stack
-
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary.Core
-open import Function
-
-check1 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
-check1 Nothing _ = False
-check1 (Just n)  x with Data.Nat.compare (value n)  x
-...  | equal _ = True
-...  | _ = False
-
-check2 : {m : Level } (n : Maybe (Node  ℕ ℕ)) -> ℕ -> Bool {m}
-check2 Nothing _ = False
-check2 (Just n)  x with compare2 (value n)  x
-...  | EQ = True
-...  | _ = False
-
-putTree1 : {n m : Level } {a k : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k -> k -> a -> (RedBlackTree {n} {m} {t} a k -> t) -> t
-putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
-...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
-...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s -> findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 -> replaceNode tree1 s n1 next))
-
-open ≡-Reasoning
-
 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
 
@@ -71,7 +35,7 @@
 compareLemma1 {suc _} {zero} ()
 compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
    where
-      lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
+     lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
       lemma2 = refl
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))

--- a/final_main/src/AgdaTreeProof.agda.replaced	Sun Feb 18 21:43:41 2018 +0900
+++ b/final_main/src/AgdaTreeProof.agda.replaced	Mon Feb 19 18:44:59 2018 +0900
@@ -1,37 +1,3 @@
-module AgdaTreeTest where
-
-open import RedBlackTree
-open import stack
-open import Level hiding (zero)
-
-open import Data.Nat
-
-open Tree
-open Node
-open RedBlackTree.RedBlackTree
-open Stack
-
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary.Core
-open import Function
-
-check1 : {m : Level } (n : Maybe (Node  @$\mathbb{N}$@ @$\mathbb{N}$@)) @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool {m}
-check1 Nothing _ = False
-check1 (Just n)  x with Data.Nat.compare (value n)  x
-...  | equal _ = True
-...  | _ = False
-
-check2 : {m : Level } (n : Maybe (Node  @$\mathbb{N}$@ @$\mathbb{N}$@)) @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool {m}
-check2 Nothing _ = False
-check2 (Just n)  x with compare2 (value n)  x
-...  | EQ = True
-...  | _ = False
-
-putTree1 : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
-putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree)
-...                                | Nothing = next (record tree {root = Just (leafNode k1 value) })
-...                                | Just n2  = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ replaceNode tree1 s n1 next))
-
 open @$\equiv$@-Reasoning
 
 redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@
@@ -71,7 +37,7 @@
 compareLemma1 {suc _} {zero} ()
 compareLemma1 {suc x} {suc y} eq = cong ( \z @$\rightarrow$@ @$\mathbb{N}$@.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
    where
-      lemma2 : compare2 (@$\mathbb{N}$@.suc x) (@$\mathbb{N}$@.suc y) @$\equiv$@ compare2 x y
+     lemma2 : compare2 (@$\mathbb{N}$@.suc x) (@$\mathbb{N}$@.suc y) @$\equiv$@ compare2 x y
       lemma2 = refl
 
 putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@))

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/final_main/src/stackImpl.agda	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,38 @@
+record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+open Element
+
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+  top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+-- push 以下は省略
+
+-- Basic stack implementations are specifications of a Stack
+
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                               }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                            stack = emptySingleLinkedStack ;
+                            stackMethods = singleLinkedStackSpec
+                          }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presen/slide.html	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,248 @@
+<!DOCTYPE html>
+<html>
+<head>
+   <meta http-equiv="content-type" content="text/html;charset=utf-8">
+   <title>「Agda による継続を用いたプログラムの検証」</title>
+
+<meta name="generator" content="Slide Show (S9) v2.5.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]">
+<meta name="author"    content="外間 政尊" >
+
+<!-- style sheet links -->
+<link rel="stylesheet" href="s6/themes/projection.css"   media="screen,projection">
+<link rel="stylesheet" href="s6/themes/screen.css"       media="screen">
+<link rel="stylesheet" href="s6/themes/print.css"        media="print">
+<link rel="stylesheet" href="s6/themes/blank.css"        media="screen,projection">
+
+<!-- JS -->
+<script src="s6/js/jquery-1.11.3.min.js"></script>
+<script src="s6/js/jquery.slideshow.js"></script>
+<script src="s6/js/jquery.slideshow.counter.js"></script>
+<script src="s6/js/jquery.slideshow.controls.js"></script>
+<script src="s6/js/jquery.slideshow.footer.js"></script>
+<script src="s6/js/jquery.slideshow.autoplay.js"></script>
+
+<!-- prettify -->
+<link rel="stylesheet" href="scripts/prettify.css">
+<script src="scripts/prettify.js"></script>
+
+<script>
+  $(document).ready( function() {
+    Slideshow.init();
+
+    $('code').each(function(_, el) {
+      if (!el.classList.contains('noprettyprint')) {
+        el.classList.add('prettyprint');
+      }
+    });
+    prettyPrint();
+  } );
+
+  
+</script>
+
+<!-- Better Browser Banner for Microsoft Internet Explorer (IE) -->
+<!--[if IE]>
+<script src="s6/js/jquery.microsoft.js"></script>
+<![endif]-->
+
+
+
+</head>
+<body>
+
+<div class="layout">
+  <div id="header"></div>
+  <div id="footer">
+    <div align="right">
+      <img src="s6/images/logo.svg" width="200px">
+    </div>
+  </div>
+</div>
+
+<div class="presentation">
+
+  <div class='slide cover'>
+    <table width="90%" height="90%" border="0" align="center">
+      <tr>
+        <td>
+          <div align="center">
+            <h1><font color="#808db5">「Agda による継続を用いたプログラムの検証」</font></h1>
+          </div>
+        </td>
+      </tr>
+      <tr>
+        <td>
+          <div align="left">
+            外間 政尊
+            @並列信頼研
+            <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;">
+          </div>
+        </td>
+      </tr>
+    </table>
+  </div>
+
+<div class='slide '>
+<!-- === begin markdown block ===
+
+      generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]
+                on 2018-02-19 03:03:45 +0900 with Markdown engine kramdown (1.15.0)
+                  using options {}
+  -->
+
+<!-- _S9SLIDE_ -->
+<h1 id="section">研究概要</h1>
+
+<ul>
+  <li>
+    <p>動作するプログラムの信頼性を保証したい</p>
+  </li>
+  <li>
+    <p>そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している</p>
+  </li>
+  <li>
+    <p>処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる</p>
+  </li>
+  <li>
+    <p>本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている</p>
+  </li>
+  <li>
+    <p>CbC での記述を Agda にマッピングし、その性質の一部を証明した</p>
+  </li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="codegear--datagear">CodeGear と DataGear</h1>
+
+<ul>
+  <li>
+    <p>CodeGear とはプログラムを記述する際の処理の単位である。</p>
+  </li>
+  <li>
+    <p>DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。</p>
+  </li>
+  <li>
+    <p>CodeGear はメタ計算によって CodeGear へ接続される</p>
+  </li>
+  <li>
+    <p>CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する。</p>
+  </li>
+</ul>
+
+<!-- CbC のスライドを作って間にいれる…？ -->
+<p># Continuation based C (CbC)</p>
+
+<ul>
+  <li>
+    <p>当研究室で開発している言語</p>
+  </li>
+  <li>
+    <p>基本的な構文は C lang</p>
+  </li>
+  <li>
+    <p>前述の CodeGear DataGear を用いてプログラムを記述する</p>
+  </li>
+  <li>
+    <p>CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく</p>
+  </li>
+  <li>
+    <p>DataGear をCodeGearで扱う際に、直接触れるといろいろできちゃう</p>
+  </li>
+  <li>
+    <p>その為、 Context というものを通して CodeGear の メタ計算として stub CodeGear を通して Context からデータを取ってきて変更して DataGear に返すということをしている。</p>
+  </li>
+  <li>
+    <p>現段階で複雑でない stub CodeGear はスクリプトを使って自動生成している</p>
+  </li>
+  <li>
+    <p>ただ、複雑な処理をする際には stub CodeGear を手動で書く必要がある、煩雑。</p>
+  </li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="interface">Interface</h1>
+
+<ul>
+  <li>
+    <p>そこで Interface を記述することになった</p>
+  </li>
+  <li>
+    <p>データ構造としての api と DataGear を結びつけて呼び出しやすくなった</p>
+  </li>
+</ul>
+
+<!-- interface の例 -->
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="agda">Agda</h1>
+
+<ul>
+  <li>
+    <p>Agda とは定理証明支援器で、型システムを用いて証明を記述できる。</p>
+  </li>
+  <li>
+    <p>Agda 上でも CodeGear、 DataGear の単位と継続を定義した(「メタ計算を用いた Continuation based C」琉球大学工学部情報工学科平成 29 年度学位論文(修士)より)</p>
+  </li>
+  <li>
+    <p>Agda上でも CbC の Interface と同様のものを記述した。</p>
+  </li>
+</ul>
+
+<!-- AgdaのInterface の例 -->
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="agda--interface-stack-">Agda での Interface の部分的な証明(Stack の例)</h1>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="agda--interface-tree-">Agda での Interface の部分的な証明(Tree の例)</h1>
+
+<!-- なんでだめなのかがうまく説明できないかも… -->
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="hoare-logic">Hoare Logic</h1>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-1">今後の課題</h1>
+
+<ul>
+  <li>
+    <p>本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。</p>
+  </li>
+  <li>
+    <p>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。</p>
+  </li>
+  <li>
+    <p>また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。</p>
+  </li>
+  <li>
+    <p>今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。</p>
+  </li>
+</ul>
+<!-- === end markdown block === -->
+</div>
+
+
+</div><!-- presentation -->
+</body>
+</html>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presen/slide.md	Mon Feb 19 18:44:59 2018 +0900
@@ -0,0 +1,89 @@
+title: 「Agda による継続を用いたプログラムの検証」
+author: 外間 政尊
+profile: @並列信頼研
+lang: Japanese
+code-engine: coderay
+
+
+# 研究概要
+
+* 動作するプログラムの信頼性を保証したい
+
+* そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している
+
+* 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる
+
+* 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている
+
+* CbC での記述を Agda にマッピングし、その性質の一部を証明した
+
+# CodeGear と DataGear
+
+* CodeGear とはプログラムを記述する際の処理の単位である。
+
+* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。
+
+* CodeGear はメタ計算によって CodeGear へ接続される
+
+* CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する。
+
+
+<!-- CbC のスライドを作って間にいれる…？ -->
+# Continuation based C (CbC)
+
+* 当研究室で開発している言語
+
+* 基本的な構文は C lang
+
+* 前述の CodeGear DataGear を用いてプログラムを記述する
+
+* CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく
+
+* DataGear をCodeGearで扱う際に、直接触れるといろいろできちゃう
+
+* その為、 Context というものを通して CodeGear の メタ計算として stub CodeGear を通して Context からデータを取ってきて変更して DataGear に返すということをしている。
+
+* 現段階で複雑でない stub CodeGear はスクリプトを使って自動生成している
+
+* ただ、複雑な処理をする際には stub CodeGear を手動で書く必要がある、煩雑。
+
+# Interface
+
+* そこで Interface を記述することになった
+
+* データ構造としての api と DataGear を結びつけて呼び出しやすくなった
+
+<!-- interface の例 -->
+
+# Agda
+
+* Agda とは定理証明支援器で、型システムを用いて証明を記述できる。
+
+* Agda 上でも CodeGear、 DataGear の単位と継続を定義した(「メタ計算を用いた Continuation based C」琉球大学工学部情報工学科平成 29 年度学位論文(修士)より)
+
+* Agda上でも CbC の Interface と同様のものを記述した。
+
+<!-- AgdaのInterface の例 -->
+
+# Agda での Interface の部分的な証明(Stack の例)
+
+
+
+# Agda での Interface の部分的な証明(Tree の例)
+
+<!-- なんでだめなのかがうまく説明できないかも… -->
+
+
+# Hoare Logic
+
+
+
+# 今後の課題
+
+* 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
+
+* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
+
+* また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
+
+* 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。