--- a/tex/hoare.tex	Mon Sep 14 02:58:14 2020 +0900
+++ b/tex/hoare.tex	Mon Sep 14 05:41:23 2020 +0900
@@ -1,13 +1,20 @@
 \section{Hoare Logic}
-	Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
-	これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
-	というもので、CbCの実行を継続するという性質に非常に相性が良い。
-	Hoare Logic を表記すると以下のようになる。
-    {P} C {Q}
-	この3つ組は Hoare Triple と呼ばれる。
+Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。
+これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」
+というもので、CbCの実行を継続するという性質に非常に相性が良い。
+Hoare Logic を表記すると以下のようになる。
+{P} C {Q}
+この3つ組は Hoare Triple と呼ばれる。
+
+Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
 
-	Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。
+Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
+これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
+
 
-	Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
-	これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
+\begin{center}
+\includegraphics[height=3.5cm]{pic/hoare_cg_dg.pdf}
+\caption{CodeGear、DataGear での Hoare Logic}
+\label{hoare}
+\end{center}