Mercurial > hg > Papers > 2020 > soto-midterm

annotate tex/hoare.tex @ 3:b124f02ea3f1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
post agda code
author soto@cr.ie.u-ryukyu.ac.jp
date Wed, 09 Sep 2020 22:07:32 +0900
parents
children acad18934981
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
1 \section{Hoare Logic}
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
2 Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
3 これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
4 というもので、CbCの実行を継続するという性質に非常に相性が良い。
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
5 Hoare Logic を表記すると以下のようになる。
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
6 {P} C {Q}
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
7 この3つ組は Hoare Triple と呼ばれる。
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
8
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
9 Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
10
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
11 Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
12 これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
b124f02ea3f1 post agda code
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
13