|
3
|
1 \section{研究目的}
|
|
8
|
2 OS やアプリケーションの信頼性を高めることは重要な課題である。
|
|
11
|
3 信頼性を高める為にはプログラムが仕様を満たした実装をされていることを検証する必要がある。
|
|
8
|
4 具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。
|
|
11
|
5 当研究室では CbC という言語を開発している。
|
|
8
|
6 CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。
|
|
|
7 この言語の信用性を検証したい。
|
|
3
|
8
|
|
8
|
9 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。
|
|
|
10 Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、
|
|
11
|
11 事後条件が成り立つことでコマンドの検証を行う。
|
|
8
|
12 この定義が CbC の実行を継続するという性質と相性が良い。
|
|
|
13
|
|
|
14 CbCでは実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。
|
|
11
|
15 それを繋げていくため、個々の関数の
|
|
8
|
16 正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
|
|
|
17
|
|
11
|
18 CbCではループ制御構造を取り除いているため、CbCにてループが含まれるプログラムを作成した際の検証を行う必要がある。
|
|
|
19 先行研究ではCbCにおけるWhileLoopの検証を行なっている。
|
|
|
20
|
|
|
21 Agdaが変数への再代入を許していない為、
|
|
|
22 ループが存在し、かつ再代入がプログラムに含まれる RedBlackTree の検証を行いたい。
|
|
|
23
|
|
8
|
24 % これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。
|
|
11
|
25 これらのことから、CbC に対応するように Agda で RedBlackTree を記述し、Hoare Logic により検証を行うことを目指す。
|
