--- a/paper/akasha.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/akasha.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -7,7 +7,7 @@
 \section{モデル検査}
 モデル検査とは、ソフトウェアの全ての状態において仕様が満たされるかを確認するものである。
 このモデル検査を行なうソフトウェアをモデル検査器と呼ぶ。
-モデルは検査器は、仕様の定義と確認ができる。
+モデルは検査器は、仕様の定義とその検証ができる。
 加えて、仕様を満たさない場合にはソフトウェアがどのような状態であったか反例を返す。
 
 モデル検査器には Spin\cite{spin} やCBMC\cite{cbmc} などが存在する。
@@ -82,8 +82,8 @@
 CAS(Check and Set) とは、アトミックに値を置き換える操作であり、使う際は更新前の値と更新後の値を渡す。
 CAS で渡された更新前の値が、保存している値と同じであれば競合していないために値の更新に成功し、異なる場合は他に書き込みがあったことを示すために値の更新が失敗する操作のことである。
 
-非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとする。
-この際に変更が行なわれていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。
+非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとすることである。
+この際に変更されていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。
 これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。
 
 \begin{figure}[htbp]
@@ -145,7 +145,7 @@
 操作を挿入に限定し、どのような順番で要素を挿入しても木がバランスすることを検証する。
 検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。
 
-akasha では仕様は常に成り立つべき CbC の条件式として定義される。
+akasha では仕様は常に成り立つべき CbC の条件式として定義する。
 具体的には Meta CodeSegment に定義した assert が仕様に相当する。
 仕様の例として「木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる」という式を定義する(リスト\ref{src:assert})。