Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/abstract.tex @ 98:42f463ef7bb2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update abstract
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 12 Feb 2017 10:45:45 +0900
parents 5a354cba3694
children a891d7551bbf
comparison
equal deleted inserted replaced
97:5a354cba3694 98:42f463ef7bb2
1 \begin{abstract} 1 \begin{abstract}
2 高い信頼性を持つソフトウェアを提供することは重要である。 2 高い信頼性を持つソフトウェアを提供することは重要である。
3 それには、ソフトウェアが期待される仕様を満たすか検査する手法と、 3 それには、ソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。
4 仕様を直接証明する手法とがある。
5 特に実際に動作するソフトウェアを検証や証明できるとなお良い。 4 特に実際に動作するソフトウェアを検証や証明できるとなお良い。
6 本論文では 検証や証明に直接使用することができる言語として 5 本論文では 検証や証明に直接使用することができる言語として Continuation based C(CbC) 言語を用いる。
7 Continuation based C(CbC) 言語を用いる。
8 6
9 CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たしているかどうかを調べるモデル検査的手法を提案し、 7 CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法を提案し、メタ計算ライブラリ Akasha として実装した。
10 Akasha Meta 計算ライブラリとして実装し、赤黒木の仕様を実用的な木の大きさの範囲内で検証した。 8 Akasha では赤黒木の仕様を、限定的な木の大きさの範囲内で検証した。
11 木の大きさを制限することなく実装が仕様を満たしていることを示すには証明が必要である。
12 プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが
13 知られている。本論文では証明支援系 Agda を用いた。
14 9
15 部分型を用いるとCbC の型システムを定義できる。証明やモデル検査は、これらに対するメタ計算に相当する。 10 木の大きさを制限せず実装が仕様を満たしていることを示すには証明が必要である。
16 CbCの計算を実装するメタ計算はCbCで記述することができ、これは、CbCの記述なので、部分型を用いた 11 プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。
17 型システムで相似的に定義できることを示した。 12 本論文では依存型を持つ証明支援系 Agda を用いて証明を行なう。
18 13 部分型を用いてCbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。
19 それを Agda上で定義した。 14 これらの形式的定義を Agda によって記述し、CbC のコードの合成の結合則とSingle Linked Stackの満たす性質を証明した。
20 これらの形式的定義を使い、CbC のコードの合成の結合則とSingle Linked Stackの満たす性質をAgdaで証明することができた。
21
22 15
23 \end{abstract} 16 \end{abstract}
24 17
18 \begin{abstract_eng}
19 Proving highly reliable software is important.
20 One way is checking if the specification is satisfied or not, the other way is to prove the implementation satisfies the specification directly.
21 If we can check or prove actual implementations, it it much better.
22 In this paper, we use Continuation base C programming language (CbC) which can be used in both model checking and proof.
25 23
26 \begin{abstract_eng} 24 We propose model checking method by enumerating bounded computational state in CbC code as a meta computation.
27 Provinding highly reraiable software is important. One way is checking if the specification is statisfied or not, the other 25 Akasha Meta Computation library makes it possible to check red-black tree algorithm within a bounded tree size.
28 way is to prove the implementation satisfies the specification directly.
29 If we can check or prove actual implementations, it it much better.
30 In this papaer, we use Continuation base C programming language (CbC) which can be used in both proof and model checking.
31 We propose model checking method By enumerating bounded computational state in CbC code as a meta computation.
32 Aksha Meta Computation library makes it possible to check red-black tree algorythm within a practical tree size.
33 To assure the property for arbitrary size of tree, we need proof method. Proofs in a program is known to corresponds $\lambda$ calculus,
34 which is a Curry-Howward Isomorphism. We use Agda proof assistance system.
35 26
36 We can define the CbC formal type system as a subtype. The proofs or model checkings are meta compuations of the formal type systems. 27 To assure the property for arbitrary size of trees, we need proof method.
37 Meta computaion which implements CbC computation can be descripbed as a CbC oomputation, that is, it is also defined by 28 Proofs in a program are known to correspond $\lambda$ calculus, which is a Curry-Howward Isomorphism.
38 CbC formal tyoe system as a subtype 29 We use dependently typed Agda proof assistance system.
39 30 Formal definitions of CbC are similarly defined by subtyped CbC terms using Agda.
40 Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism. 31 We prove associativity of CbC code and Properties of Single Linked Stack using proposed formal definitions.
41
42
43 \end{abstract_eng} 32 \end{abstract_eng}
44 33