Mercurial > hg > Papers > 2017 > atton-master
changeset 113:2e30ed0e2633
Fix akasha
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 13 Feb 2017 15:44:45 +0900 |
| parents | 4e30a8a7128c |
| children | 5cca315b0230 |
| files | paper/abstract.tex |
| diffstat | 1 files changed, 3 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- 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.