Mercurial > hg > Document > Growi

annotate user/soto/log/2020-07-07.md @ 49:fae0d5b27a2d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
backup 2021-03-24
author autobackup
date Wed, 24 Mar 2021 00:10:03 +0900
parents e12992dca4a0
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 # 研究目的
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 - OSやアプリケーションの信頼性は重要な課題である。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 - 研究室でCbCという言語を開発している。その信頼性を証明したい。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 - プログラムの正当性を証明するためにHoare Logicという検証手法がある。これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というもので、CbCの実行を継続するという性質に非常に相性が良い。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 - これらのことから、Hoare Logicを用いてCbCを検証できるか実験していく。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 # 今週の進捗
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 - btの実装と睨めっこしてました。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 # 近況として
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 - バイトを2ヶ月ほど休む交渉をしてきました。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 - ただ、そろそろ保険管理センターのバイトが始まります…
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 - あとはOOLのSDNプログラムも始まります…
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 # 来週は
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 - btの実装を読む