Mercurial > hg > Papers > 2018 > ryokka-sigos

changeset 11:7aa41769f1f1

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 23:42:24 +0900
parents 328bcfd300bd
children e20725cd6d8a
files Slide/sigos.html Slide/sigos.md
diffstat 2 files changed, 179 insertions(+), 168 deletions(-) [+]
line wrap: on
line diff
--- a/Slide/sigos.html	Sun May 20 21:57:24 2018 +0900
+++ b/Slide/sigos.html	Sun May 20 23:42: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-20 21:56:29 +0900 with Markdown engine kramdown (1.15.0)
+                on 2018-05-20 23:41:15 +0900 with Markdown engine kramdown (1.15.0)
                   using options {}
   -->
 <!-- <span style="background-color:#ffcc99"> </span> -->
@@ -94,17 +94,27 @@
 <!-- <span style="background-color:#ffcc99">hoge</span> -->
 <!-- ``` -->
 
+<!-- ## 本発表の流れ -->
+<!-- * 研究目的 -->
+<!-- * CodeGear と DataGear の説明 -->
+<!-- * Agda の記述 -->
+<!-- * Interface の説明 -->
+<!-- * Agda での CodeGear 、 DataGear 、 Interface の表現 -->
+<!-- * 実際に行なった証明 -->
+<!-- * まとめ -->
+
 
 <!-- _S9SLIDE_ -->
-<h2 id="section">本発表の流れ</h2>
+<h2 id="section">プログラムの信頼性の保証</h2>
 <ul>
-  <li>研究目的</li>
-  <li>CodeGear と DataGear の説明</li>
-  <li>Agda の記述</li>
-  <li>Interface の説明</li>
-  <li>Agda での CodeGear 、 DataGear 、 Interface の表現</li>
-  <li>実際に行なった証明</li>
-  <li>まとめ</li>
+  <li>動作するプログラムの信頼性を保証したい</li>
+  <li>保証をするためには仕様を検証する必要がある</li>
+  <li>仕様を検証するには <strong>モデル検査</strong> と <strong>定理証明</strong> の２つの手法がある
+    <ul>
+      <li><strong>モデル検査</strong> はプログラムの持つ状態を数え上げて仕様を満たしているか</li>
+      <li><strong>定理証明</strong>　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する</li>
+    </ul>
+  </li>
 </ul>
 
 
@@ -112,93 +122,48 @@
 <div class='slide '>
 <!-- _S9SLIDE_ -->
 <h2 id="section-1">プログラムの信頼性の保証</h2>
-<ul>
-  <li>動作するプログラムの信頼性を保証したい</li>
-  <li>保証をするためには仕様を検証する必要がある</li>
-  <li>仕様を検証するにはモデル検査と <strong>定理証明</strong> の２つの手法がある
-    <ul>
-      <li>モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか</li>
-      <li>定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する</li>
-    </ul>
-  </li>
-  <li>当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している</li>
-  <li>また、上記の単位で計算をノーマルレベル、メタレベルに分け、信頼性と拡張性をメタレベルで保証する GearsOS を開発している</li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="section-2">プログラムの信頼性の保証</h2>
 <!-- * データ構造を仕様と実装に分けて記述するため、GearsOS のモジュール化の仕組みである **Interface** を記述した -->
 <ul>
-  <li>CodeGear、 DataGear を使ったプログラミングは関数型プログラミングに近い形になる</li>
-  <li>本研究では関数型の <strong>定理証明支援系</strong> の言語 <strong>Agda</strong> を用いて仕様を検証することとした</li>
-  <li>Agda で CodeGear 、DataGear、という単位と Interface を定義した</li>
-  <li>CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った</li>
+  <li>当研究室では検証しやすい単位として <strong>CodeGear</strong>、<strong>DataGear</strong> という単位を用いてプログラムを記述する手法を提案している</li>
+  <li>これは関数型プログラミングに近い形になる</li>
+  <li>本研究では関数型の <strong>定理証明支援系</strong> の言語 <strong>Agda</strong> を用いて仕様を検証することにした</li>
 </ul>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="codegear--datagear-">CodeGear と DataGear の定義</h2>
+<h2 id="section-2">発表の流れ</h2>
 <ul>
-  <li>CodeGear とはプログラムを記述する際の処理の単位で、Agda では通常の関数で表現する</li>
-  <li>DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている</li>
-  <li>CodeGear はメタ計算によって次の CodeGear へ接続される</li>
-  <li>メタ計算部分では並列処理などの様々な処理を記述ができる</li>
+  <li>CodeGear と DataGear の定義</li>
+  <li>Agda の説明</li>
+  <li>Agda での CodeGear、 DataGear の表現</li>
+  <li>今回行なった証明</li>
 </ul>
 
-<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/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> -->
 
 
 </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="cbc-hoare" width="800" />
-</div>
-
-
-</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>
-
-<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>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="agda-">Agda での型</h2>
+<h2 id="agda-">Agda での型定義</h2>
 <ul>
   <li>型は <strong>関数名 : 型</strong> のように <strong>:</strong> を使って定義する</li>
   <li>a -&gt; b という型は、<strong>「a を受け取り、 b を返す」</strong>という型</li>
@@ -211,35 +176,12 @@
 <!-- _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>
@@ -381,7 +323,67 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="inteface">Inteface</h2>
+<h2 id="codegear--datagear-">CodeGear と DataGear の定義</h2>
+<ul>
+  <li>CodeGear とはプログラムを記述する際の処理の単位</li>
+  <li>DataGear は 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="gearsos">GearsOS</h2>
+<ul>
+  <li>本研究室では処理の単位を Code Gear、 データの単位を Data Gear を用いて 信頼性が高い処理を行う Gears OS を開発している</li>
+  <li>GearsOS では計算をノーマルレベルとメタレベルに階層化し、 信頼性と拡張性をメタレベルで保証している</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--codegear-datagear-">Agda での CodeGear、 DataGear の表現</h2>
+<ul>
+  <li>GearsOS の検証を行うため、CodeGear、DataGear を Agda で定義した</li>
+  <li>CodeGear は処理の単位なので、 Agda では通常関数として記述する</li>
+  <li>DataGear は Agda の record を使用し記述する</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--codegear">Agda での CodeGear</h2>
+<ul>
+  <li>例として Stack への push を考える</li>
+  <li>通常の push を normalPush と 継続を用いた push を continuePush とする</li>
+</ul>
+
+<pre lang="AGDA"><code>-- 通常のpushの型 
+normalPush : Si -&gt; a -&gt; Si
+-- 継続を用いたpushの型
+continuePush : Si -&gt; a -&gt; (CodeGear : Si -&gt; t) -&gt; t 
+</code></pre>
+
+<ul>
+  <li>normalPush は 「<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>
+  <li><strong>CodeGear の型</strong> は <strong>(code: a -&gt; t) -&gt; t</strong> のような形になる</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="interface">Interface</h2>
 <ul>
   <li>Interface は GearsOS のモジュール化の仕組み</li>
   <li>ある Data Gear と それに対する操作(API) を行う Code Gear の集合を表現</li>
--- a/Slide/sigos.md	Sun May 20 21:57:24 2018 +0900
+++ b/Slide/sigos.md	Sun May 20 23:42:24 2018 +0900
@@ -10,92 +10,65 @@
 <!-- ``` -->
 
 
-## 本発表の流れ
-* 研究目的
-* CodeGear と DataGear の説明
-* Agda の記述
-* Interface の説明
-* Agda での CodeGear 、 DataGear 、 Interface の表現
-* 実際に行なった証明
-* まとめ
+<!-- ## 本発表の流れ -->
+<!-- * 研究目的 -->
+<!-- * CodeGear と DataGear の説明 -->
+<!-- * Agda の記述 -->
+<!-- * Interface の説明 -->
+<!-- * Agda での CodeGear 、 DataGear 、 Interface の表現 -->
+<!-- * 実際に行なった証明 -->
+<!-- * まとめ -->
 
 ## プログラムの信頼性の保証
 * 動作するプログラムの信頼性を保証したい
 * 保証をするためには仕様を検証する必要がある
-* 仕様を検証するにはモデル検査と **定理証明** の２つの手法がある
-  * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか
-  * 定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
-* 当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
-* また、上記の単位で計算をノーマルレベル、メタレベルに分け、信頼性と拡張性をメタレベルで保証する GearsOS を開発している
+* 仕様を検証するには **モデル検査** と **定理証明** の２つの手法がある
+  * **モデル検査** はプログラムの持つ状態を数え上げて仕様を満たしているか
+  * **定理証明**　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
 
 ## プログラムの信頼性の保証
 <!-- * データ構造を仕様と実装に分けて記述するため、GearsOS のモジュール化の仕組みである **Interface** を記述した -->
-* CodeGear、 DataGear を使ったプログラミングは関数型プログラミングに近い形になる
-* 本研究では関数型の **定理証明支援系** の言語 **Agda** を用いて仕様を検証することとした
-* Agda で CodeGear 、DataGear、という単位と Interface を定義した
-* CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った
+* 当研究室では検証しやすい単位として **CodeGear**、**DataGear** という単位を用いてプログラムを記述する手法を提案している
+* これは関数型プログラミングに近い形になる
+* 本研究では関数型の **定理証明支援系** の言語 **Agda** を用いて仕様を検証することにした
 
-## CodeGear と DataGear の定義
-* CodeGear とはプログラムを記述する際の処理の単位で、Agda では通常の関数で表現する
-* DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている
-* CodeGear はメタ計算によって次の CodeGear へ接続される
-* メタ計算部分では並列処理などの様々な処理を記述ができる
+## 発表の流れ
+* CodeGear と DataGear の定義
+* Agda の説明
+* Agda での CodeGear、 DataGear の表現
+* 今回行なった証明
 
-<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} が成り立つとき、部分的に正当である -->
 
-## 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/cgdg.svg" alt="cbc-hoare" width="800">
-</div>
+<!-- <div style="text-align: center;"> -->
+<!--     <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 で書かれたプログラムに対して検証する
+<!-- ## 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>
+<!-- <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 での型定義
 * 型は **関数名 : 型** のように **:** を使って定義する
 * 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 を返す
@@ -187,8 +160,44 @@
 * **record** 後ろの **{}** 内部で **フィールド名 = 値** で列挙
 * 複数のフィールドを作成する際は **;** で区切る
 
-## Inteface
-* Interface は GearsOS のモジュール化の仕組み
+## CodeGear と DataGear の定義
+* CodeGear とはプログラムを記述する際の処理の単位
+* DataGear は CodeGear で扱うデータの単位
+* CodeGear はメタ計算によって次の CodeGear へ接続される
+* メタ計算部分に並列処理などの様々な処理や、検証を記述することができる
+
+<div style="text-align: center;">
+    <img src="./fig/meta_cg_dg.svg" alt="goto" width="800">
+</div>
+
+## GearsOS
+* 本研究室では処理の単位を Code Gear、 データの単位を Data Gear を用いて 信頼性が高い処理を行う Gears OS を開発している
+* GearsOS では計算をノーマルレベルとメタレベルに階層化し、 信頼性と拡張性をメタレベルで保証している
+
+
+## Agda での CodeGear、 DataGear の表現
+* GearsOS の検証を行うため、CodeGear、DataGear を Agda で定義した
+* CodeGear は処理の単位なので、 Agda では通常関数として記述する
+* DataGear は Agda の record を使用し記述する
+
+## Agda での CodeGear
+* 例として Stack への push を考える
+* 通常の push を normalPush と 継続を用いた push を continuePush とする
+
+```AGDA
+-- 通常のpushの型 
+normalPush : Si -> a -> Si
+-- 継続を用いたpushの型
+continuePush : Si -> a -> (CodeGear : Si -> t) -> t 
+```
+
+* normalPush は 「**stack** と  **data**  を受け取り、 **data が取り出された stack** を返す」型
+* continuePush は 「**stack** と **data** **と 継続先の (Code : )** を受け取り、 **継続先である t**を返す」型 
+* t は明示されていない不定な型で、継続を表している
+* **CodeGear の型** は **(code: a -> t) -> t** のような形になる
+
+## Interface
+* Interface は GearsOS でのモジュール化の仕組み
 * ある Data Gear と それに対する操作(API) を行う Code Gear の集合を表現
 * Interface を使うとデータ構造への操作を仕様と実装に分けて記述することができる