# 研究目的

• OSやアプリケーションの信頼性は重要な課題である。

  • 信頼性をあげるには「モデル検査」や「定理証明など」がある。
  • 検証手法として「Hoare Logic」がある。

• CbCはCode Gear の継続によって記述される。これにHoare Logicの部分正当性を適応させると、CbCで記述されたプログラムの検証を簡単に行うことができる。

• CbCをHoare Logicにより検証していく

# CbCについて

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

• Code / Data Gear による継続によって記述される。

# Hoare Logicについて

• プログラム検証の手法で、事前条件(P)、プログラム(Q)、及びその実行結果の説明(R)とする。

  • プログラム(Q)の開始前に事前条件(P)が真の場合、結果Rはその完了時に真となるというもの。(部分正当性)

• 普通のプログラムでは、途中で前提条件となる(P)に何が当てはまるのか正確にはわからない。しかし、CbCなら引数は前のCode Gearの結果が入ることが分かる。

• DatasegmentをPとし、CodesegmentをQ、出力されたDatasegmentをRとしてCbCの記述にHoare Logicを当てはめることでCodesegmentが部分的に正当であることが示せる。

• Code Gearの前提条件はその前の継続の結果…というようにできる。

• このように、CbCではプログラムの一部分を全てHoare Logicにより証明できたなら、その継続となるプログラムとなるので、CbCとの相性が良い。

# 今週の進捗

• 論文(axiomatic basis for computer Programming)を読んでいます。
• AtCoderで茶色になりました。

# 次

• ryokkaさんが作成したものが少し混雑しているので整頓
  • Pre condition, Post conditionのもの
  • Hoare Logicのもの

# memo

• izaverafolte?でやったものもあるっぽい（あとで調べる）