Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/intro.tex @ 8:27a6616b6683

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author soto@cr.ie.u-ryukyu.ac.jp
date Mon, 14 Sep 2020 19:58:10 +0900
parents b124f02ea3f1
children a8bc8c6b48bd
comparison
equal deleted inserted replaced
7:acad18934981 8:27a6616b6683
1 \section{研究目的} 1 \section{研究目的}
2 OS やアプリケーションの信頼性を高めることは重要な課題である。 2 OS やアプリケーションの信頼性を高めることは重要な課題である。
3 信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。 3 信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。
4 具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。 4 具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。
5 研究室で CbC という言語を開発している。
6 CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。
7 この言語の信用性を検証したい。
5 8
6 研究室で CbC という言語を開発している。 9 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。
7 CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。 10 Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、
8 この言語の信用性を検証したい。 11 に事後条件が成り立つことでコマンドの検証を行う。
9 12 この定義が CbC の実行を継続するという性質と相性が良い。
10 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。 13
11 Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、 14 CbCでは実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。
12 に事後条件が成り立つことでコマンドの検証を行う。 15 それを繋げていくので、個々の関数の
13 16 正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
14 CbC の実行を継続するという性質が Hoare Logic の事前条件と事後条件の定義から検証を行うことと非常に相性が良い。 17
15 これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。 18 % これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。
19 これらのことから、本稿では CbC に対応するようにagdaで記述し、Hoare Logic により検証を行うことを目指す。