\chapter{プログラミング言語の検証}
\pagenumbering{arabic}

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

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

%\section{研究目的}
仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。
Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、
事後条件が成り立つことでコマンドの検証を行う。
この定義が CbC の実行を継続するという性質と相性が良い。

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

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

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

% これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。
これらのことから、CbC に対応するように Agda で RedBlackTree を記述し、
Hoare Logic により検証を行うことを目指す。

\begin{comment}
\section{論文の構成}
本論文は以下の流れで構成されている。

\begin{itemize}
\item 第1章は, 本研究の背景と目的を述べる
\item 第2章は, 検証を行う CbC について述べる
\item 第3章は, 証明に使用する言語である Agda について述べる
\item 第4章は, 検証手法である Hoare Logic について述べる
\item 第5章は, Agda を Continuation style で記述する方法について述べる
\item 第6章は, Red Back Tree について述べる
\item 第7章は、Agda での Red Black Tree の実装方法について述べる
\item 第8章は、Red Black Tree の Hoare Logic を用いた検証について述べる
\item 第9章は, 本研究におけるまとめと今後の課題について述べる
\end{itemize}

\end{comment}