Mercurial > hg > Members > atton > seminar_slides

annotate slides/20160503/slide.md @ 140:fc3efb313753

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Regenerate slide
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 May 2016 17:54:03 +0900
parents 66b84be220db
children 711edad8adc2
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
138
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Verification of programs using Continuation based C
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 profile:
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 # 研究目的
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 # 研究内容
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 * コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 * コードセグメントどうしの接続の間にメタ計算として検証機構を導入する
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * コードを検証用に変更することなく、仕様を満たすか検証する
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * 検証の対象として Gears OS のデータ構造を用いる
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 # 近況報告
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 * SWoPP のネタ
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * Gears のデータ構造の検証
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 * Operational Semantics of CbC
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 * 発表申込締切が 2016/05/13 あたりなので来週くらいに発表アブストを持ってきます
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 # Gears のデータ構造の検証
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 * Red-Black Tree
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 * insertion の全探索は13要素までOK
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 * 6,227,020,800 通り
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 * Synchronized Queue
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 * bounded queue
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 * 各 thread が取りえる操作を全探索
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 * unbounded queue
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 * アイデア: 0, 1, 2 以上で抽象化
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 # Operational Semantics of CbC
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 * Agda で CbC を書けるか
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 * memory allocation 部分とかは meta に押しつけて書く
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 * 待ちあわせとかも無い
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 * cs は ds -> ds
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 * それだと行き先情報が無いので
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 * ds に next を含める or State Monad 辺りでやってみる
139
66b84be220db Regenerate slide
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
41 * Agda を 2.5.1 に上げて State Monad を書いてみてます
138
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
fd3b93df28e8 Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 <!-- vim: set filetype=markdown.slide: -->