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