|
10
|
1 \begin{abstract}
|
|
97
|
2 高い信頼性を持つソフトウェアを提供することは重要である。
|
|
|
3 それには、ソフトウェアが期待される仕様を満たすか検査する手法と、
|
|
|
4 仕様を直接証明する手法とがある。
|
|
|
5 特に実際に動作するソフトウェアを検証や証明できるとなお良い。
|
|
|
6 本論文では 検証や証明に直接使用することができる言語として
|
|
|
7 Continuation based C(CbC) 言語を用いる。
|
|
73
|
8
|
|
97
|
9 CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たしているかどうかを調べるモデル検査的手法を提案し、
|
|
|
10 Akasha Meta 計算ライブラリとして実装し、赤黒木の仕様を実用的な木の大きさの範囲内で検証した。
|
|
|
11 木の大きさを制限することなく実装が仕様を満たしていることを示すには証明が必要である。
|
|
|
12 プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが
|
|
|
13 知られている。本論文では証明支援系 Agda を用いた。
|
|
73
|
14
|
|
97
|
15 部分型を用いるとCbC の型システムを定義できる。証明やモデル検査は、これらに対するメタ計算に相当する。
|
|
|
16 CbCの計算を実装するメタ計算はCbCで記述することができ、これは、CbCの記述なので、部分型を用いた
|
|
|
17 型システムで相似的に定義できることを示した。
|
|
|
18
|
|
|
19 それを Agda上で定義した。
|
|
|
20 これらの形式的定義を使い、CbC のコードの合成の結合則とSingle Linked Stackの満たす性質をAgdaで証明することができた。
|
|
|
21
|
|
10
|
22
|
|
|
23 \end{abstract}
|
|
97
|
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
|
