\section{研究目的}
OSやアプリケーションの信頼性を高めることは重要な課題である。
信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。
具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。

当研究室では Continuation based C (CbC) という言語を開発している。
CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、
継続を導入した C言語の下位言語である。
その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。

CbCでは実行を継続するため、ある関数の実行結果は事後条件になるが、
その実行結果が遷移する次の関数の事前条件になる。
それを繋げていくため、個々の関数の
正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。

CbCではループ制御構造を取り除いているため、
CbCにてループが含まれるプログラムを作成した際の検証を行う必要がある。
先行研究ではCbCにおけるWhileLoopの検証を行なっている。

Agdaが変数への再代入を許していない為、
ループが存在し、かつ再代入がプログラムに含まれる RedBlackTree の検証を行いたい。