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