--- a/Slide/prosym.html	Wed Jan 17 13:26:35 2018 +0900
+++ b/Slide/prosym.html	Thu Jan 18 09:27:32 2018 +0900
@@ -86,32 +86,74 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.4.0 (2016-12-24) [x86_64-darwin16]
-                on 2018-01-16 18:50:54 +0900 with Markdown engine kramdown (1.13.2)
+                on 2018-01-18 09:19:07 +0900 with Markdown engine kramdown (1.13.2)
                   using options {}
   -->
 
 <!-- _S9SLIDE_ -->
-<h1 id="os-">OS の拡張性と信頼性の両立</h1>
+<h1 id="gears-os">Gears OS</h1>
+
+<ul>
+  <li>
+    <p>現代の OS では拡張性と信頼性を両立させることが要求されている。
+<!--信頼性 信頼性を保証するには従来のテストとデバッグでは不十分-->
+<!--信頼性を保証するには証明とモデル検査を用いる方法がある--></p>
+  </li>
+  <li>
+    <p>信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。</p>
+  </li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section">メタレベルの計算</h1>
 
-<p>さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。
+<ul>
+  <li>プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理やスレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。これらの計算をメタ計算と呼ぶ。</li>
+  <li>メタ計算をノーマルレベルの計算から切り離して記述したい。</li>
+  <li>本研究ではノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C を用いる。</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="continuation-based-c-cbc">Continuation based C (CbC)</h1>
+<!--
+Gears OS は Continuation based C ^\(CbC)によってアプリケーションと OS そのものを記述する。
+
+CbCはノーマルレベルではメタ構造を直接見ることはなく、継続を用いた関数型プログラミングに見える。
+メタレベルから見た Data Gear をノーマルレベルの Code Gear に接続するには stub という Meta Code Gear を用いる。
+stub と Meta はユーザーレベル Code Gear / Data Gear からスクリプトにより作成される。
+
+ノーマルレベルからメタレベルを含んだコードへの変換に必要な情報はプログラムを構成する Code Gear と Data Gear の集まりから得る。
+この集まりを Interface として定義している。
+本研究では、Interfaceを用いたプログラミングと、メタ計算の実例を示す。
+
+# OS の拡張性と信頼性の両立
+
+さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。
 時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。
 その信頼性を保証するには、従来の テストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。
 これに対処するため には、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
 検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。
 このため信頼性と拡張性を両立させることが重要である。
-&lt;!–プログラムからデータを分離して扱うデータベースには、
-プログラム中のデータ構造とRDBの表構造のずれにより、<u>インピーダンスミスマッチ</u>という問題がある。</p>
+-->
+<!--プログラムからデータを分離して扱うデータベースには、
+プログラム中のデータ構造とRDBの表構造のずれにより、<u>インピーダンスミスマッチ</u>という問題がある。
 
-<p>データベースのレコードをプログラム中のオブジェクトとして使える<u>OR Mapper</u>や、
-データベース自体も、表に特化したKey Value Storeや、Jsonなどの不定形のデータ構造を格納するように機能拡張されてきている。</p>
+データベースのレコードをプログラム中のオブジェクトとして使える<u>OR Mapper</u>や、
+データベース自体も、表に特化したKey Value Storeや、Jsonなどの不定形のデータ構造を格納するように機能拡張されてきている。
 
-<p>しかし、プログラム中のデータは複雑な構造をメモリ上に構築しており、これらの方法でもまだギャップがある。–&gt;</p>
+しかし、プログラム中のデータは複雑な構造をメモリ上に構築しており、これらの方法でもまだギャップがある。-->
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section">メタ計算の重要性</h1>
+<h1 id="section-1">メタ計算の重要性</h1>
 <ul lang="Code_Gear">
   <li>プログラムを記述する際、ノーマルな処理の他に、メモリ管理やスレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。これらの計算をメタ計算と呼ぶ。</li>
   <li>メタ計算はノーマルな計算から切り離して記述したい。</li>
@@ -282,13 +324,13 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-1">比較</h1>
+<h1 id="section-2">比較</h1>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">今後の課題</h1>
+<h1 id="section-3">今後の課題</h1>
 <ul>
   <li>本研究では interface の記述、CbC ファイルから Gears OS の記述に必要な Context と stub の生成を行う perl スクリプトの生成を行なった。</li>
   <li>これにより Gears OS のコードの煩雑さは改善され、ユーザーは Context への接続を意識する必要がなくなった。</li>

--- a/Slide/prosym.md	Wed Jan 17 13:26:35 2018 +0900
+++ b/Slide/prosym.md	Thu Jan 18 09:27:32 2018 +0900
@@ -4,14 +4,14 @@
 lang: Japanese
 code-engine: coderay
 
-<!--
-# 研究目的
+# Gears OS
 
-現代の OS では拡張性と信頼性を両立させることが要求されている。
+- 現代の OS では拡張性と信頼性を両立させることが要求されている。
 <!--信頼性 信頼性を保証するには従来のテストとデバッグでは不十分-->
 <!--信頼性を保証するには証明とモデル検査を用いる方法がある-->
 
-信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。
+- 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。
+<!--
 Gears OS は Continuation based C ^\(CbC)によってアプリケーションと OS そのものを記述する。
 
 CbCはノーマルレベルではメタ構造を直接見ることはなく、継続を用いた関数型プログラミングに見える。
@@ -21,7 +21,6 @@
 ノーマルレベルからメタレベルを含んだコードへの変換に必要な情報はプログラムを構成する Code Gear と Data Gear の集まりから得る。
 この集まりを Interface として定義している。
 本研究では、Interfaceを用いたプログラミングと、メタ計算の実例を示す。
--->
 
 # OS の拡張性と信頼性の両立
 
@@ -31,6 +30,7 @@
 これに対処するため には、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
 検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。
 このため信頼性と拡張性を両立させることが重要である。
+-->
 <!--プログラムからデータを分離して扱うデータベースには、
 プログラム中のデータ構造とRDBの表構造のずれにより、<u>インピーダンスミスマッチ</u>という問題がある。
 
@@ -40,13 +40,16 @@
 しかし、プログラム中のデータは複雑な構造をメモリ上に構築しており、これらの方法でもまだギャップがある。-->
 
 # メタ計算の重要性
-- プログラムを記述する際、ノーマルな処理の他に、メモリ管理やスレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。これらの計算をメタ計算と呼ぶ。
-- メタ計算はノーマルな計算から切り離して記述したい。
+- プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理やスレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。これらの計算をメタ計算と呼ぶ。
+- メタ計算はノーマルレベルの計算から切り離して記述したい。
 - そのためには処理を細かく分割する必要があるが、関数やクラスなどの単位は容易に分割できない。
 - そこで当研究室ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を提案している。
+
 # Continuation based C (CbC) 
 - Continuation based C (CbC) はこの Code Gear 単位を用いたプログラミング言語として開発している。
 - CbC では Code Gear は \_\_code という型を持つ関数の構文で定義される。
+
+# CbC のコード例
 - Code Gear は戻り値を持たないので、関数とは異なり return 文は存在しない。
 - goto の後に Code Gear 名と引数を並べて、次の Code Gear の遷移を記述する。
 - この goto の行き先を継続と呼び、このときの a+b が次の Code Gear への出力となる。