Mercurial > hg > Papers > 2018 > ryokka-sigos

changeset 10:328bcfd300bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix slides
author ryokka
date Sun, 20 May 2018 21:57:24 +0900
parents 907f967f662e
children 7aa41769f1f1
files Slide/fig/cbc-hoare.xbb Slide/fig/hoare-logic.xbb Slide/fig/meta.xbb Slide/sigos.html Slide/sigos.md
diffstat 5 files changed, 415 insertions(+), 455 deletions(-) [+]
line wrap: on
line diff
--- a/Slide/fig/cbc-hoare.xbb	Sat May 19 19:14:19 2018 +0900
+++ b/Slide/fig/cbc-hoare.xbb	Sun May 20 21:57:24 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: fig/cbc-hoare.pdf
+%%Title: cbc-hoare.pdf
 %%Creator: extractbb 20180217
 %%BoundingBox: 0 0 580 175
 %%HiResBoundingBox: 0.000000 0.000000 580.000000 175.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue May 15 18:15:06 2018
+%%CreationDate: Sat May 19 20:23:56 2018
 
--- a/Slide/fig/hoare-logic.xbb	Sat May 19 19:14:19 2018 +0900
+++ b/Slide/fig/hoare-logic.xbb	Sun May 20 21:57:24 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: fig/hoare-logic.pdf
+%%Title: hoare-logic.pdf
 %%Creator: extractbb 20180217
 %%BoundingBox: 0 0 580 76
 %%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue May 15 18:15:06 2018
+%%CreationDate: Sat May 19 20:23:56 2018
 
--- a/Slide/fig/meta.xbb	Sat May 19 19:14:19 2018 +0900
+++ b/Slide/fig/meta.xbb	Sun May 20 21:57:24 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: fig/meta.pdf
+%%Title: meta.pdf
 %%Creator: extractbb 20180217
 %%BoundingBox: 0 0 958 148
 %%HiResBoundingBox: 0.000000 0.000000 958.000000 148.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Tue May 15 18:15:06 2018
+%%CreationDate: Sat May 19 20:23:56 2018
 
--- a/Slide/sigos.html	Sat May 19 19:14:19 2018 +0900
+++ b/Slide/sigos.html	Sun May 20 21:57:24 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-05-19 17:31:37 +0900 with Markdown engine kramdown (1.15.0)
+                on 2018-05-20 21:56:29 +0900 with Markdown engine kramdown (1.15.0)
                   using options {}
   -->
 <!-- <span style="background-color:#ffcc99"> </span> -->
@@ -100,10 +100,10 @@
 <ul>
   <li>研究目的</li>
   <li>CodeGear と DataGear の説明</li>
-  <li>Agda での記述</li>
+  <li>Agda の記述</li>
+  <li>Interface の説明</li>
   <li>Agda での CodeGear 、 DataGear 、 Interface の表現</li>
   <li>実際に行なった証明</li>
-  <li>証明の改善</li>
   <li>まとめ</li>
 </ul>
 
@@ -117,11 +117,12 @@
   <li>保証をするためには仕様を検証する必要がある</li>
   <li>仕様を検証するにはモデル検査と <strong>定理証明</strong> の２つの手法がある
     <ul>
-      <li>モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認するもの</li>
-      <li>定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できるもの</li>
+      <li>モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか</li>
+      <li>定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する</li>
     </ul>
   </li>
   <li>当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している</li>
+  <li>また、上記の単位で計算をノーマルレベル、メタレベルに分け、信頼性と拡張性をメタレベルで保証する GearsOS を開発している</li>
 </ul>
 
 
@@ -129,11 +130,12 @@
 <div class='slide '>
 <!-- _S9SLIDE_ -->
 <h2 id="section-2">プログラムの信頼性の保証</h2>
+<!-- * データ構造を仕様と実装に分けて記述するため、GearsOS のモジュール化の仕組みである **Interface** を記述した -->
 <ul>
-  <li>本研究では <strong>定理証明支援系</strong> の言語 <strong>Agda</strong> をつかって仕様を検証した</li>
-  <li>データ構造を仕様と実装に分けて記述するため、モジュール化の仕組みである <strong>Interface</strong> を記述した</li>
-  <li>今回は Agda で CodeGear 、DataGear、という単位と Interface を定義した</li>
-  <li>また、 CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った</li>
+  <li>CodeGear、 DataGear を使ったプログラミングは関数型プログラミングに近い形になる</li>
+  <li>本研究では関数型の <strong>定理証明支援系</strong> の言語 <strong>Agda</strong> を用いて仕様を検証することとした</li>
+  <li>Agda で CodeGear 、DataGear、という単位と Interface を定義した</li>
+  <li>CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った</li>
 </ul>
 
 
@@ -142,20 +144,55 @@
 <!-- _S9SLIDE_ -->
 <h2 id="codegear--datagear-">CodeGear と DataGear の定義</h2>
 <ul>
-  <li>CodeGear とはプログラムを記述する際の処理の単位</li>
+  <li>CodeGear とはプログラムを記述する際の処理の単位で、Agda では通常の関数で表現する</li>
   <li>DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている</li>
-  <li>CodeGear はメタ計算によって別の CodeGear へ接続される</li>
+  <li>CodeGear はメタ計算によって次の CodeGear へ接続される</li>
+  <li>メタ計算部分では並列処理などの様々な処理を記述ができる</li>
+</ul>
+
+<div style="text-align: center;">
+    <img src="./fig/meta_cg_dg.svg" alt="goto" width="800" />
+</div>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="hoare-logic">Hoare Logic</h2>
+<ul>
+  <li>Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証する手法</li>
+  <li>前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) で変更する</li>
+  <li>{P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である</li>
 </ul>
 
 <div style="text-align: center;">
-    <img src="./fig/cgdg.svg" alt="goto" width="800" />
+    <img src="./fig/cgdg.svg" alt="cbc-hoare" width="800" />
 </div>
 
-<!-- ## Agda での CodeGear、 DataGear　の表現 -->
-<!-- * CodeGear は処理の単位なので、 Agda では通常関数として記述するものとする -->
-<!-- * DataGear はレコード型で定義できるため、 Agda の record を使用し記述する -->
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="hoare-logic--codegear-datagear">Hoare Logic と CodeGear、 DataGear</h2>
+<ul>
+  <li>Hoare Logic の状態と処理を CodeGear、 DataGear に当てはめる事ができる</li>
+  <li>Pre-condition を input の DataGear , Post-Conditon を output の DataGear , Command は CodeGear そのもの</li>
+  <li>Pre-conditon や Post-conditon をメタ計算部分で検証し、 CodeGear、 DataGear で書かれたプログラムに対して検証する</li>
+</ul>
 
-<p>次のスライドからは Agda の記述について解説を行う</p>
+<div style="text-align: center;">
+    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800" />
+</div>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--codegear-datagear">Agda での CodeGear、 DataGear　の表現</h2>
+<ul>
+  <li>CodeGear は処理の単位なので、 Agda では通常関数として記述する</li>
+  <li>DataGear は Agda の record を使用し記述する</li>
+</ul>
 
 
 </div>
@@ -163,17 +200,52 @@
 <!-- _S9SLIDE_ -->
 <h2 id="agda-">Agda での型</h2>
 <ul>
-  <li>Agda の 型は <strong>関数名 : 型</strong> のように <strong>:</strong> を使って定義される</li>
-  <li>ここでは Stack の<strong>実装</strong>である <strong>popSingleLinkedStack</strong> の型を例とする</li>
-  <li>この型は stack を受け取り、stack の先頭を取って、次の関数に渡すという関数の型</li>
-  <li>stack は空の可能性があるので Maybe a を返す</li>
-  <li>popSingleLinkedStack は Stack の pop のCodeGearで、継続に型 Maybe a を受けとる CodeGear <span style="background-color:#ffcc99">( <strong>(fa -&gt; t) -&gt; t</strong>)</span> に渡す</li>
+  <li>型は <strong>関数名 : 型</strong> のように <strong>:</strong> を使って定義する</li>
+  <li>a -&gt; b という型は、<strong>「a を受け取り、 b を返す」</strong>という型</li>
+  <li><strong>a -&gt; b -&gt; c</strong> のような型は <strong>a -&gt; (b -&gt; c)</strong> と同じで、  <strong>「a を受け取り、 b を受け取り、 c を返す」</strong> という型</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--1">Agda での型(例)</h2>
+<ul>
+  <li><strong>CodeGear の型</strong> は <strong>(code: a -&gt; t) -&gt; t</strong> のような形になる</li>
+  <li>例として通常の push (nomalPush) と 継続を用いた push (continuePush) の型を考える</li>
+</ul>
+
+<pre lang="AGDA"><code>-- 通常のstack
+nomalPush : Si -&gt; a -&gt; Si
+-- 継続を用いたstack
+continuePush : Si -&gt; a -&gt; (CodeGear : Si -&gt; t) -&gt; t
+</code></pre>
+
+<ul>
+  <li>nomalPush は 「<strong>stack</strong> と  <strong>data</strong>  を受け取り、 <strong>data が取り出された stack</strong> を返す」型</li>
+  <li>continuePush は 「<strong>stack</strong> と <strong>data</strong> <strong>と 継続先の (Code : )</strong> を受け取り、 <strong>継続先である t</strong>を返す」型</li>
+  <li>t は明示されていない不定な型で、継続を表している</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda-2">Agda での型(例2)</h2>
+<ul>
+  <li>実際に Stack の pop 操作の <strong>実装</strong> である <strong>popSingleLinkedStack</strong> の型を見る</li>
 </ul>
 
 <pre lang="AGDA"><code>popSingleLinkedStack : SingleLinkedStack a -&gt; 
    (Code : SingleLinkedStack a -&gt; (Maybe a) -&gt; t) -&gt; t
 </code></pre>
 
+<ul>
+  <li>この型では stack と行き先の CodeGear を受け取り、次の CodeGear に継続する</li>
+  <li>popSingleLinkedStack 継続に型 Maybe a を受けとる CodeGear ( <strong>(fa -&gt; t) -&gt; t</strong>) に渡している</li>
+  <li>stack の中身は空の可能性があるので Maybe型の a を返す</li>
+</ul>
+
 
 </div>
 <div class='slide '>
@@ -181,7 +253,7 @@
 <h2 id="maybe">Maybe</h2>
 <ul>
   <li><strong>Maybe</strong> はNothingかJustの２つの場合を持つ型で Agda の <strong>data</strong> として定義されている</li>
-  <li>Just か Nothing はパターンマッチで場合分けするNothing と Just a は Maybe を生成する constructor</li>
+  <li>Just か Nothing は場合分けで Nothing と Just a は Maybe を生成する constructor</li>
 </ul>
 
 <pre lang="AGDA"><code>data Maybe a : Set where
@@ -193,11 +265,11 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="data-">data を用いた等式の証明</h2>
+<h2 id="agda--2">Agda でのデータ</h2>
 <ul>
-  <li>x ≡ x は Agda では常に正しい論理式</li>
-  <li>data は <strong>data データ名 : 型</strong></li>
-  <li><strong>refl</strong> は左右の項が等しいことを表す x ≡ x を生成する項</li>
+  <li>データは <strong>data データ名 : 型</strong></li>
+  <li><strong>(x : A)</strong> は ある集合(a)に属する {A} という型を持った変数 <strong>x</strong> を表現</li>
+  <li><strong>refl</strong> は左右の項が等しいことを表す <strong>x ≡ x</strong> を生成</li>
   <li>x ≡ x を証明したい時には refl と書く</li>
 </ul>
 
@@ -209,32 +281,30 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda--1">Agda での関数</h2>
+<h2 id="refl-">refl を使った証明</h2>
 <ul>
-  <li>Agda での関数定義は <strong>関数名 = 関数の実装</strong></li>
-  <li>ここでは <strong>popSingleLinkedStack</strong> の関数を例とする</li>
-  <li>引数は <strong>関数名</strong> と <strong>=</strong> の間に記述する</li>
-  <li>stack と 次の CodeGear である cs を受け取り、 stack の中から data を取り出し、新しい stack に継続し、次の CodeGear へと stack 渡している</li>
-  <li>stack の top は Maybe a なので Nothing か Just が返ってくる</li>
-  <li><strong>with</strong> で data のパターンマッチができる</li>
+  <li>refl を使った例題 <strong>sym</strong></li>
 </ul>
 
-<pre lang="AGDA"><code>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))
+<pre lang="AGDA"><code>sym : {x : Set} {y : Set} -&gt; x ≡ y -&gt; y ≡ x
+sym refl = refl
 </code></pre>
 
+<ul>
+  <li><strong>x ≡ y</strong> ならば <strong>y ≡ x</strong> の証明</li>
+  <li>型は論理式として成り立っており、関数で証明を行っている</li>
+  <li>初めの x ≡ y は引数として与えられ、これは <strong>refl</strong></li>
+  <li><strong>x ≡ y</strong> が成り立つ時、初めて <strong>y ≡ x</strong> は refl</li>
+</ul>
+
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
 <h2 id="agda--record">Agda での record　の定義</h2>
 <ul>
-  <li>record は複数のデータをまとめて記述する型</li>
-  <li><strong>record レコード名</strong> を書き、その次の行の <strong>field</strong> 後に <strong>フィールド名:型名</strong> と列挙する</li>
+  <li>record 複数のデータをまとめて記述する型</li>
   <li>ここでは SingleLinkedStack の定義を例とする</li>
-  <li>定義では top フィールドのみを定義しているが複数定義することもできる</li>
-  <li>top には Element 型の要素 a が定義されており、 <strong>Element</strong> 型は現在の <strong>data</strong> と次の data を指す <strong>next</strong> を定義している</li>
 </ul>
 
 <pre lang="AGDA"><code>record SingleLinkedStack (a : Set) : Set where
@@ -242,37 +312,96 @@
     top : Maybe (Element a)
 </code></pre>
 
+<ul>
+  <li><strong>record レコード名</strong> 、下に <strong>field</strong> 、さらに下に <strong>フィールド名:型名</strong> を列挙</li>
+  <li>フィールド名は <strong>accessor</strong></li>
+  <li>top は Maybe (Element a) 型</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="element">Element</h2>
+<ul>
+  <li>Element 型も record で定義されている</li>
+  <li>このレコードは直積になっている</li>
+  <li><strong>datum</strong> は Element の要素自体で、 <strong>next</strong> は次の要素</li>
+</ul>
+
+<pre lang="AGDA"><code>record Element (a : Set) : Set where
+  field
+    datum : a
+    next : Maybe (Element a)
+</code></pre>
+
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda--record-">Agda での record の構築</h2>
+<h2 id="agda--3">Agda での関数</h2>
 <ul>
-  <li>record の構築は関数側</li>
-  <li><strong>record</strong> 後ろの <strong>{}</strong> 内部で <strong>フィールド名 = 値</strong> で列挙する</li>
-  <li>複数のレコードを記述するさいは <strong>;</strong> で区切る</li>
-  <li>例として <strong>pushSingleLinkedStack</strong> の関数部分を扱う</li>
-  <li>pushSingleLinkedStack では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している</li>
+  <li>Agda での関数は <strong>関数名 = 関数の実装</strong></li>
+  <li>ここでは <strong>popSingleLinkedStack</strong> の関数を例とする
+    <ul>
+      <li><strong>関数名</strong> と <strong>=</strong> の間に記述されてる stack 、 cg は引数</li>
+      <li>stack の top は Maybe a なので Nothing か Just が返り、2つの場合が存在</li>
+      <li><strong>with</strong> と <strong>|</strong> を使うことで data の場合分けができる</li>
+    </ul>
+  </li>
 </ul>
 
-<pre lang="Agda"><code>pushSingleLinkedStack stack datum next = 
-    next record {top = Just (record {datum = datum;next =(top stack)})}
+<pre lang="AGDA"><code>popSingleLinkedStack : SingleLinkedStack a -&gt; 
+   (Code : SingleLinkedStack a -&gt; (Maybe a) -&gt; t) -&gt; t
+popSingleLinkedStack stack cg with (top stack)
+popSingleLinkedStack stack cg | Nothing = cg stack  Nothing
+popSingleLinkedStack stack cg | Just d  = cg record  { top = (next d) } (Just (datum d))
 </code></pre>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h2 id="agda--record-">Agda での record の作成</h2>
+<ul>
+  <li>record の作成は関数内で行う</li>
+  <li>例として <strong>pushSingleLinkedStack</strong> の関数部分を扱う</li>
+</ul>
+
+<pre lang="Agda"><code>pushSingleLinkedStack : {t : Set} {a : Set} -&gt; SingleLinkedStack a -&gt; a -&gt; (Code : SingleLinkedStack a -&gt; t) -&gt; t
+pushSingleLinkedStack stack datum next = next record {top = Just (record {datum = datum;next =(top stack)})}
+</code></pre>
+
+<ul>
+  <li><strong>record</strong> 後ろの <strong>{}</strong> 内部で <strong>フィールド名 = 値</strong> で列挙</li>
+  <li>複数のフィールドを作成する際は <strong>;</strong> で区切る</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="inteface">Inteface</h2>
+<ul>
+  <li>Interface は GearsOS のモジュール化の仕組み</li>
+  <li>ある Data Gear と それに対する操作(API) を行う Code Gear の集合を表現</li>
+  <li>Interface を使うとデータ構造への操作を仕様と実装に分けて記述することができる</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h2 id="agda--interface-">Agda での Interface の定義</h2>
 <ul>
-  <li>Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した</li>
+  <li>GearsOS の Interface を Agda で定義した
+<!-- * Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した --></li>
   <li>ここでの push、 pop は仕様の型のみ記述され、実装は構築時に与える</li>
-  <li>t は継続を返す型を表し、次の CodeGear を指す</li>
-  <li>ここでの push 、 pop は pushSingleLinkedStack 、 popSingleLinkedStack に繋げる</li>
+  <li>t は不定な型で継続を表し、次の CodeGear を指す</li>
+  <li><strong>StackMethods</strong> は Stack から interface を通して 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
+<pre lang="AGDA"><code>record StackMethods (a : Set) {t : Set} (stackImpl : Set) : Set where
       field
         push : stackImpl -&gt; a -&gt; (stackImpl -&gt; t) -&gt; t
         pop  : stackImpl -&gt; (stackImpl -&gt; Maybe a -&gt; t) -&gt; t
@@ -282,12 +411,39 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h2 id="agda--interface--1">Agda での Interface の記述</h2>
+<ul>
+  <li>Stack を作成するとき仕様と実装を繋げている</li>
+  <li><strong>createSingleLinkedStack</strong> は中身のない Stack を作る</li>
+</ul>
+
+<pre lang="AGDA"><code>createSingleLinkedStack : {t : Set} {a : Set} -&gt; Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                             stack = emptySingleLinkedStack ;
+                             stackMethods = singleLinkedStackSpec 
+                           }
+</code></pre>
+
+<ul>
+  <li><strong>singleLinkedStackSpec</strong> は実装側の push、 pop をまとめている</li>
+</ul>
+
+<pre lang="AGDA"><code>singleLinkedStackSpec : {t : Set} {a : Set} -&gt; StackMethods a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                           }
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h2 id="section-3">証明の概要</h2>
 <ul>
-  <li>今回は Interface を通して、 <strong>任意の数</strong> を stack に push し、データが入った stack に対して pop を行なう</li>
-  <li>このとき push した値と pop した値が等しくなることを証明する</li>
-  <li>また、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい</li>
-  <li>そのため、<strong>状態の不定な</strong> Stack を作成する関数を定義した</li>
+  <li>今回は <strong>任意の数</strong> を Stack に push し、直後にその Stack に対して pop を行ない、 push したデータと pop して取れたデータが等しくなることを証明する</li>
+  <li>どのような状態の Stack に push し、 pop をしても値が等しくなって欲しい</li>
+  <li><strong>状態の不定な</strong> Stack を作成する関数を定義した</li>
 </ul>
 
 
@@ -296,9 +452,9 @@
 <!-- _S9SLIDE_ -->
 <h2 id="stack-">状態が不定な Stack の定義</h2>
 <ul>
-  <li>ここでは状態が不定な Stack を作成する関数 <strong>stackInSomeState</strong> を定義する</li>
-  <li>不定なstackを入力(s : SingleLinkedStack a )で与える</li>
-  <li>stackInSomeState は stack を受け取り、状態の決まっていない stack を構築する</li>
+  <li>状態が不定な Stack を作成する関数 <strong>stackInSomeState</strong></li>
+  <li>入力を使って任意の Stack を表す</li>
+  <li>stackInSomeState は Stack を受け取り、状態の決まっていない Stack を作成</li>
 </ul>
 
 <pre lang="AGDA"><code>stackInSomeState : (s : SingleLinkedStack a ) -&gt; Stack a ( SingleLinkedStack  a )
@@ -309,50 +465,28 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="agda--interface--1">Agda での Interface を含めた部分的な証明</h2>
+<h2 id="agda--interface--2">Agda での Interface を含めた部分的な証明</h2>
 <ul>
-  <li>証明部分は型部分にラムダ式で与える</li>
-  <li><strong>push-&gt;push-&gt;pop2</strong>では push を２回したときの値と、直後に pop を2回して取れた値が等しいことを型に記述している</li>
+  <li><strong>push-&gt;pop</strong>では push をし、直後に pop をして取れたデータが等しい</li>
+  <li>Agda では不明な部分を <strong>?</strong> と書くことができ、証明部分を ? としている</li>
 </ul>
 
-<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) -&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} {a} x y s = ?
+<pre lang="AGDA"><code>push-&gt;pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -&gt; pushStack (stackInSomeState s) x (\s1 -&gt; popStack s1 (\s2 x1 -&gt; (Just x ≡ x1 )))
+push-&gt;pop {a} x s = ?
 </code></pre>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="section-4">ラムダ式</h2>
+<h2 id="push-pop-">push-&gt;pop の型</h2>
 <ul>
-  <li><strong>\s1 -&gt;</strong> はラムダ式で push-&gt;push-&gt;pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している</li>
+  <li>ラムダ計算で結果を次の実行に渡している</li>
+  <li>ラムダ計算は関数を抽象的に扱うもので、名前がなく、入力と出力だけ</li>
+  <li>ここでは <strong>\s1 -&gt;</strong> がラムダ計算で、受け取った Stack (s) に push を行い、更新された Stack (s1) を次の CodeGear に渡している</li>
 </ul>
 
-<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) -&gt;
-    pushStack ( stackInSomeState s )  x ( \s1 -&gt;* pushStack s1 y ( \s2 -&gt;
-    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-</code></pre>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="agda--interface--2">Agda での Interface を含めた部分的な証明</h2>
-<ul>
-  <li>Agda では不明な部分を <strong>?</strong> と書くことができる</li>
-  <li><strong>?</strong> 部分はコンパイルすると <strong>{}n</strong> のように番号が付き、Agda から内部に入る型を示してもらえる</li>
-</ul>
-
-<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 {l} {a} 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))))
+<pre lang="AGDA"><code>push-&gt;pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -&gt; pushStack (stackInSomeState s) x (\s1 -&gt; popStack s1 (\s2 x1 -&gt; (Just x ≡ x1 )))
 </code></pre>
 
 
@@ -361,194 +495,45 @@
 <!-- _S9SLIDE_ -->
 <h2 id="agda--interface--3">Agda での Interface を含めた部分的な証明</h2>
 <ul>
-  <li>ここでは最終的に <strong>(Just x ≡ x1) ∧ (Just y ≡ y1)</strong> が返ってくる必要がある</li>
-  <li><strong>(x ≡ x1)</strong> と <strong>(y ≡ y1)</strong> の２つが同時に成り立つ必要がある</li>
-  <li>そこで <strong>∧</strong> の部分を record で定義した</li>
+  <li><strong>?</strong> 部分はコンパイルすると <strong>{}n</strong> のように番号が付き、Agda から内部に入る型を示してもらえる</li>
 </ul>
 
-<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>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="agda--interface--4">Agda での Interface を含めた部分的な証明(∧)</h2>
-<ul>
-  <li>a と b の２つの証明から a かつ b という証明を行うため <strong>∧</strong> を定義する</li>
-  <li>これには異なる２つのものを引数にとり、それらがレコードに同時に存在することが示せれば良い</li>
-  <li><strong>∧</strong> は 型 a と 型b をもつ2つの要素を左右にとり、 それらが同時に存在することを示すレコード型</li>
-</ul>
-
-<pre lang="AGDA"><code>record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
-  field
-    pi1 : a
-    pi2 : b
+<pre lang="AGDA"><code>push-&gt;pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -&gt; pushStack (stackInSomeState s) x (\s1 -&gt; popStack s1 (\s2 x1 -&gt; (Just x ≡ x1 )))
+push-&gt;pop {a} x s = { }0
 </code></pre>
 
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="agda--interface--5">Agda での Interface を含めた部分的な証明</h2>
-<ul>
-  <li>定義した ∧ を関数部分で構築する</li>
-  <li>ここでは <strong>pi1</strong> 、 <strong>pi2</strong> の両方を <strong>?</strong> としておく</li>
-</ul>
-
-<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) -&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} {a} x y s = record { pi1 = { }0 ; pi2 = { }1 }
-</code></pre>
-
-<pre lang="AGDA"><code>?0 : Just x ≡
-Just
-(Element.datum
- (.stack.element (stack (stackInSomeState s)) x
-  (λ s1 →
-     pushStack
-     (record
-      { stack = s1 ; stackMethods = stackMethods (stackInSomeState s) })
-     y
-     (λ s2 →
-        pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))))
-</code></pre>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="agda--interface--6">Agda での Interface を含めた部分的な証明</h2>
-<ul>
-  <li>∧ で定義された左右に <strong>x ≡ x1</strong> と　<strong>y ≡ y1</strong> が入る</li>
-  <li><strong>x ≡ x1</strong>、　<strong>y ≡ y1</strong> は共に <strong>refl</strong> で証明できる</li>
-  <li>pi1、pi2 は両方 refl が入ることで証明ができる</li>
-  <li>また、型に書かれた順で値が取り出されている為、最後のラムダ式で stack の性質である FIFO 通りに値が取れていることが分かる</li>
-  <li>これにより証明の目的であった「どのような状態の Stack に push し、 pop をしても値が等しくなる」ことを証明することができた</li>
-</ul>
-
-<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) -&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} {a} x y s = record { pi1 = refl ; pi2 = refl }
+<pre lang="AGDA"><code>?0 : pushStack (stackInSomeState s) x
+(λ s1 → popStack s1 (λ s2 → _≡_ (Just x)))
 </code></pre>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="section-5">手証明での限界</h2>
+<h2 id="agda--interface--4">Agda での Interface を含めた部分的な証明</h2>
 <ul>
-  <li>現在 Binary Tree に対して近い証明を書いている</li>
-  <li>これは 「Tree に対して node を put し、 get した時取れる node の値は put した node と等しい」というもの</li>
-  <li>Tree に対する操作では root Node から Node を辿る Loop があり、それを展開しながら証明を書く</li>
-  <li>Agda 側が put した node と get した node が等しいことを分かってくれず、証明が完成していない…</li>
-  <li>今後は新しい証明規則を導入して証明を行おうと考えている</li>
+  <li><strong>{ }0</strong> 部分には x≡x1 が入り、これは refl</li>
 </ul>
 
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="hoare-logic">Hoare Logic</h2>
-<ul>
-  <li>Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法</li>
-  <li>前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更するといったもの</li>
-  <li>この {P} C {Q} でプログラムを部分的に表すことができる</li>
-  <li>{P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である</li>
-</ul>
+<pre lang="AGDA"><code>push-&gt;pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -&gt; pushStack (stackInSomeState s) x (\s1 -&gt; popStack s1 (\s2 x1 -&gt; (Just x ≡ x1 )))
+push-&gt;pop {a} x s = refl
+</code></pre>
 
-<div style="text-align: center;">
-    <img src="./fig/hoare.svg" alt="hoare" width="1000" />
-</div>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="hoare-logic--cbc">Hoare Logic と CbC</h2>
-
-<ul>
-  <li>Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている</li>
-  <li>Pre-condition を input DataGear , Post-Conditon を output DataGear , Command は CodeGear そのものとして扱えると考えている。</li>
-</ul>
-
-<div style="text-align: center;">
-    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800" />
-</div>
+<p>とすることで証明することができた</p>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="hoare-logic--binary-tree">Hoare Logic での例 (Binary Tree)</h2>
-
-<!-- * この例では Node を put するための関数 "putTree" の移り変わりである。 -->
-<ul>
-  <li>この例では今後の証明に使おうとしている BinaryTree での put, get を例にする。</li>
-  <li>初めに Node を put するべき位置を調べる “findNode” を行い root から ノードを辿っている。ここでは辿ったノードを Stack に保存する</li>
-  <li>次に put すべき位置から木を再構成する”replaceNode”を行い、 Stack に保存したノードを辿り、木を再構築していく</li>
-</ul>
-
-<div style="text-align: center;">
-    <img src="./fig/fanctionLoop.svg" alt="f-loop" width="500" />
-</div>
-
-<p>ここでは findNode に注目する。</p>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="hoare-logic--binary-tree--findnode">Hoare Logic での例 (Binary Tree : findNode)</h2>
-<ul>
-  <li>findNode では引数として受け取ったノードと木の現在見ているノードを比較して ノードを入れる位置を決定している</li>
-  <li>また、Tree を再構築するために辿った node を Stack に保存している</li>
-  <li>この時 Hoare Logic 上での {P} 、 {Q} は <strong>Tree と Stack の総量</strong> になると考えている</li>
-  <li>{P} が 元のTree と 中身のないStack で、 {Q} が 中身のないTree と 全てのNodeが入ったStack となる
-<!-- * replaceNode では逆に {P} が 中身のないTree と 全てのNodeが入ったStack で、 {Q} が Nodeが更新されたTree と 中身のないStack となるはずである --></li>
-  <li>このように <strong>C</strong> で不変な変数を見つけることでループなどの処理も部分的に正当であると証明することができる</li>
-</ul>
-
-<div style="text-align: center;">
-    <img src="./fig/funcLoopinAutomata.svg" alt="f-loop-auto" width="500" />
-</div>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="section-6">まとめと今後の方針</h2>
-
+<h2 id="section-4">まとめと今後の方針</h2>
 <ul>
   <li>本研究では CodeGear、DataGear を Agda で定義することができた</li>
   <li>また Agda で Interface の記述及び Interface を含めた証明を行うことができた</li>
   <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた</li>
   <li>また、CbC での Interface 記述では考えられていなかった細かな記述が明らかになった</li>
-  <li>今後の方針としては  継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明が行えるかを検討する</li>
+  <li>RedBlackTree では Stack と異なり一つの操作に複数の CodeGear が入っているため Hoare Logic を使っての証明や、関数を展開しての証明などを行う</li>
+  <li>SynchronisedQueue の証明では並列処理シミュレーションを Agda で行うことと、動機機構などを含めての証明を行う</li>
 </ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<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/sigos.md	Sat May 19 19:14:19 2018 +0900
+++ b/Slide/sigos.md	Sun May 20 21:57:24 2018 +0900
@@ -13,63 +13,96 @@
 ## 本発表の流れ
 * 研究目的
 * CodeGear と DataGear の説明
-* Agda での記述
+* Agda の記述
+* Interface の説明
 * Agda での CodeGear 、 DataGear 、 Interface の表現
 * 実際に行なった証明
-* 証明の改善
 * まとめ
 
 ## プログラムの信頼性の保証
 * 動作するプログラムの信頼性を保証したい
 * 保証をするためには仕様を検証する必要がある
 * 仕様を検証するにはモデル検査と **定理証明** の２つの手法がある
-  * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認するもの
-  * 定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できるもの
+  * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか
+  * 定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
 * 当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
+* また、上記の単位で計算をノーマルレベル、メタレベルに分け、信頼性と拡張性をメタレベルで保証する GearsOS を開発している
 
 ## プログラムの信頼性の保証
-* 本研究では **定理証明支援系** の言語 **Agda** をつかって仕様を検証した
-* 当研究室では 信頼性の高い ~ として GearsOS という OS を開発している
-* CodeGear DataGear での プログラミングは 関数型に近いかたちのプログラミングになる
-* Agda は関数型言語であるため 近い形になると考えた~
-* データ構造を仕様と実装に分けて記述するため、モジュール化の仕組みである **Interface** を記述した
-* 今回は Agda で CodeGear 、DataGear、という単位と Interface を定義した
-* また、 CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った
+<!-- * データ構造を仕様と実装に分けて記述するため、GearsOS のモジュール化の仕組みである **Interface** を記述した -->
+* CodeGear、 DataGear を使ったプログラミングは関数型プログラミングに近い形になる
+* 本研究では関数型の **定理証明支援系** の言語 **Agda** を用いて仕様を検証することとした
+* Agda で CodeGear 、DataGear、という単位と Interface を定義した
+* CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った
 
 ## CodeGear と DataGear の定義
-* CodeGear とはプログラムを記述する際の処理の単位
+* CodeGear とはプログラムを記述する際の処理の単位で、Agda では通常の関数で表現する
 * DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている
-* CodeGear はメタ計算によって別の CodeGear へ接続される
+* CodeGear はメタ計算によって次の CodeGear へ接続される
+* メタ計算部分では並列処理などの様々な処理を記述ができる
+
+<div style="text-align: center;">
+    <img src="./fig/meta_cg_dg.svg" alt="goto" width="800">
+</div>
+
+## Hoare Logic
+* Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証する手法
+* 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) で変更する
+* {P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である
 
 <div style="text-align: center;">
-    <img src="./fig/meta.svg" alt="goto" width="800">
+    <img src="./fig/cgdg.svg" alt="cbc-hoare" width="800">
+</div>
+
+## Hoare Logic と CodeGear、 DataGear
+* Hoare Logic の状態と処理を CodeGear、 DataGear に当てはめる事ができる
+* Pre-condition を input の DataGear , Post-Conditon を output の DataGear , Command は CodeGear そのもの
+* Pre-conditon や Post-conditon をメタ計算部分で検証し、 CodeGear、 DataGear で書かれたプログラムに対して検証する
+
+<div style="text-align: center;">
+    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800">
 </div>
 
-<!-- ## Agda での CodeGear、 DataGear　の表現 -->
-<!-- * CodeGear は処理の単位なので、 Agda では通常関数として記述するものとする -->
-<!-- * DataGear はレコード型で定義できるため、 Agda の record を使用し記述する -->
-
-次のスライドからは Agda の記述について解説を行う
+## Agda での CodeGear、 DataGear　の表現
+* CodeGear は処理の単位なので、 Agda では通常関数として記述する
+* DataGear は Agda の record を使用し記述する
 
 ## Agda での型
-<!-- a->b->c  a ->(b->c) でスライド一枚 -->
-<!-- Code : SingleLinkedStack a -> (Maybe a) -> t の部分も上のスライドに入れる 写真にあるやつを例に入れる -->
-<!-- t の話もいれる -->
-* Agda の 型は **関数名 : 型** のように **:** を使って定義される
-* ここでは Stack の**実装**である **popSingleLinkedStack** の型を例とする
-* この型は stack を受け取り、stack の先頭を取って、次の関数に渡すという関数の型
-* stack は空の可能性があるので Maybe a を返す
-* popSingleLinkedStack は Stack の pop のCodeGearで、継続に型 Maybe a を受けとる CodeGear <span style="background-color:#ffcc99">( **(fa -> t) -> t**)</span> に渡す
+* 型は **関数名 : 型** のように **:** を使って定義する
+* a -> b という型は、**「a を受け取り、 b を返す」**という型
+* **a -> b -> c** のような型は **a -> (b -> c)** と同じで、  **「a を受け取り、 b を受け取り、 c を返す」** という型
+
+## Agda での型(例)
+* **CodeGear の型** は **(code: a -> t) -> t** のような形になる
+* 例として通常の push (nomalPush) と 継続を用いた push (continuePush) の型を考える
+
+```AGDA
+-- 通常のstack
+nomalPush : Si -> a -> Si
+-- 継続を用いたstack
+continuePush : Si -> a -> (CodeGear : Si -> t) -> t
+```
+
+* nomalPush は 「**stack** と  **data**  を受け取り、 **data が取り出された stack** を返す」型
+* continuePush は 「**stack** と **data** **と 継続先の (Code : )** を受け取り、 **継続先である t**を返す」型
+* t は明示されていない不定な型で、継続を表している
+
+
+## Agda での型(例2)
+* 実際に Stack の pop 操作の **実装** である **popSingleLinkedStack** の型を見る
 
 ```AGDA
 popSingleLinkedStack : SingleLinkedStack a -> 
    (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
 ```
 
+* この型では stack と行き先の CodeGear を受け取り、次の CodeGear に継続する
+* popSingleLinkedStack 継続に型 Maybe a を受けとる CodeGear ( **(fa -> t) -> t**) に渡している
+* stack の中身は空の可能性があるので Maybe型の a を返す
+
 ## Maybe
-(x : A) の説明
 * **Maybe** はNothingかJustの２つの場合を持つ型で Agda の **data** として定義されている
-* Just か Nothing はパターンマッチで場合分けするNothing と Just a は Maybe を生成する constructor
+* Just か Nothing は場合分けで Nothing と Just a は Maybe を生成する constructor
 
 ```AGDA
 data Maybe a : Set where
@@ -77,43 +110,33 @@
   Just    : a -> Maybe a
 ```
 
-## data を用いた等式の証明
-<!-- sym x==y,y==x の 証明をいれる 写真 -->
-* x ≡ x は Agda では常に正しい論理式
-* data は **data データ名 : 型**
-* **refl** は左右の項が等しいことを表す x ≡ x を生成する項
-*  x ≡ x を証明したい時には refl と書く
+## Agda でのデータ
+* データは **data データ名 : 型**
+* **(x : A)** は ある集合(a)に属する {A} という型を持った変数 **x** を表現
+* **refl** は左右の項が等しいことを表す **x ≡ x** を生成
+* x ≡ x を証明したい時には refl と書く
 
 ```AGDA
 data _≡_ {a} {A : Set a} (x : A) : A → Set a where
   refl : x ≡ x
 ```
 
-## Agda での関数
-<!-- with と | で場合分けができます -->
-* Agda での関数定義は **関数名 = 関数の実装**
-* ここでは **popSingleLinkedStack** の関数を例とする
-* 引数は **関数名** と **=** の間に記述する
-* stack と 次の CodeGear である cs を受け取り、 stack の中から data を取り出し、新しい stack に継続し、次の CodeGear へと stack 渡している
-* stack の top は Maybe a なので Nothing か Just が返ってくる
-* **with** で data のパターンマッチができる
+## refl を使った証明
+* refl を使った例題 **sym**
 
 ```AGDA
-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))
+sym : {x : Set} {y : Set} -> x ≡ y -> y ≡ x
+sym refl = refl
 ```
 
+* **x ≡ y** ならば **y ≡ x** の証明
+* 型は論理式として成り立っており、関数で証明を行っている
+* 初めの x ≡ y は引数として与えられ、これは **refl**
+* **x ≡ y** が成り立つ時、初めて **y ≡ x** は refl
+
 ## Agda での record　の定義
-<!-- data が表してるのは等式と場合分け -->
-<!-- data の直積 object が欲しい Agda では~ -->
-<!-- Element のスライドもいれる -->
-<!-- top はアクセサ -->
-* record は複数のデータをまとめて記述する型
-* **record レコード名** を書き、その次の行の **field** 後に **フィールド名:型名** と列挙する
+* record 複数のデータをまとめて記述する型
 * ここでは SingleLinkedStack の定義を例とする
-* 定義では top フィールドのみを定義しているが複数定義することもできる
-* top には Element 型の要素 a が定義されており、 **Element** 型は現在の **data** と次の data を指す **next** を定義している
 
 ```AGDA
 record SingleLinkedStack (a : Set) : Set where
@@ -121,57 +144,99 @@
     top : Maybe (Element a)
 ```
 
+* **record レコード名** 、下に **field** 、さらに下に **フィールド名:型名** を列挙
+* フィールド名は **accessor**
+* top は Maybe (Element a) 型
+
 ## Element
-* Element の説明
+* Element 型も record で定義されている
+* このレコードは直積になっている
+* **datum** は Element の要素自体で、 **next** は次の要素
+
 ```AGDA
-record Element {l : Level} (a : Set l) : Set l where
-  inductive
-  constructor cons
+record Element (a : Set) : Set where
   field
-    datum : a  -- `data` is reserved by Agda.
+    datum : a
     next : Maybe (Element a)
 ```
 
+## Agda での関数
+* Agda での関数は **関数名 = 関数の実装**
+* ここでは **popSingleLinkedStack** の関数を例とする
+    * **関数名** と **=** の間に記述されてる stack 、 cg は引数
+    * stack の top は Maybe a なので Nothing か Just が返り、2つの場合が存在
+    * **with** と **\|** を使うことで data の場合分けができる
 
-## Agda での record の構築
-* record の構築は関数側
-* **record** 後ろの **{}** 内部で **フィールド名 = 値** で列挙する
-* 複数のレコードを記述するさいは **;** で区切る
-* 例として **pushSingleLinkedStack** の関数部分を扱う
-* pushSingleLinkedStack では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
-
-```Agda
-pushSingleLinkedStack stack datum next = 
-    next record {top = Just (record {datum = datum;next =(top stack)})}
+```AGDA
+popSingleLinkedStack : SingleLinkedStack a -> 
+   (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack stack cg with (top stack)
+popSingleLinkedStack stack cg | Nothing = cg stack  Nothing
+popSingleLinkedStack stack cg | Just d  = cg record  { top = (next d) } (Just (datum d))
 ```
 
+## Agda での record の作成
+* record の作成は関数内で行う
+* 例として **pushSingleLinkedStack** の関数部分を扱う
+
+```Agda
+pushSingleLinkedStack : {t : Set} {a : Set} -> SingleLinkedStack a -> a -> (Code : SingleLinkedStack a -> t) -> t
+pushSingleLinkedStack stack datum next = next record {top = Just (record {datum = datum;next =(top stack)})}
+```
+
+* **record** 後ろの **{}** 内部で **フィールド名 = 値** で列挙
+* 複数のフィールドを作成する際は **;** で区切る
+
+## Inteface
+* Interface は GearsOS のモジュール化の仕組み
+* ある Data Gear と それに対する操作(API) を行う Code Gear の集合を表現
+* Interface を使うとデータ構造への操作を仕様と実装に分けて記述することができる
+
 ## Agda での Interface の定義
-<!-- Si -> a -> Si -->
-<!-- Si -> a (Si -> t) -> t -->
-<!-- t は 不定な感じ -->
-* Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した
+* GearsOS の Interface を Agda で定義した
+<!-- * Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した -->
 * ここでの push、 pop は仕様の型のみ記述され、実装は構築時に与える
-* t は継続を返す型を表し、次の CodeGear を指す
-* ここでの push 、 pop は pushSingleLinkedStack 、 popSingleLinkedStack に繋げる
+* t は不定な型で継続を表し、次の CodeGear を指す
+* **StackMethods** は Stack から interface を通して singleLinkedStack への操作を行う際の型を定義してる
 
 ```AGDA
-record StackMethods {n m : Level } (a : Set n ) 
-    {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+record StackMethods (a : Set) {t : Set} (stackImpl : Set) : Set where
       field
         push : stackImpl -> a -> (stackImpl -> t) -> t
         pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
 ```
 
+## Agda での Interface の記述
+* Stack を作成するとき仕様と実装を繋げている
+* **createSingleLinkedStack** は中身のない Stack を作る
+
+```AGDA
+createSingleLinkedStack : {t : Set} {a : Set} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                             stack = emptySingleLinkedStack ;
+                             stackMethods = singleLinkedStackSpec 
+                           }
+```
+
+* **singleLinkedStackSpec** は実装側の push、 pop をまとめている
+
+```AGDA
+singleLinkedStackSpec : {t : Set} {a : Set} -> StackMethods a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                           }
+```
+
 ## 証明の概要
-* 今回は Interface を通して、 **任意の数** を stack に push し、データが入った stack に対して pop を行なう
-* このとき push した値と pop した値が等しくなることを証明する
-* また、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
-* そのため、**状態の不定な** Stack を作成する関数を定義した
+* 今回は **任意の数** を Stack に push し、直後にその Stack に対して pop を行ない、 push したデータと pop して取れたデータが等しくなることを証明する
+* どのような状態の Stack に push し、 pop をしても値が等しくなって欲しい
+* **状態の不定な** Stack を作成する関数を定義した
 
 ## 状態が不定な Stack の定義
-* ここでは状態が不定な Stack を作成する関数 **stackInSomeState** を定義する
-* 不定なstackを入力(s : SingleLinkedStack a )で与える
-* stackInSomeState は stack を受け取り、状態の決まっていない stack を構築する
+* 状態が不定な Stack を作成する関数 **stackInSomeState**
+* 入力を使って任意の Stack を表す
+* stackInSomeState は Stack を受け取り、状態の決まっていない Stack を作成
 
 ```AGDA
 stackInSomeState : (s : SingleLinkedStack a ) -> Stack a ( SingleLinkedStack  a )
@@ -179,140 +244,50 @@
 ```
 
 ## Agda での Interface を含めた部分的な証明
-* 証明部分は型部分にラムダ式で与える
-* **push->push->pop2**では push を２回したときの値と、直後に pop を2回して取れた値が等しいことを型に記述している
-
-```AGDA
-push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
-    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
-    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {a} x y s = ?
-```
-
-## ラムダ式
-* **\s1 ->** はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
-
-```AGDA
-push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
-    pushStack ( stackInSomeState s )  x ( \s1 ->* pushStack s1 y ( \s2 ->
-    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-```
-
-## Agda での Interface を含めた部分的な証明
-* Agda では不明な部分を **?** と書くことができる
-* **?** 部分はコンパイルすると **{}n** のように番号が付き、Agda から内部に入る型を示してもらえる
-
-```AGDA
-push->push->pop2 {l} {a} x y s = { }0
-```
+* **push->pop**では push をし、直後に pop をして取れたデータが等しい
+* Agda では不明な部分を **?** と書くことができ、証明部分を ? としている
 
 ```AGDA
--- Goal
-?0 : pushStack (stackInSomeState s) x
-(λ s1 →
-   pushStack s1 y
-   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
+push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
+push->pop {a} x s = ?
 ```
 
-## Agda での Interface を含めた部分的な証明
-* ここでは最終的に **(Just x ≡ x1) ∧ (Just y ≡ y1)** が返ってくる必要がある
-* **(x ≡ x1)** と **(y ≡ y1)** の２つが同時に成り立つ必要がある
-* そこで **∧** の部分を record で定義した
+## push->pop の型
+* ラムダ計算で結果を次の実行に渡している
+* ラムダ計算は関数を抽象的に扱うもので、名前がなく、入力と出力だけ
+* ここでは **\s1 ->** がラムダ計算で、受け取った Stack (s) に push を行い、更新された Stack (s1) を次の CodeGear に渡している
 
 ```AGDA
--- 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 という証明を行うため **∧** を定義する
-* これには異なる２つのものを引数にとり、それらがレコードに同時に存在することが示せれば良い
-* **∧** は 型 a と 型b をもつ2つの要素を左右にとり、 それらが同時に存在することを示すレコード型
-
-```AGDA
-record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
-  field
-    pi1 : a
-    pi2 : b
+push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
 ```
 
 ## Agda での Interface を含めた部分的な証明
-* 定義した ∧ を関数部分で構築する
-* ここでは **pi1** 、 **pi2** の両方を **?** としておく
-
+* **?** 部分はコンパイルすると **{}n** のように番号が付き、Agda から内部に入る型を示してもらえる
 
 ```AGDA
-push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
-    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
-    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {a} x y s = record { pi1 = { }0 ; pi2 = { }1 }
+push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
+push->pop {a} x s = { }0
 ```
 
 ```AGDA
-?0 : Just x ≡
-Just
-(Element.datum
- (.stack.element (stack (stackInSomeState s)) x
-  (λ s1 →
-     pushStack
-     (record
-      { stack = s1 ; stackMethods = stackMethods (stackInSomeState s) })
-     y
-     (λ s2 →
-        pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))))
+?0 : pushStack (stackInSomeState s) x
+(λ s1 → popStack s1 (λ s2 → _≡_ (Just x)))
 ```
 
 ## Agda での Interface を含めた部分的な証明
-* ∧ で定義された左右に **x ≡ x1** と　**y ≡ y1** が入る
-* **x ≡ x1**、　**y ≡ y1** は共に **refl** で証明できる
-* pi1、pi2 は両方 refl が入ることで証明ができる
-* また、型に書かれた順で値が取り出されている為、最後のラムダ式で stack の性質である FIFO 通りに値が取れていることが分かる
-* これにより証明の目的であった「どのような状態の Stack に push し、 pop をしても値が等しくなる」ことを証明することができた
+* **{ }0** 部分には x≡x1 が入り、これは refl
 
 ```AGDA
-push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
-    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
-    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {a} x y s = record { pi1 = refl ; pi2 = refl }
+push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
+push->pop {a} x s = refl
 ```
 
-## 手証明での限界
-* 現在 Binary Tree に対して近い証明を書いている
-* これは 「Tree に対して node を put し、 get した時取れる node の値は put した node と等しい」というもの
-* Tree に対する操作では root Node から Node を辿る Loop があり、それを展開しながら証明を書く
-* Agda 側が put した node と get した node が等しいことを分かってくれず、証明が完成していない…
-* 今後は新しい証明規則を導入して証明を行おうと考えている
-
-## Hoare Logic
-* Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法
-* 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更するといったもの
-* この {P} C {Q} でプログラムを部分的に表すことができる
-* {P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である
-
-<div style="text-align: center;">
-    <img src="./fig/hoare.svg" alt="hoare" width="1000">
-</div>
-
-
-## Hoare Logic と CbC
-
-* Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている
-* Pre-condition を input DataGear , Post-Conditon を output DataGear , Command は CodeGear そのものとして扱えると考えている。
-
-<div style="text-align: center;">
-    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800">
-</div>
-
-
+とすることで証明することができた
 
 ## まとめと今後の方針
 * 本研究では CodeGear、DataGear を Agda で定義することができた
 * また Agda で Interface の記述及び Interface を含めた証明を行うことができた
 * これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
 * また、CbC での Interface 記述では考えられていなかった細かな記述が明らかになった
-* 今後は RedBlackTree や syncronisedQueue に対して証明を行う
-<!-- * 今後の方針としては  継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明が行えるかを検討する -->
-
+* RedBlackTree では Stack と異なり一つの操作に複数の CodeGear が入っているため Hoare Logic を使っての証明や、関数を展開しての証明などを行う
+* SynchronisedQueue の証明では並列処理シミュレーションを Agda で行うことと、動機機構などを含めての証明を行う