Mercurial > hg > Members > atton > seminar_slides
annotate slides/20161213/slide.md @ 163:b8e16c48a5a4 default tip
Update template
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 17 Jan 2017 17:18:41 +0900 |
parents | 6e4a6421f168 |
children |
rev | line source |
---|---|
157
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 title: Verification method of programs using Continuation based C |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 author: Yasutaka Higa |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 profile: |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 lang: Japanese |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 # 研究目的 |
158 | 7 * 動作するプログラムの信頼性を保証したい |
8 * 検証を行ないやすい単位としてプログラムをコードセグメントとデータセグメントという単位で記述する | |
157
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 * プログラムはコードセグメントという処理の集合として表され、相互に接続される |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 * 型検査器を導入することでコードセグメントが接続可能かどうかを判断する |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 * また、コードセグメントの型から推論してデータセグメントの生成を行なう |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 # 研究内容 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 * コードセグメントとデータセグメントを用いて記述する言語 Continuation based C に型を導入する |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 * コードセグメント内部の演算と変数代入から型を推論する |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 * 接続可能かどうかをコンパイル時に判断し、必要なデータセグメントを型情報から生成する |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 # 近況報告 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 * Gears の Stack の証明をこねてました |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 * 任意の Stack に対して n回 push した後に n回 pop したら元に戻る |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 * 空の Stack に対しても同様 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 * Gears の型をどうするかのアイデア |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 # Type of Gears |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 * CodeSegment のは DataSegment -> DataSegment |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 * DataSegment は制約か部分型 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 * 合成できるのならOK |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 * 全ての部分型を満たすものが最初の引数になるのでそれを生成できれば良い |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 * 関数合成部分を切り替え可能なメタ計算にする |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 * Allocate とかも書けそう |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 # 問題点 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 * どう書くか/書けるのか |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 * goto の分岐 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 * 総称型に拡張可能かどうか |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 * 並列実行はどう書くのか |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 * まだAPIが無い |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 |
4c1b25782208
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 <!-- vim: set filetype=markdown.slide: --> |