--- a/paper/abstract.tex	Thu Jan 16 19:21:45 2020 +0900
+++ b/paper/abstract.tex	Mon Jan 27 20:41:36 2020 +0900
@@ -1,11 +1,11 @@
 \chapter*{要旨}
+
 OS やアプリケーションの信頼性は重要である。
 信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。
 プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。
 HoareLogic は事前条件が成り立っているときにある
-関数を実行して、それが停止する際に事後条件を満た
-すことを確認することで、検証を行う。
-HoareLogic はシンプルなアプローチであるが通常のプログラミング言語で使用することができず、
+関数を実行して、それが停止する際に事後条件を満たすことを確認することで、検証を行う。
+しかし、 HoareLogic はシンプルなアプローチであるが通常のプログラミング言語で使用することができず、
 広まっているとはいえない。
 
 当研究室では信頼性の高い OS として GearsOS を開発している。
@@ -22,5 +22,6 @@
 
 本研究では Agda 上での HoareLogic の記述を使い、簡単な while Loop のプログラムの作成、証明を行った。
 また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと
-したwhile Loop プログラムを記述、その証明を行なった。
+した while Loop プログラムを記述、その証明を行なった。
+
 \chapter*{Abstract}