Mercurial > hg > Papers > 2020 > soto-midterm
annotate tex/intro.tex @ 3:b124f02ea3f1
post agda code
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Wed, 09 Sep 2020 22:07:32 +0900 |
| parents | |
| children | 27a6616b6683 |
| rev | line source |
|---|---|
| 3 | 1 \section{研究目的} |
| 2 OS やアプリケーションの信頼性を高めることは重要な課題である。 | |
| 3 信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。 | |
| 4 具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。 | |
| 5 | |
| 6 研究室で CbC という言語を開発している。 | |
| 7 CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。 | |
| 8 この言語の信用性を検証したい。 | |
| 9 | |
| 10 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。 | |
| 11 Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、 | |
| 12 に事後条件が成り立つことでコマンドの検証を行う。 | |
| 13 | |
| 14 CbC の実行を継続するという性質が Hoare Logic の事前条件と事後条件の定義から検証を行うことと非常に相性が良い。 | |
| 15 これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。 |