--- a/slide/slide.md	Tue Jan 15 17:47:18 2019 +0900
+++ b/slide/slide.md	Tue Jan 15 17:59:14 2019 +0900
@@ -1,24 +1,25 @@
 title: GearsOS の Hoare Logic を用いた検証
-author: Masataka Hokama
+author: 外間政尊 : 河野真治
 profile: 琉球大学 : 並列信頼研究室
 lang: Japanese
 
 <!-- 発表20分、質疑応答5分 -->
 
-## 研究背景
+## OS の検証技術としての HoareLogic の問題点
 - OS やアプリケーションなどの信頼性は重要な課題
 - 信頼性を上げるために仕様を検証する必要
 - 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある
   - 事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす
-- 既存の言語ではあまり利用されていない
+- OS の検証などで使われているが、実装の記述の他に関数型の記述が必要となる
+- HoareLogic の単位である代入や、WhileLoop に対応する分解が煩雑 
 
-## 背景
+## GearsOS によるメタ計算としての HoareLogic の導入
 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案
 - CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
-<!-- - Gear 間の接続処理はメタ計算として定義 -->
-<!--   - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証 -->
 - この単位を用いて信頼性の高い OS として GearsOS を開発している
-- 本発表では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する
+- Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する
+- CodeGear は CbC により、C と同等の速度で実行可能かつ Agda の継続記述にもなっている
+- 変換を必要とせずに HoareLogic による証明をメタ計算として記述できる
 
 
 ## Gears について
@@ -33,19 +34,6 @@
 <!-- ![cgdg](./pic/codeGear_dataGear.pdf){} -->
 <!-- <p style="text-align:center;"><img src="./pic/cgdg.svg" alt=""  width="30%" height="30%"/></p> -->
 
-## CbC について
-- Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在
-  - これは C からループ制御構造と関数呼び出しを取り除き、代わりに継続を導入したもの
-- 現在の CbC でもメタ計算での検証は可能
-- 将来的には証明も扱えるようにしたいが現段階では未実装
-- そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している
-
-## Agda とは
-- Agda は定理証明支援系の言語
-- 依存型を持つ関数型言語
-- Curry-Howard の証明支援系
-- 型と値がある
-- Agda の文法については次のスライドから軽く説明する
 
 ## Agda での Gears の記述(whileLoop)
 - Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数