# 研究目的
- OSやアプリケーションの信頼性は重要な課題である。

- 研究室でCbCという言語を開発している。その信頼性を証明したい。

- CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。

- プログラムの正当性を証明するためにHoare Logicという検証手法がある。これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というもので、CbCの実行を継続するという性質に非常に相性が良い。

- これらのことから、Hoare Logicを用いてCbCを検証できるか実験していく。

# 今週の進捗
- btの実装と睨めっこしてました。

# 近況として
- バイトを2ヶ月ほど休む交渉をしてきました。
- ただ、そろそろ保険管理センターのバイトが始まります…
- あとはOOLのSDNプログラムも始まります…

# 来週は
- btの実装を読む