Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/hoare.tex @ 7:acad18934981

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add description of rbtree
author soto@cr.ie.u-ryukyu.ac.jp
date Mon, 14 Sep 2020 05:41:23 +0900
parents b124f02ea3f1
children 27a6616b6683
comparison
equal deleted inserted replaced
6:4bf00f7ba825 7:acad18934981
1 \section{Hoare Logic} 1 \section{Hoare Logic}
2 Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。 2 Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
3 これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」 3 これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
4 というもので、CbCの実行を継続するという性質に非常に相性が良い。 4 というもので、CbCの実行を継続するという性質に非常に相性が良い。
5 Hoare Logic を表記すると以下のようになる。 5 Hoare Logic を表記すると以下のようになる。
6 {P} C {Q} 6 {P} C {Q}
7 この3つ組は Hoare Triple と呼ばれる。 7 この3つ組は Hoare Triple と呼ばれる。
8 8
9 Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。 9 Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
10 10
11 Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。 11 Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
12 これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。 12 これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
13 13
14
15 \begin{center}
16 \includegraphics[height=3.5cm]{pic/hoare_cg_dg.pdf}
17 \caption{CodeGear、DataGear での Hoare Logic}
18 \label{hoare}
19 \end{center}
20