# HG changeset patch
# User ryokka
# Date 1526827344 -32400
# Node ID 7aa41769f1f12e416702f47f84894109b7688e2d
# Parent 328bcfd300bdffb6ac84c61cee8e6e179b654700
fix slides
diff -r 328bcfd300bd -r 7aa41769f1f1 Slide/sigos.html
--- 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 @@
@@ -94,17 +94,27 @@
+
+
+
+
+
+
+
+
+
-
本発表の流れ
+プログラムの信頼性の保証
- - 研究目的
- - CodeGear と DataGear の説明
- - Agda の記述
- - Interface の説明
- - Agda での CodeGear 、 DataGear 、 Interface の表現
- - 実際に行なった証明
- - まとめ
+ - 動作するプログラムの信頼性を保証したい
+ - 保証をするためには仕様を検証する必要がある
+ - 仕様を検証するには モデル検査 と 定理証明 の2つの手法がある
+
+ - モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか
+ - 定理証明 はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
+
+
@@ -112,93 +122,48 @@
プログラムの信頼性の保証
-
- - 動作するプログラムの信頼性を保証したい
- - 保証をするためには仕様を検証する必要がある
- - 仕様を検証するにはモデル検査と 定理証明 の2つの手法がある
-
- - モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか
- - 定理証明 はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
-
-
- - 当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
- - また、上記の単位で計算をノーマルレベル、メタレベルに分け、信頼性と拡張性をメタレベルで保証する GearsOS を開発している
-
-
-
-
-
-
-
プログラムの信頼性の保証
- - 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 の表現
+ - 今回行なった証明
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
Hoare Logic
-
- - Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証する手法
- - 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) で変更する
- - {P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である
-
-
-
-
-
-
-
-
-
-
-
Hoare Logic と CodeGear、 DataGear
-
- - Hoare Logic の状態と処理を CodeGear、 DataGear に当てはめる事ができる
- - Pre-condition を input の DataGear , Post-Conditon を output の DataGear , Command は CodeGear そのもの
- - Pre-conditon や Post-conditon をメタ計算部分で検証し、 CodeGear、 DataGear で書かれたプログラムに対して検証する
-
-
-
-
-
-
-
-
-
-
-
Agda での CodeGear、 DataGear の表現
-
- - CodeGear は処理の単位なので、 Agda では通常関数として記述する
- - DataGear は Agda の record を使用し記述する
-
-
-
-
-
-
-
Agda での型
+
Agda での型定義
- 型は 関数名 : 型 のように : を使って定義する
- a -> b という型は、「a を受け取り、 b を返す」という型
@@ -211,35 +176,12 @@
Agda での型(例)
- - CodeGear の型 は (code: a -> t) -> t のような形になる
- - 例として通常の push (nomalPush) と 継続を用いた push (continuePush) の型を考える
-
-
-
-- 通常の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 の型を見る
popSingleLinkedStack : SingleLinkedStack a ->
(Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
-
- この型では stack と行き先の CodeGear を受け取り、次の CodeGear に継続する
- popSingleLinkedStack 継続に型 Maybe a を受けとる CodeGear ( (fa -> t) -> t) に渡している
@@ -381,7 +323,67 @@
-
Inteface
+
CodeGear と DataGear の定義
+
+ - CodeGear とはプログラムを記述する際の処理の単位
+ - DataGear は CodeGear で扱うデータの単位
+ - CodeGear はメタ計算によって次の CodeGear へ接続される
+ - メタ計算部分に並列処理などの様々な処理や、検証を記述することができる
+
+
+
+
+
+
+
+
+
+
+
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 とする
+
+
+
-- 通常の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 の集合を表現
diff -r 328bcfd300bd -r 7aa41769f1f1 Slide/sigos.md
--- 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 の表現
-* 実際に行なった証明
-* まとめ
+
+
+
+
+
+
+
+
## プログラムの信頼性の保証
* 動作するプログラムの信頼性を保証したい
* 保証をするためには仕様を検証する必要がある
-* 仕様を検証するにはモデル検査と **定理証明** の2つの手法がある
- * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか
- * 定理証明 はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
-* 当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
-* また、上記の単位で計算をノーマルレベル、メタレベルに分け、信頼性と拡張性をメタレベルで保証する GearsOS を開発している
+* 仕様を検証するには **モデル検査** と **定理証明** の2つの手法がある
+ * **モデル検査** はプログラムの持つ状態を数え上げて仕様を満たしているか
+ * **定理証明** はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
## プログラムの信頼性の保証
-* 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 の表現
+* 今回行なった証明
-
-
-
+
+
+
+
-## Hoare Logic
-* Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証する手法
-* 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) で変更する
-* {P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である
-
-
-
-
+
+
+
-## Hoare Logic と CodeGear、 DataGear
-* Hoare Logic の状態と処理を CodeGear、 DataGear に当てはめる事ができる
-* Pre-condition を input の DataGear , Post-Conditon を output の DataGear , Command は CodeGear そのもの
-* Pre-conditon や Post-conditon をメタ計算部分で検証し、 CodeGear、 DataGear で書かれたプログラムに対して検証する
+
+
+
+
-
-
-
+
+
+
-## 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 へ接続される
+* メタ計算部分に並列処理などの様々な処理や、検証を記述することができる
+
+
+
+
+
+## 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 を使うとデータ構造への操作を仕様と実装に分けて記述することができる