Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/intro.tex @ 11:a8bc8c6b48bd default tip

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