# 研究目的

CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。
CbCの信頼性を検証したい。
ホーア理論の定義に部分正当性と正当性というものがある。事前条件（precondition） P が成り立つときに、プログラム S を実行して、それが停止した場合においては必ず事後条件（postcondition） Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して部分的に正当（partially correct）と言う。
DatasegmentをPとし、CodesegmentをS、出力されたDatasegmentをQとしてCbCの記述にHoare Logicを当てはめることでCodesegmentが部分的に正当であることが示せる。
Hoare Logicの定義に正当性(correctness)と言うものがある。プログラム S が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという。
- これについてryokkaさんが修論でCbCでのループ文を検証した

# 今週やったこと

研究目的を書くために論文などを調査
- Continuation based C での Hoare Logic を用いた仕様記述と検証
- 継続を基本とする言語CbCによる分散プログラミング
- 継続を基本とするC言語CbCのご紹介
- An Axiomatic Basis for Computer Programming(途中)