annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
3dba680da508 init-test
soto
parents:
diff changeset
1 \section{研究目的}
13
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
2 OSやアプリケーションの信頼性を高めることは重要な課題である。
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
3 信頼性を高める為にはプログラムが仕様を満たした実装を検証する必要がある。
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
4 具体的には「モデル検査」や「定理証明」などが検証手法としてあげられる。
0
3dba680da508 init-test
soto
parents:
diff changeset
5
13
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
6 当研究室では Continuation based C (CbC) という言語を開発している。
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
7 CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
8 継続を導入した C言語の下位言語である。
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
9 その為、それを実装した際のプログラムが正確に動作するのか検証を行いたい。
0
3dba680da508 init-test
soto
parents:
diff changeset
10
13
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
11 CbCでは実行を継続するため、ある関数の実行結果は事後条件になるが、
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
12 その実行結果が遷移する次の関数の事前条件になる。
0
3dba680da508 init-test
soto
parents:
diff changeset
13 それを繋げていくため、個々の関数の
3dba680da508 init-test
soto
parents:
diff changeset
14 正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
3dba680da508 init-test
soto
parents:
diff changeset
15
13
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
16 CbCではループ制御構造を取り除いているため、
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
17 CbCにてループが含まれるプログラムを作成した際の検証を行う必要がある。
0
3dba680da508 init-test
soto
parents:
diff changeset
18 先行研究ではCbCにおけるWhileLoopの検証を行なっている。
3dba680da508 init-test
soto
parents:
diff changeset
19
3dba680da508 init-test
soto
parents:
diff changeset
20 Agdaが変数への再代入を許していない為、
13
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
21 ループが存在し、かつ再代入がプログラムに含まれる RedBlackTree の検証を行いたい。