Mercurial > hg > Papers > 2018 > ryokka-thesis

Binary file final_main/fig/csds.graffle has changed
Binary file final_pre/finalPre.pdf has changed
--- a/final_pre/finalPre.tex	Wed Feb 21 15:27:37 2018 +0900
+++ b/final_pre/finalPre.tex	Wed Feb 21 23:35:09 2018 +0900
@@ -58,17 +58,17 @@
   % この論文ではそれらに対して幾つかの部分的な証明を試みた。


-  % High reliability is important in Program.
-  % we are proposing programing units of CodeGear, DataGear for increase
-  % the reliability.
-  % we are deceloping Continuation based C (CbC) that can use units CodeGear and
-  % DataGear.
-  % In CbC, the handling of data in existing implementations is complicated.
-  % for that purpose, we can provide a interface mechanisms which are packages of
-  % CodeGears and DataGears.
-  % we made these units and interface available for Agda.
-  % In this papaer, we converted Stack and Tree using the interface discribe in
-  % CbC to Agda, and we tried several proofs on them.
+  High reliability is important in Program.
+  we are proposing programing units of CodeGear, DataGear for increase
+  the reliability.
+  we are deceloping Continuation based C (CbC) that can use units CodeGear and
+  DataGear.
+  In CbC, the handling of data in existing implementations is complicated.
+  for that purpose, we can provide a interface mechanisms which are packages of
+  CodeGears and DataGears.
+  we made these units and interface available for Agda.
+  In this papaer, we converted Stack and Tree using the interface discribe in
+  CbC to Agda, and we tried several proofs on them.


 \end{onecolabstract}]
--- a/slide/slide.html	Wed Feb 21 15:27:37 2018 +0900
+++ b/slide/slide.html	Wed Feb 21 23:35:09 2018 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===

       generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]
-                on 2018-02-21 15:26:02 +0900 with Markdown engine kramdown (1.15.0)
+                on 2018-02-21 23:26:03 +0900 with Markdown engine kramdown (1.15.0)
                   using options {}
   -->

@@ -94,7 +94,7 @@
 <h2 id="section">プログラムの信頼性の保証</h2>
 <ul>
   <li>動作するプログラムの信頼性を保証したい</li>
-  <li>プログラムの仕様を検証するには<strong>モデル検査</strong>と<strong>定理証明</strong>の２つの手法がある
+  <li>プログラムの仕様を検証するには <strong>モデル検査</strong> と <strong>定理証明</strong> の２つの手法がある
     <ul>
       <li>モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する</li>
       <li>定理証明　はプログラムの性質を論理式で記述しそれが常に正しいことを証明する</li>
@@ -103,12 +103,6 @@
   <li>また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している</li>
 </ul>

-<!-- * 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる -->
-
-<!-- * 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている -->
-
-<!-- * CbC での記述を Agda にマッピングし、その性質の一部を証明した -->
-

 </div>
 <div class='slide '>
@@ -118,168 +112,131 @@
   <li>CodeGear とはプログラムを記述する際の処理の単位である。</li>
   <li>DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。</li>
   <li>CodeGear はメタ計算によって CodeGear へ接続される</li>
-  <li>接続はメタ計算で行われ、メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる</li>
-  <li>CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する</li>
+  <li>メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる</li>
+  <li>Agda 上で CodeGear 、 DataGear という単位を定義した</li>
 </ul>

 <div style="text-align: center;">
-    <img src="./fig/csds.svg" alt="goto" width="800" />
+    <img src="./fig/cgdg.svg" alt="goto" width="800" />
 </div>


 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="continuation-based-c-cbc">Continuation based C (CbC)</h2>
+<h2 id="agda-">Agda とは</h2>
 <ul>
-  <li>当研究室で開発している言語</li>
-  <li>基本的な構文は C 言語と同じ</li>
-  <li>CodeGear、 DataGear という単位を用いてプログラムを記述する</li>
-  <li>CbC では 通常計算とメタ計算を分離している</li>
-  <li>CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく</li>
-  <li>CodeGear は関数の定義前に__codeがつく</li>
-  <li>関数末尾の goto により次の CodeGear に継続する</li>
+  <li>定理証明支援系</li>
+  <li>関数型言語</li>
+  <li>型を明示する必要がある</li>
+  <li>インデントも意味を持つ</li>
+  <li>型システムを用いて証明を記述できる</li>
 </ul>

-<pre lang="C"><code>__code cg0(int a, int b){
-  goto cg1(a+b);
-}

-__code cg1(int c){
-  goto cg2(c);
-}
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--1">Agda の型、関数</h2>
+<ul>
+  <li>例として singleLinkedStack の pop を使う</li>
+  <li>Agda の 型は <strong>関数名:型</strong> で定義される</li>
+  <li>Agda の 項、関数部分は <strong>関数名 = 値</strong></li>
+  <li>なにかを受け取って計算して次の関数に継続する型(<strong>-&gt; (fa -&gt; t) -&gt; t</strong>)</li>
+  <li>これはstackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型</li>
+  <li>このような形で CodeGear を Agda で定義できる</li>
+</ul>
+
+<pre lang="AGDA"><code>popSingleLinkedStack : -&gt; SingleLinkedStack a
+       -&gt; (Code : SingleLinkedStack a -&gt; (Maybe a) -&gt; t) -&gt; t
 </code></pre>


 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="context">Context</h2>
+<h2 id="maybe">Maybe</h2>
 <ul>
-  <li>CodeGear や DataGear をリストとして、 Context と呼ばれる Meta DataGear の中で定義している</li>
-  <li>しかし Context は Meta DataGear のため、通常レベルである CodeGear で直接扱うのは避けたい</li>
-  <li>その為、 stub CodeGear という Meta CodeGear を定義している。</li>
-  <li>stub CodeGear は Context を通して必要なデータを取り出し、次の CodeGear に接続する</li>
-  <li>stub CodeGear は CodeGear 毎に生成される</li>
+  <li><strong>Maybe</strong> はNothingかJustを返す型でAgda の dataとして定義されている</li>
+  <li>ここでは Just か Nothing をパターンマッチで返す</li>
+  <li>要素にも型を書く必要がある</li>
 </ul>

-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="interface">Interface</h2>
-<ul>
-  <li>CbC で実装していくにつれて stub CodeGear の記述が煩雑になることがわかった</li>
-  <li>そこで Interface というモジュール化の仕組みを導入した</li>
-  <li>Interface は CodeGear とそこで扱われている DataGear の集合を抽象的に表現した Meta DataGear として定義されている</li>
-  <li><strong>__code next(…)</strong> は継続を表していて <strong>…</strong>部分は後続の引数に相当する</li>
-</ul>
-
-<pre lang="C"><code>typedef struct Stack&lt;Type, Impl&gt;{
-        // DataGear
-        union Data* stack;
-        union Data* data;
-        union Data* data1;
-
-        // CodeGear
-        __code whenEmpty(...);
-        __code clear(Impl* stack,__code next(...));
-        __code push(Impl* stack,Type* data, __code next(...));
-        // 省略
-        __code next(...);
-} Stack;
+<pre lang="AGDA"><code>data Maybe a : Set where
+  Nothing : Maybe a
+  Just    : a -&gt; Maybe a
 </code></pre>


 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="interface-1">Interface</h2>
+<h2 id="refl">refl</h2>
 <ul>
-  <li>Interface を表す DataGear は次のような関数で生成される</li>
-  <li><strong>stack-&gt;push</strong> のようにしてコード中で使うことができる</li>
+  <li>data は <strong>data データ名 :</strong> と書く</li>
+  <li>等しいという data として <strong>refl</strong> が定義されている</li>
 </ul>

-<pre lang="C"><code>Stack* createSingleLinkedStack(struct Context* context) {
-    struct Stack* stack = new Stack();
-    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
-    stack-&gt;stack = (union Data*)singleLinkedStack;
-    singleLinkedStack-&gt;top = NULL;
-    stack-&gt;push = C_pushSingleLinkedStack;
-    stack-&gt;pop  = C_popSingleLinkedStack;
-    // 省略
-    return stack;
+<pre lang="AGDA"><code>data _≡_ {a} {A : Set a} (x : A) : A → Set a where
+  refl : x ≡ x
 </code></pre>


 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda">Agda</h2>
+<h2 id="agda">Agdaの関数</h2>
 <ul>
-  <li>Agda とは定理証明支援器で、型システムを用いて証明を記述できる。</li>
-  <li>Agda では関数の型を明示する必要がある</li>
+  <li>例として popSingleLinkedStack の関数を使う</li>
+  <li><strong>ラムダ式</strong> とは関数内で定義できる名前のない関数</li>
+  <li><strong>\ -&gt;</strong> で定義される</li>
+  <li>ラムダ式を使って CodeGear を継続することができる</li>
+  <li>関数での引数は <strong>関数名 a b :</strong> のように書く</li>
+  <li><strong>{変数}</strong> のように記述すると暗黙的な意味になり省略してもよい</li>
 </ul>

-<pre lang="AGDA"><code>-- Booleanの定義(データの定義例)
-data Bool : Set where
-  true : Bool
-  false : Bool
-
--- Bool値を反転する関数の例
-not : Bool → Bool
-not  true = false
-not  false = true
-
--- xor(複数の引数を取る例)
-xor : Bool → Bool → Bool
-xor  true true = false
-xor  false false = false
-xor _ _ = true
+<pre lang="AGDA"><code>popSingleLinkedStack :  -&gt; SingleLinkedStack a -&gt;
+   (Code : SingleLinkedStack a -&gt; (Maybe a) -&gt; t) -&gt; t
+popSingleLinkedStack stack cs with (top stack)
+popSingleLinkedStack stack cs | Nothing = cs stack  Nothing
+popSingleLinkedStack stack cs | Just d  = cs record  { top = (next d) } (Just (datum d))
 </code></pre>


 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda-1">AGDA</h2>
+<h2 id="record">record</h2>
 <ul>
-  <li>Agda 上で CodeGear、 DataGear の単位と継続を定義した</li>
-  <li>DataGear はレコード型として定義し、 CodeGear は通常の関数。</li>
+  <li>record は複数のデータを纏めて記述する型で、他の言語のオブジェクトのように <strong>レコード名.フィールド名</strong> でアクセスできる</li>
+  <li>SingleLinkedStack を例にとる</li>
+  <li><strong>record レコード名</strong> と書き、その次の行に <strong>field</strong> と書く</li>
+  <li>その下の行に <strong>フィールド名:型名</strong> と列挙する</li>
+  <li>SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている</li>
+  <li>Element では record で data と次の要素 next を定義している</li>
 </ul>

-<pre lang="AGDA"><code>// CbC
-__code cg0(int a, int b){
-  goto cg1(a+b);
-}
-
-</code></pre>
-<pre><code>-- agda DataGear
-record dg0 : Set where
+<pre lang="AGDA"><code>record SingleLinkedStack (a : Set) : Set where
   field
-    a : Int
-    b : Int
-
--- agda CodeGear define
-data CodeGear (A B : Set) : Set where
-  cg : (A -&gt; B) -&gt; CodeGear A B
-
--- agda CodeGear example
-cg0 : CodeGear dg0 dg1
-cg0 = cg (\d -&gt; goto cg1 (record {c = (dg0.a d) + (dg0.b d)}))
+    top : Maybe (Element a)
 </code></pre>


 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda-">Agda での証明</h2>
+<h2 id="pushsinglelinkedstackrecord">pushSingleLinkedStackの定義とrecordの構築</h2>
 <ul>
-  <li>型で論理を書き、関数部分で導出</li>
+  <li>pushSingleLinkedStack の型では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している</li>
+  <li>関数側では record の構築を行う</li>
+  <li><strong>record</strong> の後ろの {} 内部で <strong>フィールド名 = 値</strong> の形で列挙する</li>
+  <li>複数書くときは <strong>;</strong> で区切る</li>
 </ul>

-<pre lang="AGDA"><code>ex : 1 + 2 ≡ 3
-ex = refl
+<pre lang="Agda"><code>pushSingleLinkedStack2 : {n m : Level } {t : Set m } {Data : Set n} -&gt;
+    SingleLinkedStack Data -&gt; Data -&gt; (Code : SingleLinkedStack Data -&gt; t) -&gt; t
+pushSingleLinkedStack2 stack datum next =
+    next record {top = Just (record {datum = datum;next =(top stack)})}
 </code></pre>


@@ -288,94 +245,108 @@
 <!-- _S9SLIDE_ -->
 <h2 id="agda--interface-">Agda での Interface の定義</h2>
 <ul>
-  <li>Agda上でも CbC の Interface と同様のものを定義した。</li>
+  <li>stack の色々な実装を抽象的に表すために record を使い <strong>StackMethods</strong> をつくった</li>
+  <li>実装時は関数の中で record を構築している</li>
+  <li>push、 pop は実装によらないAPI</li>
+  <li>push、 pop に singlelinkedstack の実装が入る</li>
 </ul>

-<pre lang="AGDA"><code>record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
-  field
-    push : stackImpl -&gt; a -&gt; (stackImpl -&gt; t) -&gt; t
-    pop  : stackImpl -&gt; (stackImpl -&gt; Maybe a -&gt; t) -&gt; t
-    -- 省略
-open StackMethods
-
-record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
-  field
-    stack : si
-    stackMethods : StackMethods {n} {m} a {t} si
-  pushStack :  a -&gt; (Stack a si -&gt; t) -&gt; t
-  pushStack d next = push (stackMethods ) (stack ) d (\s1 -&gt; next (record {stack = s1 ; stackMethods = stackMethods } ))
-  popStack : (Stack a si -&gt; Maybe a  -&gt; t) -&gt; t
-  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -&gt; next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  -- 省略
-</code></pre>
-<ul lang="AGDA">
-  <li>インスタンス生成</li>
-</ul>
-<pre><code>singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -&gt; StackMethods {n} {m} a {t} (SingleLinkedStack a)
-singleLinkedStackSpec = record {
-                                   push = pushSingleLinkedStack
-                                 ; pop  = popSingleLinkedStack
-                                 -- 省略
-                           }
-
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -&gt; Stack {n} {m} a {t} (SingleLinkedStack a)
-createSingleLinkedStack = record {
-                             stack = emptySingleLinkedStack ;
-                             stackMethods = singleLinkedStackSpec
-                           }
+<pre lang="AGDA"><code>record StackMethods {n m : Level } (a : Set n )
+    {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+      field
+        push : stackImpl -&gt; a -&gt; (stackImpl -&gt; t) -&gt; t
+        pop  : stackImpl -&gt; (stackImpl -&gt; Maybe a -&gt; t) -&gt; t
 </code></pre>

-<!-- ## Tree の Interface -->
-
-<!-- ```AGDA -->
-<!-- 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 ) -->
-<!-- ``` -->
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--1">Agda での Interface を含めた部分的な証明</h2>
+<ul>
+  <li>stackInSomeState で不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している</li>
+  <li>Agda 中では不明な部分を <strong>?</strong> と書くことができる</li>
+  <li><strong>?</strong> 部分には値が入る</li>
+  <li>証明部分は ラムダ式で与える</li>
+</ul>

-<!-- * インスタンス生成 -->
+<pre lang="AGDA"><code>stackInSomeState : {l m : Level } {D : Set l} {t : Set m }
+   (s : SingleLinkedStack D ) -&gt; Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+</code></pre>

-<!-- ```AGDA -->
-
-<!-- ``` -->
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
+    pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt;
+    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push-&gt;push-&gt;pop2 {l} {D} x y s = ?
+</code></pre>


 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda--interface-stack-">Agda での Interface を含めた部分的な証明(Stack の例)</h2>
-
+<h2 id="agda--interface--2">Agda での Interface を含めた部分的な証明</h2>
 <ul>
-  <li>不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している</li>
+  <li>証明部分に書いた ? はコンパイル後に <strong>{ }0</strong> に変わり、中に入る型が表示される</li>
+  <li>x、y はMaybe なので Justで返ってくる</li>
+  <li>push した x、 y と x1、 y1 が共に等しいことを証明したい</li>
+  <li>そこで <strong>∧</strong> の部分をrecordで定義した</li>
 </ul>

-<pre lang="AGDA"><code>stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -&gt; Stack {l} {m} D {t}  ( SingleLinkedStack  D )
-stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
+    pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt;
+    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push-&gt;push-&gt;pop2 {l} {D} x y s = { }0
+</code></pre>

+<pre lang="AGDA"><code>-- Goal
+?0 : pushStack (stackInSomeState s) x
+(λ s1 →
+   pushStack s1 y
+   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
 </code></pre>

-<p lang="AGDA">実際の証明</p>
-<pre><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--3">Agda での Interface を含めた部分的な証明(∧)</h2>
+<ul>
+  <li>a と b の証明から aかつb を作るコンストラクタ</li>
+  <li>直積を表す型を定義する</li>
+</ul>
+
+<pre lang="AGDA"><code>record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--4">Agda での Interface を含めた部分的な証明</h2>
+<ul>
+  <li>∧でまとめたpi1、pi2は <strong>refl</strong> で証明することができた</li>
+</ul>
+
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
     pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt; pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
 push-&gt;push-&gt;pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
 </code></pre>

-<!-- ## Agda での Interface の部分的な証明と課題(Tree の例) -->

-<!-- ```AGDA -->
-
-<!-- ``` -->
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="section-1">今後の課題</h2>
+<ul>
+  <li>本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。</li>
+  <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。</li>
+  <li>また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。</li>
+  <li>今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている。</li>
+</ul>


 </div>
@@ -410,13 +381,17 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="section-1">今後の課題</h2>
-<ul>
-  <li>本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。</li>
-  <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。</li>
-  <li>また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。</li>
-  <li>今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。</li>
+<h2 id="element">Element</h2>
+<ul lang="AGDA">
+  <li>Element の説明</li>
 </ul>
+<pre><code>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)
+</code></pre>
 <!-- === end markdown block === -->
 </div>
--- a/slide/slide.md	Wed Feb 21 15:27:37 2018 +0900
+++ b/slide/slide.md	Wed Feb 21 23:35:09 2018 +0900
@@ -7,239 +7,186 @@

 ## プログラムの信頼性の保証
 * 動作するプログラムの信頼性を保証したい
-* プログラムの仕様を検証するには**モデル検査**と**定理証明**の２つの手法がある
+* プログラムの仕様を検証するには **モデル検査** と **定理証明** の２つの手法がある
   * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する
   * 定理証明　はプログラムの性質を論理式で記述しそれが常に正しいことを証明する
 * また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している

-<!-- * 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる -->
-
-<!-- * 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている -->
-
-<!-- * CbC での記述を Agda にマッピングし、その性質の一部を証明した -->
-

 ## CodeGear と DataGear
 * CodeGear とはプログラムを記述する際の処理の単位である。
 * DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。
 * CodeGear はメタ計算によって CodeGear へ接続される
-* 接続はメタ計算で行われ、メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる
-* CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する
+* メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる
+* Agda 上で CodeGear 、 DataGear という単位を定義した

 <div style="text-align: center;">
-    <img src="./fig/csds.svg" alt="goto" width="800">
+    <img src="./fig/cgdg.svg" alt="goto" width="800">
 </div>

-## Continuation based C (CbC)
-* 当研究室で開発している言語
-* 基本的な構文は C 言語と同じ
-* CodeGear、 DataGear という単位を用いてプログラムを記述する
-* CbC では 通常計算とメタ計算を分離している
-* CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく
-* CodeGear は関数の定義前に__codeがつく
-* 関数末尾の goto により次の CodeGear に継続する
-
-
-```C
-__code cg0(int a, int b){
-  goto cg1(a+b);
-}
-
-__code cg1(int c){
-  goto cg2(c);
-}
-```
-

-## Context
-* CodeGear や DataGear をリストとして、 Context と呼ばれる Meta DataGear の中で定義している
-* しかし Context は Meta DataGear のため、通常レベルである CodeGear で直接扱うのは避けたい
-* その為、 stub CodeGear という Meta CodeGear を定義している。
-* stub CodeGear は Context を通して必要なデータを取り出し、次の CodeGear に接続する
-* stub CodeGear は CodeGear 毎に生成される
+## Agda とは
+* 定理証明支援系
+* 関数型言語
+* 型を明示する必要がある
+* インデントも意味を持つ
+* 型システムを用いて証明を記述できる

-## Interface
-* CbC で実装していくにつれて stub CodeGear の記述が煩雑になることがわかった
-* そこで Interface というモジュール化の仕組みを導入した
-* Interface は CodeGear とそこで扱われている DataGear の集合を抽象的に表現した Meta DataGear として定義されている
-* **__code next(...)** は継続を表していて **...**部分は後続の引数に相当する
+## Agda の型、関数
+* 例として singleLinkedStack の pop を使う
+* Agda の 型は **関数名 : 型** で定義される
+* Agda の 項、関数部分は **関数名 = 値**
+* なにかを受け取って計算して次の関数に継続する型(**-> (fa -> t) -> t**)
+* これはstackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型
+* このような形で CodeGear を Agda で定義できる

-```C
-typedef struct Stack<Type, Impl>{
-        // DataGear
-        union Data* stack;
-        union Data* data;
-        union Data* data1;
+```AGDA
+popSingleLinkedStack : -> SingleLinkedStack a
+       -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+```

-        // CodeGear
-        __code whenEmpty(...);
-        __code clear(Impl* stack,__code next(...));
-        __code push(Impl* stack,Type* data, __code next(...));
-        // 省略
-        __code next(...);
-} Stack;
+## Maybe
+* **Maybe** はNothingかJustを返す型でAgda の dataとして定義されている
+* ここでは Just か Nothing をパターンマッチで返す
+* 要素にも型を書く必要がある
+
+```AGDA
+data Maybe a : Set where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
 ```

-## Interface
-* Interface を表す DataGear は次のような関数で生成される
-* **stack->push** のようにしてコード中で使うことができる
+## refl
+* data は **data データ名 :** と書く
+* 等しいという data として **refl** が定義されている

-```C
-Stack* createSingleLinkedStack(struct Context* context) {
-    struct Stack* stack = new Stack();
-    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
-    stack->stack = (union Data*)singleLinkedStack;
-    singleLinkedStack->top = NULL;
-    stack->push = C_pushSingleLinkedStack;
-    stack->pop  = C_popSingleLinkedStack;
-    // 省略
-    return stack;
+```AGDA
+data _≡_ {a} {A : Set a} (x : A) : A → Set a where
+  refl : x ≡ x
 ```

-## Agda
-* Agda とは定理証明支援器で、型システムを用いて証明を記述できる。
-* Agda では関数の型を明示する必要がある
+## Agdaの関数
+* 例として popSingleLinkedStack の関数を使う
+* ラムダ式を使って CodeGear を継続することができる
+* ラムダ式で**\ ->**書くことができる
+* 関数での引数は **関数名 a b :** のように書く
+* **{変数}** のように記述すると暗黙的な意味になり省略してもよい

 ```AGDA
--- Booleanの定義(データの定義例)
-data Bool : Set where
-  true : Bool
-  false : Bool
-
--- Bool値を反転する関数の例
-not : Bool → Bool
-not  true = false
-not  false = true
-
--- xor(複数の引数を取る例)
-xor : Bool → Bool → Bool
-xor  true true = false
-xor  false false = false
-xor _ _ = true
+popSingleLinkedStack :  -> SingleLinkedStack a ->
+   (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack stack cs with (top stack)
+popSingleLinkedStack stack cs | Nothing = cs stack  Nothing
+popSingleLinkedStack stack cs | Just d  = cs record  { top = (next d) } (Just (datum d))
 ```

-## AGDA
-* Agda 上で CodeGear、 DataGear の単位と継続を定義した
-* DataGear はレコード型として定義し、 CodeGear は通常の関数。
+## record
+* record は複数のデータを纏めて記述する型で、他の言語のオブジェクトのように **レコード名.フィールド名** でアクセスできる
+* SingleLinkedStack を例にとる
+* **record レコード名** と書き、その次の行に **field** と書く
+* その下の行に **フィールド名:型名** と列挙する
+* SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている
+* Element では record で data と次の要素 next を定義している

-```C
-// CbC
-__code cg0(int a, int b){
-  goto cg1(a+b);
-}
-
-```
 ```AGDA
--- agda DataGear
-record dg0 : Set where
+record SingleLinkedStack (a : Set) : Set where
   field
-    a : Int
-    b : Int
-
--- agda CodeGear define
-data CodeGear (A B : Set) : Set where
-  cg : (A -> B) -> CodeGear A B
-
--- agda CodeGear example
-cg0 : CodeGear dg0 dg1
-cg0 = cg (\d -> goto cg1 (record {c = (dg0.a d) + (dg0.b d)}))
+    top : Maybe (Element a)
 ```

-## Agda での証明
-* 型で論理を書き、関数部分で導出
+## pushSingleLinkedStackの定義とrecordの構築
+* pushSingleLinkedStack の型では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
+* 関数側では record の構築を行う
+* **record** の後ろの {} 内部で **フィールド名 = 値** の形で列挙する
+* 複数書くときは **;** で区切る

-```AGDA
-ex : 1 + 2 ≡ 3
-ex = refl
+```Agda
+pushSingleLinkedStack2 : {n m : Level } {t : Set m } {Data : Set n} ->
+    SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack2 stack datum next =
+    next record {top = Just (record {datum = datum;next =(top stack)})}
 ```


 ## Agda での Interface の定義
-* Agda上でも CbC の Interface と同様のものを定義した。
+* stack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
+* 実装時は関数の中で record を構築している
+* push、 pop は実装によらないAPI
+* push、 pop に singlelinkedstack の実装が入る

 ```AGDA
-record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
-  field
-    push : stackImpl -> a -> (stackImpl -> t) -> t
-    pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
-    -- 省略
-open StackMethods
+record StackMethods {n m : Level } (a : Set n )
+    {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+      field
+        push : stackImpl -> a -> (stackImpl -> t) -> t
+        pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
+```

-record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
-  field
-    stack : si
-    stackMethods : StackMethods {n} {m} a {t} si
-  pushStack :  a -> (Stack a si -> t) -> t
-  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
-  popStack : (Stack a si -> Maybe a  -> t) -> t
-  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  -- 省略
-```
-* インスタンス生成
+## Agda での Interface を含めた部分的な証明
+* stackInSomeState で不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している
+* Agda 中では不明な部分を **?** と書くことができる
+* **?** 部分には値が入る
+* 証明部分は ラムダ式で与える
+
 ```AGDA
-singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
-singleLinkedStackSpec = record {
-                                   push = pushSingleLinkedStack
-                                 ; pop  = popSingleLinkedStack
-                                 -- 省略
-                           }
+stackInSomeState : {l m : Level } {D : Set l} {t : Set m }
+   (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+```

-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
-createSingleLinkedStack = record {
-                             stack = emptySingleLinkedStack ;
-                             stackMethods = singleLinkedStackSpec
-                           }
+```AGDA
+push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
+    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {D} x y s = ?
 ```

-<!-- ## Tree の Interface -->
-
-<!-- ```AGDA -->
-<!-- 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 -->
+## Agda での Interface を含めた部分的な証明
+*  証明部分に書いた ? はコンパイル後に **{ }0** に変わり、中に入る型が表示される
+* x、y はMaybe なので Justで返ってくる
+* push した x、 y と x1、 y1 が共に等しいことを証明したい
+* そこで **∧** の部分をrecordで定義した

-<!-- 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 ) -->
-<!-- ``` -->
-
-<!-- * インスタンス生成 -->
-
-<!-- ```AGDA -->
-
-<!-- ``` -->
-
-## Agda での Interface を含めた部分的な証明(Stack の例)
-
-* 不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している
-
+```AGDA
+push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
+    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {D} x y s = { }0
+```

 ```AGDA
-stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
-stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
-
+-- Goal
+?0 : pushStack (stackInSomeState s) x
+(λ s1 →
+   pushStack s1 y
+   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
 ```

-実際の証明
+## Agda での Interface を含めた部分的な証明(∧)
+* a と b の証明から aかつb を作るコンストラクタ
+* 直積を表す型を定義する
+
+```AGDA
+record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+```
+
+## Agda での Interface を含めた部分的な証明
+* ∧でまとめたpi1、pi2は **refl** で証明することができた
+
 ```AGDA
 push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
     pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
 push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
 ```

-<!-- ## Agda での Interface の部分的な証明と課題(Tree の例) -->
-
-
-<!-- ```AGDA -->
-
-<!-- ``` -->
+## 今後の課題
+* 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
+* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
+* また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
+* 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている。


 ## Hoare Logic
@@ -261,8 +208,13 @@
 </div>


-## 今後の課題
-* 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
-* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
-* また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
-* 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。
+## Element
+* Element の説明
+```AGDA
+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)
+```