Mercurial > hg > Papers > 2018 > nozomi-master

changeset 107:e1d3317d5789

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing slide...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 13 Feb 2017 13:47:04 +0900
parents cc2ca280345f
children 4b26c8020229 a133c32db45e
files presentation/slide.md
diffstat 1 files changed, 39 insertions(+), 78 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.md	Mon Feb 13 13:22:18 2017 +0900
+++ b/presentation/slide.md	Mon Feb 13 13:47:04 2017 +0900
@@ -21,11 +21,19 @@
     * 型システムを通して CbC の形式的な定義を得る
     * SingleLinkedStack の性質の証明
 
+# モデル検査的アプローチについての流れ
+* Continuation based C (CbC) 言語について
+* CbC における CodeSegment と DataSegment を用いたプログラミングスタイル
+* CbC とメタ計算について
+* CbC で記述された GearsOS とそのデータ構造である赤黒木
+* 赤黒木の仕様の定義とその検証手法
+
 # Continuation based C
 * 当研究室で開発しているプログラミング言語
 * アセンブラとC言語の中間のような言語であり、構文はほとんど C 言語
 * OS や組み込みソフトウェアなどを対象にしている
 * CodeSegment と DataSegment という単位を用いてプログラミングする
+* 両検証手法をメタ計算として利用可能
 
 # CodeSegment
 * CodeSegment とは
@@ -45,9 +53,9 @@
 # メタ計算
 * とある計算を実現するための計算
 * ネットワーク接続、例外処理、メモリ確保、並列処理など
-* 時に本来行ないたい処理よりも複雑になる
 * CbC は通常レベルの計算とメタ計算を分離して考える
     * 通常レベルではポインタは出てこない、など
+* CodeSegment の接続部分に処理を追加することで実現
 * TODO: 図
 
 # Meta CodeSegment
@@ -60,14 +68,6 @@
 * 通常の DataSegment を含むような DataSegment
 * TODO: 図
 
-# C言語との対応
-* CodeSegment は C 言語における返り値の無い関数
-* DataSegment は C 言語における構造体
-* Meta CodeSegment は CodeSegment の前後にある CodeSegment
-* Meta DataSegment は全ての DataSegment の共用体を持つ構造体
-* CodeSegment の接続は goto における軽量継続
-    * 末尾のみで行なうスタックを保持しない関数呼び出し
-
 # 並列に信頼性高く動作する GearsOS
 * CbC を用いたメタ計算の例として本研究室で開発している GearsOS がある
 * 並列実行やモデル検査をメタ計算として提供する
@@ -112,8 +112,9 @@
 
 # メタ計算ライブラリ akasha
 * メタ計算としてプログラムの状態を数え上げる
-* goto された時に挿入される要素の組み合わせを全て列挙して実行する
-* その度に仕様の式は成り立つかをチェックする
+    * goto された時に挿入される要素の組み合わせを全て列挙して実行する
+    * その度に仕様の式は成り立つかをチェックする
+* ノーマルレベルのコードを検証用に変更せず検証可能
 * TODO: 図
 
 # チェックする仕様
@@ -129,79 +130,39 @@
     * akasha は返した
 * 固定の要素数までの仕様検査で十分なのか?
 
-# 定理証明
+# 定理証明的なアプローチの流れ
+*
+
+# 定理証明を Continuation based C へ適用するには
 * 任意の回数だけ木の操作を行なっても大丈夫なことを保証したい
 * そのままプログラムの性質を保証してやる
-* プログラムと証明は Curry-Howard Isomorphism により、自然演繹と型付ラムダ計算が対応
-    * プログラムにおける命題は型であり、証明はその導出が存在するかどうか
-    * 例えば三段論法が書ける
-        * (A -> B) -> (B -> C) -> (A -> C)
-        * (int -> bool) -> (bool -> float) -> (int -> float)
+* Coq, Agda, ATS2 などのプログラミング言語で証明が可能
+    * 本当は CbC で CbC 自身を証明したい
+    * しかし CbC の形式的な定義が無いために今はできない
+* Agda 上に CbC を定義することで形式的な定義を得る
 
-# 証明支援系 Agda
-* 依存型を持つ言語
-    * 型が第一級(型が値である)
-    * 「型を取って型を返す型」などが定義可能
-* 定理証明が記述可能
-    * この言語の上に CbC の項を表現する
-    * Agda 経由で CbC の形式的な定義を得る
-
-# Agda 上に CbC を記述するには?
-* CbC と CbC の対応で書ける?
-    * DataSegment -> 構造体(複数の値と名前によって成り立つ)
-    * CodeSegment -> 関数型(型を取って型を返す)
-    * Meta DataSegment -> 構造体の共用体
-    * Meta CodeSegment -> 関数型?
-* Meta CodeSegment の階層構造をどう定義するか
-    * 構造体に相当するレコード型はAgdaにある
-    * 共用体に相当する直和型も定義可能
+# Agda における CodeSegment と DataSegment
+# Agda と CodeSegment
+# Agda と DataSegment
 
 # メタレベルの型付け
-* Meta CodeSegment が持っているべき性質
-    * メタレベルは階層構造を持つ
-        * メタ計算は組み合わせられる
-    * ノーマルレベルの DataSegment を一様に扱える
-    * ノーマルレベルの CodeSegment へと goto できる
-        * どんなプログラムからもライブラリとして使える
-* 構造体では融通が効かない
-    * 完全にマッチしなくてはいけない
-* TODO: ソース
-
-# 部分型
-* DataSegment が持つべき制約を表現できる型
-* 型 T が期待される文脈で S を用いても良い、というようなことができる
-    * 「S <: T」で「S は T の部分型である」と読む
-    * 全てのDataSegment に対して「MDS <: DS」となるような MDS を用意する
-* DataSegment X が期待される CodeSegment に Meta DataSegment を渡してやる
-
-# 入力の部分型
-# 出力の部分型
+* メタ計算とは通常のレベルとは区別された計算
+* 任意の通常のレベルの計算を扱えなくてはならない
+    * ライブラリが呼び出されるプログラムは無数にあるようなイメージ
+* メタレベルを使うための制約を満たしていれば良い、ということを表現できれば良い
+* 部分型を使う
+    * Java におけるインターフェース、Haskell における型クラス
+    * 「このデータにはこのフィールドさえあれば良い」
 
-# 部分型で何ができたか?
-* Meta CodeSegment を部分型とすることで
-    * ノーマルレベルの CodeSegment の前後に処理を入れても型は整合する
-    * Meta CodeSegment を CodeSegment とすることで階層構造を作れる
-* Meta DataSegment を部分型とすることで
-    * ノーマルレベルからはアクセスできないデータを保持してもOK
-    * ノーマルレベルに Meta DataSegment を渡しても良い
-    * こちらも階層構造を取ることができる
+# Agda 上の Meta CodeSegment
+# Agda 上の Meta DataSegment
 
-# SingleLinkedStack の証明
-* 証明支援系 Agda に GearsOS のデータ構造 SingleLinkedStack を定義
-    * スタックは赤黒木に用いられている
-* その性質を証明する
-    * 性質もいくつか考えられる
-    * 「push して pop するとスタックは元に戻る」
-
-# Agda を用いた証明手法
-* 基本的にはデータの構造に関する帰納法
-    * スタックは内部に SingleLinkedList を持つ
-    * SingleLinkedList は NULL か値と次のノードを持つ
-    * 値がある場合と無い場合との場合分け
-* 挿入する要素を指定せずに push を呼ぶとどうなるのか?
-    * 実装依存のコード
-    * 証明には表れる
-        * TODO: かく...
+# Agda 上に CbC を記述した成果
+* 部分型で CbC の型付けができた
+* メタ計算をきちんと階層化できた
+    * メタ計算にもメタ計算が適用可能
+* 赤黒木で利用しているデータ構造スタックの性質を証明できた
+    * 任意の回数だけ値を積んで同じだけ取り出すとスタックは変化しない
 
 # まとめ
 * Continuation based C 言語を対象にした二種類の検証アプローチ
@@ -217,7 +178,7 @@
 * 部分型を利用してCbCを型付け
 * 依存型をCbC に導入して自身を証明可能にする
 * 型情報から stub を自動生成すkる
-* 赤黒木の挿入を証明する
+* 赤黒木の挿入に関する性質を証明する
 
 <!-- vim: set filetype=markdown.slide: -->