--- a/Paper/tex/abst.tex	Wed Feb 01 22:16:45 2023 +0900
+++ b/Paper/tex/abst.tex	Thu Feb 02 17:49:33 2023 +0900
@@ -1,29 +1,30 @@
 \chapter*{要旨}
+
 開発手法の一つとして，形式手法というものがある．
 形式手法とはプログラムの仕様を形式化，つまり数学的な記述を行い，
-書いたプログラムがそれを満たしているか検証を行う手法である．
+書いたプログラムがそれを満たしているか検証を行う開発手法である．
 代表的な形式の検証手法として，定理証明やモデル検査が挙げられる．
 
-形式手法で開発したプログラムは数学的に正しいことが証明されている，
+形式手法で開発したプログラムは数学的に正しいことが証明されている.
 そのため高い安全性が必要とされる鉄道や電力などのインフラ分野に使用されている．
-しかし,一見完璧な手法であるように思えるが欠点として，膨大なコストを要する．
-シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用せずとも良いとなる．
+一見完璧な手法であるように思えるが欠点として，形式化や検証が複雑なため膨大なコストを要する．
+シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用する利点が薄くなる．
 
-そのため，他のプログラミング言語と比べて検証に適しているGears Agdaを使用する．
-Gears Agdaとは当研究室で開発している Continuation based C (CbC) の概念を
-取り入れた記法で記述された Agdaのことである．
+そのため，他のプログラミング言語と比べて検証に適している Gears Agda を使用する．
+Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を
+取り入れた記法で記述された定理証明支援器 Agda のことである．
 
 定理証明によるプログラムの検証は一般的に難易度が高いが，
 Gears Agda では検証をプログラム単位に分割することができ，比較的容易に検証を行えるようになっている．
 
 先行研究では implies を用いて Hoare Logic での定理証明を行っていた.
-しかしそれでは記述が長く,かつ複雑になってしまっていた.
-そこで今回は Invariant というプログラムの不変条件を新たに取り入れた.これを検証しながら実行を行うことで,Hoare Logic を用いた定理証明を比較的簡単に行えるようになった.
+しかし、それでは記述が長く複雑になっていた.
+そこで今回は Invariant というプログラムの不変条件を新たに取り入れた.これを検証しながら実行をすることで,Hoare Logic を用いた定理証明を比較的簡単に行えるようになった.
 
-また，定理証明では並行処理の検証は困難である.
+また，定理証明では並列処理の検証は困難である。出現する状態を一度全て出してからそれらの検証を行わないといけないためである。
 そのため，もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした．
 
-これらのことから，本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる
+これらのことから，本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる。
 
 \chapter*{Abstract}
 One of the development methods is called formal methods.