# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486968285 -32400
# Node ID 2e30ed0e26330848774f4a45082027c67dea2b0a
# Parent  4e30a8a7128c561399c21dba2a5d8114d1d006f6
Fix akasha

diff -r 4e30a8a7128c -r 2e30ed0e2633 paper/abstract.tex
--- a/paper/abstract.tex	Mon Feb 13 15:00:06 2017 +0900
+++ b/paper/abstract.tex	Mon Feb 13 15:44:45 2017 +0900
@@ -4,8 +4,8 @@
 特に実際に動作するソフトウェアを検証や証明できるとなお良い。
 本論文では 検証や証明に直接使用することができる言語として Continuation based C(CbC) 言語を用いる。
 
-CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法を提案し、メタ計算ライブラリ Akasha として実装した。
-Akasha では赤黒木の仕様を、限定的な木の大きさの範囲内で検証した。
+CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法を提案し、メタ計算ライブラリ akasha として実装した。
+akasha では赤黒木の仕様を、限定的な木の大きさの範囲内で検証した。
 
 木の大きさを制限せず実装が仕様を満たすことを示すには証明が必要である。
 プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。
@@ -22,7 +22,7 @@
 In this paper, we use Continuation base C programming language (CbC) which can be used in both model checking and proof.
 
 We propose model checking method by enumerating bounded computational state in CbC code as a meta computation.
-Akasha Meta Computation library makes it possible to check red-black tree algorithm within a bounded tree size.
+Akasha meta computation library makes it possible to check red-black tree algorithm within a bounded tree size.
 
 To assure the property for arbitrary size of trees, we need proof method.
 Proofs in a program are known to correspond $\lambda$ calculus, which is a Curry-Howward Isomorphism.