Mercurial > hg > Papers > 2022 > soto-sigos

annotate Paper/tex/intro/intro.tex @ 0:14a0e409d574

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD fast commit
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 24 Apr 2022 23:13:44 +0900
parents
children 9ec2d2ac1309
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \section{研究目的}
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 OS やアプリケーションの信頼性を高めることは重要な課題である。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 研究室で CbC という言語を開発している。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 この言語の信用性を検証したい。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 に事後条件が成り立つことでコマンドの検証を行う。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 CbC の実行を継続するという性質が Hoare Logic の事前条件と事後条件の定義から検証を行うことと非常に相性が良い。
14a0e409d574 ADD fast commit
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。