|
10
|
1 \begin{abstract}
|
|
97
|
2 高い信頼性を持つソフトウェアを提供することは重要である。
|
|
98
|
3 それには、ソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。
|
|
97
|
4 特に実際に動作するソフトウェアを検証や証明できるとなお良い。
|
|
98
|
5 本論文では 検証や証明に直接使用することができる言語として Continuation based C(CbC) 言語を用いる。
|
|
73
|
6
|
|
98
|
7 CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法を提案し、メタ計算ライブラリ Akasha として実装した。
|
|
|
8 Akasha では赤黒木の仕様を、限定的な木の大きさの範囲内で検証した。
|
|
73
|
9
|
|
98
|
10 木の大きさを制限せず実装が仕様を満たしていることを示すには証明が必要である。
|
|
|
11 プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。
|
|
|
12 本論文では依存型を持つ証明支援系 Agda を用いて証明を行なう。
|
|
|
13 部分型を用いてCbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。
|
|
|
14 これらの形式的定義を Agda によって記述し、CbC のコードの合成の結合則とSingle Linked Stackの満たす性質を証明した。
|
|
10
|
15
|
|
|
16 \end{abstract}
|
|
97
|
17
|
|
|
18 \begin{abstract_eng}
|
|
98
|
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.
|
|
97
|
21 If we can check or prove actual implementations, it it much better.
|
|
98
|
22 In this paper, we use Continuation base C programming language (CbC) which can be used in both model checking and proof.
|
|
|
23
|
|
|
24 We propose model checking method by enumerating bounded computational state in CbC code as a meta computation.
|
|
|
25 Akasha Meta Computation library makes it possible to check red-black tree algorithm within a bounded tree size.
|
|
97
|
26
|
|
98
|
27 To assure the property for arbitrary size of trees, we need proof method.
|
|
|
28 Proofs in a program are known to correspond $\lambda$ calculus, which is a Curry-Howward Isomorphism.
|
|
|
29 We use dependently typed Agda proof assistance system.
|
|
|
30 Formal definitions of CbC are similarly defined by subtyped CbC terms using Agda.
|
|
|
31 We prove associativity of CbC code and Properties of Single Linked Stack using proposed formal definitions.
|
|
97
|
32 \end{abstract_eng}
|
|
|
33
|
