Mercurial > hg > Papers > 2018 > nozomi-master
comparison paper/abstract.tex @ 97:5a354cba3694
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 10 Feb 2017 17:22:00 +0900 |
| parents | 0a4646310261 |
| children | 42f463ef7bb2 |
comparison
equal
deleted
inserted
replaced
| 96:0a4646310261 | 97:5a354cba3694 |
|---|---|
| 1 \begin{abstract} | 1 \begin{abstract} |
| 2 ソフトウェアが期待される仕様を満たすか検査することは重要である。 | 2 高い信頼性を持つソフトウェアを提供することは重要である。 |
| 3 特に実際に動作するソフトウェアを検証できるとなお良い。 | 3 それには、ソフトウェアが期待される仕様を満たすか検査する手法と、 |
| 4 仕様を直接証明する手法とがある。 | |
| 5 特に実際に動作するソフトウェアを検証や証明できるとなお良い。 | |
| 6 本論文では 検証や証明に直接使用することができる言語として | |
| 7 Continuation based C(CbC) 言語を用いる。 | |
| 4 | 8 |
| 5 本論文では Continuation based C(CbC) 言語で記述されたプログラムを検証用に変更せず信頼性を確保する手法を二つ提案する。 | 9 CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たしているかどうかを調べるモデル検査的手法を提案し、 |
| 6 一つはプログラムが持つ状態を数え挙げ、常に仕様を満たすことを保証するモデル検査的手法である。 | 10 Akasha Meta 計算ライブラリとして実装し、赤黒木の仕様を実用的な木の大きさの範囲内で検証した。 |
| 7 プログラムの実行を網羅的に行なうよう変更するメタ計算ライブラリ akasha を用いて赤黒木の仕様を検証する。 | 11 木の大きさを制限することなく実装が仕様を満たしていることを示すには証明が必要である。 |
| 12 プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが | |
| 13 知られている。本論文では証明支援系 Agda を用いた。 | |
| 8 | 14 |
| 9 もう一つの信頼性向上手法として、プログラムのデータ構造の性質を証明する手法を提案する。 | 15 部分型を用いるとCbC の型システムを定義できる。証明やモデル検査は、これらに対するメタ計算に相当する。 |
| 10 プログラムにおける証明は Curry-Howard Isomorphism により型付き $\lambda$計算に対応している。 | 16 CbCの計算を実装するメタ計算はCbCで記述することができ、これは、CbCの記述なので、部分型を用いた |
| 11 CbC プログラムの性質を証明できるよう、部分型を用いてCbC の型システムを定義する。 | 17 型システムで相似的に定義できることを示した。 |
| 12 加えて、型システムの定義を用いて証明支援系言語 Agda 上に CbC のプログラムを記述し、証明を行なう。 | 18 |
| 19 それを Agda上で定義した。 | |
| 20 これらの形式的定義を使い、CbC のコードの合成の結合則とSingle Linked Stackの満たす性質をAgdaで証明することができた。 | |
| 21 | |
| 13 | 22 |
| 14 \end{abstract} | 23 \end{abstract} |
| 24 | |
| 25 | |
| 26 \begin{abstract_eng} | |
| 27 Provinding highly reraiable software is important. One way is checking if the specification is statisfied or not, the other | |
| 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 | |
| 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. | |
| 37 Meta computaion which implements CbC computation can be descripbed as a CbC oomputation, that is, it is also defined by | |
| 38 CbC formal tyoe system as a subtype | |
| 39 | |
| 40 Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism. | |
| 41 | |
| 42 | |
| 43 \end{abstract_eng} | |
| 44 |