Mercurial > hg > Document > Growi
view user/soto/log/2020-07-07.md @ 49:fae0d5b27a2d
backup 2021-03-24
author | autobackup |
---|---|
date | Wed, 24 Mar 2021 00:10:03 +0900 (2021-03-23) |
parents | e12992dca4a0 |
children |
line wrap: on
line source
# 研究目的 - OSやアプリケーションの信頼性は重要な課題である。 - 研究室でCbCという言語を開発している。その信頼性を証明したい。 - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。 - プログラムの正当性を証明するためにHoare Logicという検証手法がある。これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というもので、CbCの実行を継続するという性質に非常に相性が良い。 - これらのことから、Hoare Logicを用いてCbCを検証できるか実験していく。 # 今週の進捗 - btの実装と睨めっこしてました。 # 近況として - バイトを2ヶ月ほど休む交渉をしてきました。 - ただ、そろそろ保険管理センターのバイトが始まります… - あとはOOLのSDNプログラムも始まります… # 来週は - btの実装を読む