changeset 98:42f463ef7bb2

Update abstract
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 12 Feb 2017 10:45:45 +0900
parents 5a354cba3694
children a891d7551bbf
files paper/abstract.tex paper/abstract_eng.tex paper/atton-master.pdf paper/atton-master.tex
diffstat 4 files changed, 20 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/paper/abstract.tex	Fri Feb 10 17:22:00 2017 +0900
+++ b/paper/abstract.tex	Sun Feb 12 10:45:45 2017 +0900
@@ -1,44 +1,33 @@
 \begin{abstract}
 高い信頼性を持つソフトウェアを提供することは重要である。
-それには、ソフトウェアが期待される仕様を満たすか検査する手法と、
-仕様を直接証明する手法とがある。
+それには、ソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。
 特に実際に動作するソフトウェアを検証や証明できるとなお良い。
-本論文では 検証や証明に直接使用することができる言語として
-Continuation based C(CbC) 言語を用いる。
+本論文では 検証や証明に直接使用することができる言語として Continuation based C(CbC) 言語を用いる。
 
-CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たしているかどうかを調べるモデル検査的手法を提案し、
-Akasha Meta 計算ライブラリとして実装し、赤黒木の仕様を実用的な木の大きさの範囲内で検証した。
-木の大きさを制限することなく実装が仕様を満たしていることを示すには証明が必要である。
-プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが
-知られている。本論文では証明支援系 Agda を用いた。
+CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法を提案し、メタ計算ライブラリ Akasha として実装した。
+Akasha では赤黒木の仕様を、限定的な木の大きさの範囲内で検証した。
 
-部分型を用いるとCbC の型システムを定義できる。証明やモデル検査は、これらに対するメタ計算に相当する。
-CbCの計算を実装するメタ計算はCbCで記述することができ、これは、CbCの記述なので、部分型を用いた
-型システムで相似的に定義できることを示した。
-
-それを Agda上で定義した。
-これらの形式的定義を使い、CbC のコードの合成の結合則とSingle Linked Stackの満たす性質をAgdaで証明することができた。
-
+木の大きさを制限せず実装が仕様を満たしていることを示すには証明が必要である。
+プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。
+本論文では依存型を持つ証明支援系 Agda を用いて証明を行なう。
+部分型を用いてCbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。
+これらの形式的定義を Agda によって記述し、CbC のコードの合成の結合則とSingle Linked Stackの満たす性質を証明した。
 
 \end{abstract}
 
-
 \begin{abstract_eng}
-Provinding highly reraiable software is important. One way is checking if the specification is statisfied or not, the other
-way is to prove the implementation satisfies the specification directly.
+Proving highly reliable software is important.
+One way is checking if the specification is satisfied or not, the other way is to prove the implementation satisfies the specification directly.
 If we can check or prove actual implementations, it it much better.
-In this papaer, we use Continuation base C programming language (CbC) which can be used in both proof and model checking.
-We propose model checking method By enumerating bounded computational state in CbC code as a meta computation.
-Aksha Meta Computation library makes it possible to check red-black tree algorythm within a practical tree size.
-To assure the property for arbitrary size of tree, we need proof method. Proofs in a program is known to corresponds $\lambda$ calculus,
-which is a Curry-Howward Isomorphism. We use Agda proof assistance system.
+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.
 
-We can define the CbC formal type system as a subtype. The proofs or model checkings are meta compuations of the formal type systems.
-Meta computaion which implements CbC computation can be descripbed as a CbC oomputation, that is, it is also defined by
-CbC formal tyoe system as a subtype 
-
-Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism.
-
-
+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.
+We use dependently typed Agda proof assistance system.
+Formal definitions of CbC are similarly defined by subtyped CbC terms using Agda.
+We prove associativity of CbC code and Properties of Single Linked Stack using proposed formal definitions.
 \end{abstract_eng}
 
--- a/paper/abstract_eng.tex	Fri Feb 10 17:22:00 2017 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-\begin{abstract_eng}
-Checking desirable specifications of software are important.
-If it checks actual implementations, much better.
-
-In this papaer, We propose two verification methods using meta computations which save original implementations.
-On the hand method verify specification by enumerate possible states on programs.
-We checked red-black tree specification using our meta computation library named Akasha, which override program executions exhaustively.
-
-On the other hand method veriy programs with proofs.
-Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism.
-We define the CbC type system with subtype for proving CbC itself.
-Dependent-typed language Agda proves properties of translated CbC programs using proposed subtype definition.
-\end{abstract_eng}
Binary file paper/atton-master.pdf has changed
--- a/paper/atton-master.tex	Fri Feb 10 17:22:00 2017 +0900
+++ b/paper/atton-master.tex	Sun Feb 12 10:45:45 2017 +0900
@@ -96,7 +96,6 @@
 
 %要旨
 \input{abstract.tex}
-\input{abstract_eng.tex}
 
 %目次
 \tableofcontents