|
7
|
1 ---
|
|
|
2 marp: true
|
|
|
3 title: Geas Agda による Left Learning Red Black Tree の検証
|
|
|
4 paginate: true
|
|
|
5
|
|
|
6 theme: default
|
|
|
7 size: 16:9
|
|
|
8 style: |
|
|
|
9 section {
|
|
|
10 background-color: #FFFFFF;
|
|
|
11 font-size: 28px;
|
|
|
12 color: #4b4b4b;
|
|
|
13 font-family: "Droid Sans Mono", "Hiragino Maru Gothic ProN";
|
|
|
14 background-image: url("logo.svg");
|
|
|
15 background-position: right 3% bottom 2%;
|
|
|
16 background-repeat: no-repeat;
|
|
|
17 background-attachment: 5%;
|
|
|
18 background-size: 20% auto;
|
|
|
19 }
|
|
|
20
|
|
|
21 section.title h1 {
|
|
|
22 color: #808db5;
|
|
|
23 text-align: center;
|
|
|
24 }
|
|
|
25
|
|
|
26 section.title p {
|
|
|
27 bottom: 25%;
|
|
|
28 width: 100%;
|
|
|
29 position: absolute;
|
|
|
30 font-size: 25px;
|
|
|
31 color: #4b4b4b;
|
|
|
32 background: linear-gradient(transparent 90%, #ffcc00 0%);
|
|
|
33 }
|
|
|
34
|
|
|
35 section.slide h1 {
|
|
|
36 width: 95%;
|
|
|
37 color: white;
|
|
|
38 background-color: #808db5;
|
|
|
39 position: absolute;
|
|
|
40 left: 50px;
|
|
|
41 top: 35px;
|
|
|
42 }
|
|
|
43
|
|
10
|
44 section.fig_cg p {
|
|
|
45 top: 300px;
|
|
|
46 text-align: center;
|
|
|
47 }
|
|
|
48
|
|
7
|
49 ---
|
|
|
50 <!-- headingDivider: 1 -->
|
|
|
51
|
|
|
52 # Gears Agda による <br> Left Learning Red Black Tree の検証
|
|
|
53 <!-- class: title -->
|
|
|
54
|
|
|
55 Uechi Yuto, Shinji Kono 琉球大学
|
|
|
56
|
|
|
57 # 証明を用いてプログラムの信頼性の向上を目指す
|
|
|
58 <!-- class: slide -->
|
|
|
59
|
|
|
60 <!-- 研究目的 -->
|
|
|
61 - プログラムの信頼性を高めることは重要な課題である
|
|
|
62 - 信頼性を高める手法として「モデル検査」や「定理証明」など
|
|
|
63 - 当研究室でCbCという言語を開発している
|
|
|
64 - C言語からループ構造とサブルーチンを取り除き、継続を導入したC言語の下位言語となる
|
|
|
65 - 先行研究では Hoare Logic を用いて 簡単なプログラムの検証を行った
|
|
8
|
66 - 本研究では Gears Agda にて重要なアルゴリズムの一つである Red Black Tree を検証する
|
|
|
67
|
|
9
|
68 # CbC について
|
|
|
69 - CbCとは当研究室で開発しているC言語の下位言語
|
|
|
70 - CbC とは C 言語からループ制御構造とサブルーチンコールを取り除き、継続を導入したC 言語の下位言語
|
|
|
71 - 継続呼び出しは引数付き goto 文で表現される。
|
|
|
72 - 処理の単位を Code Gear, データの単位を Data Gear として記述するプログラミング言語
|
|
|
73 - CbC のプログラミングでは Data Gear を Code Gear で変更し、その変更を次の Code Gear に渡して処理を行う。
|
|
|
74
|
|
8
|
75
|
|
|
76 # Agda の基本
|
|
11
|
77 - Agdaとは定理証明支援器であり、関数型言語
|
|
|
78 - Agdaでの関数は、最初に型について定義した後に、関数を定義する事で記述する
|
|
8
|
79 - これが Curry-Howard 対応となる
|
|
|
80 - 型の定義部分で、入力と出力の型を定義できる
|
|
|
81 - input → output のようになる
|
|
|
82 - 関数の定義は = を用いて行う
|
|
|
83 - 関数名の後、 = の前で受け取る引数を記述します
|
|
11
|
84
|
|
|
85 <!--
|
|
8
|
86 ```
|
|
|
87 sample1 : (A : Set ) → Set
|
|
|
88 sample1 a = a
|
|
|
89
|
|
|
90 sample2 : (A : Set ) → (B : Set ) → Set
|
|
|
91 sample2 a b = b
|
|
|
92 ```
|
|
11
|
93 -->
|
|
8
|
94
|
|
|
95 # Agda の基本 record
|
|
11
|
96 オブジェクトあるいは構造体
|
|
8
|
97 ```
|
|
|
98 record Env : Set where
|
|
|
99 field
|
|
|
100 varn : N
|
|
|
101 vari : N
|
|
|
102 open Env
|
|
|
103 ```
|
|
|
104
|
|
10
|
105 型に対応する値の導入(intro)
|
|
8
|
106 ```
|
|
|
107 record {varx = zero ; vary = suc zero}
|
|
|
108 ```
|
|
10
|
109 record の値のアクセス(elim)
|
|
8
|
110 ```
|
|
10
|
111 (env : Env) → varx env
|
|
8
|
112 ```
|
|
|
113
|
|
7
|
114
|
|
8
|
115
|
|
7
|
116 # Gears Agda の記法
|
|
10
|
117 Gears Agda では CbC と対応させるためにすべてLoopで記述する
|
|
|
118 loopは`→ t`の形式で表現する
|
|
|
119 再起呼び出しは使わない(構文的には禁止していないので注意が必要)
|
|
8
|
120 ```
|
|
|
121 {-# TERMINATING #-}
|
|
|
122 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
|
|
|
123 whileLoop env next with lt 0 (varn env)
|
|
|
124 whileLoop env next | false = next env
|
|
|
125 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
|
126 ```
|
|
11
|
127 - t を返すことで継続を表す(tは呼び出し時に任意に指定してもよい. testに使える)
|
|
10
|
128 - tail call により light weight continuation を定義している
|
|
|
129
|
|
|
130
|
|
|
131 # Gears Agda と Gears CbC の対応
|
|
|
132 Gears Agda
|
|
|
133 - 証明向きの記述
|
|
|
134 - Hoare Condition を含む
|
|
|
135
|
|
|
136 Gears CbC
|
|
|
137 - 実行向きの記述
|
|
|
138 - メモリ管理, 並列実行を含む
|
|
|
139
|
|
|
140 Context
|
|
|
141 - processに相当する
|
|
|
142 - Code Gear 単位で並列実行
|
|
7
|
143
|
|
9
|
144
|
|
10
|
145 # Normal level と Meta Level を用いた信頼性の向上
|
|
|
146 Normal Level
|
|
|
147 - 軽量継続
|
|
|
148 - Code Gear 単位で関数型プログラミングとなる
|
|
|
149 - atomic(Code Gear 自体の実行は割り込まれない)
|
|
|
150 - ポインタの操作は含まれない
|
|
|
151
|
|
|
152 Meta Level
|
|
|
153 - メモリやCPUなどの資源管理, ポインタ操作
|
|
|
154 - Hoare Condition と証明
|
|
|
155 - Contextによる並列実行
|
|
|
156 - monadに相当するData構造
|
|
|
157
|
|
|
158 #
|
|
|
159 <!-- class: fig_cg -->
|
|
|
160 
|
|
|
161
|
|
|
162 # Gears Agda と Hoare Logic
|
|
|
163 <!-- class: slide -->
|
|
|
164 C.A.R Hoare, R.W Floyd が考案
|
|
|
165 - Pre Condition → Command → Post Condition
|
|
|
166
|
|
|
167 Gears Agda による Command の例
|
|
|
168 ```
|
|
|
169 {-# TERMINATING #-}
|
|
|
170 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
|
|
|
171 whileLoop env next with lt 0 (varn env)
|
|
|
172 whileLoop env next | false = next env
|
|
|
173 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
|
174 ```
|
|
|
175 - `{-# TERMINATING #-}`
|
|
|
176 - with 文
|
|
|
177 - 型と値
|
|
|
178
|
|
|
179 # Gears Agda の Pre Condition Post Condition
|
|
|
180 ```
|
|
|
181 whileLoopSeg : {l : Level} {t : Set l} → {c10 : N } → (env : Env) → (varn env + vari env ≡ c10)
|
|
|
182 → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)
|
|
|
183 → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
|
|
|
184 ```
|
|
|
185 - Terminatingを避けるためにloopを分割
|
|
|
186 - `varn env + vari env ≡ c10` が Pre Condition
|
|
|
187 - `varn e1 + vari e1 ≡ c10` が Post Condition
|
|
|
188 - `varn e1 < varn env → t` が停止を保証する減少列
|
|
|
189
|
|
|
190 これは命題なので証明を与えてPre ConditionからPost Conditionを導出する必要がある
|
|
|
191 証明は値として次のCodeGearに渡される
|
|
|
192
|
|
|
193 # Loop の接続
|
|
|
194 分割したloopを接続するMeta Code Gearを作成する
|
|
9
|
195 ```
|
|
|
196 TerminatingLoopS : {l : Level} {t : Set l} ( Index : Set )
|
|
|
197 → {Invraiant : Index → Set } → ( reduce : Index → N)
|
|
|
198 → (loop : (r : Index) → Invraiant r
|
|
|
199 → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t)
|
|
|
200 → (r : Index) → (p : Invraiant r) → t
|
|
|
201 ```
|
|
10
|
202 - IndexはLoop変数
|
|
|
203 - Invariantはloop変数の不変条件
|
|
|
204 - loopに接続するCode Gearを与える
|
|
|
205 - reduceは停止性を保証する減少列
|
|
|
206
|
|
|
207 これを一般的に証明することができている
|
|
9
|
208
|
|
10
|
209 # 実際のloopの接続
|
|
|
210 証明したい性質を以下のように記述する
|
|
|
211 ```
|
|
|
212 whileTestSpec1 : (c10 : N) → (e1 : Env ) → vari e1 ≡ c10 → ⊤
|
|
|
213 whileTestSpec1 _ _ x = tt
|
|
|
214 ```
|
|
|
215 loopをTerminatingLoopSで接続して仕様記述に繋げる
|
|
|
216 ```
|
|
|
217 proofGearsTermS : {c10 : N} → ⊤
|
|
|
218 proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 →
|
|
|
219 TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop
|
|
|
220 (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 ))
|
|
|
221 ```
|
|
11
|
222 - conversion1はPre Condition をPost Conditionに変換する
|
|
10
|
223 - whileLoopSeg
|
|
|
224 - ⊤
|
|
9
|
225
|
|
|
226 # test との違い
|
|
|
227 - test では実数を与えた際の出力が仕様に沿ったものであるかを検証する
|
|
|
228 - コーナーケースで仕様に沿った動きをしていない場合を考慮できない
|
|
|
229 - 今回の定理証明を用いた証明では実数を必要としない
|
|
|
230 - そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる
|
|
|
231
|
|
|
232
|
|
|
233 # Gears Agda による BinaryTree の実装
|
|
11
|
234 CbCと並行した実装をするため、Stackを明示した実装をする
|
|
9
|
235
|
|
|
236 ```
|
|
11
|
237 find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
|
|
|
238 → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
|
|
9
|
239 find key leaf st _ exit = exit leaf st
|
|
|
240 find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
|
|
|
241 find key n st _ exit | tri≈ ¬a b ¬c = exit n st
|
|
|
242 find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
|
|
|
243 find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
|
|
|
244 ```
|
|
11
|
245 置き換えるnodeまでTreeを辿り、Stackに逆順にTreeを積んでいく
|
|
9
|
246
|
|
|
247 <!--
|
|
|
248 findは全部書いても大丈夫そう
|
|
|
249 -->
|
|
|
250
|
|
|
251 # Gears Agda による BinaryTree の実装 replace node
|
|
11
|
252 置き換えたnodeをStackを解消しながらTreeを再構成する
|
|
9
|
253 ```
|
|
|
254 replace : {n m : Level} {A : Set n} {t : Set m}
|
|
|
255 → (key : N) → (value : A) → bt A → List (bt A)
|
|
|
256 → (next : N → A → bt A → List (bt A) → t )
|
|
|
257 → (exit : bt A → t) → t
|
|
|
258 replace key value repl [] next exit = exit repl -- can't happen
|
|
|
259 replace key value repl (leaf ∷ []) next exit = exit repl
|
|
|
260 replace key value repl (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁
|
|
|
261 ... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right )
|
|
|
262 ... | tri≈ ¬a b ¬c = exit (node key₁ value left right )
|
|
|
263 ... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl )
|
|
|
264 replace key value repl (leaf ∷ st) next exit = next key value repl st
|
|
|
265 replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
|
|
|
266 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st
|
|
|
267 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st
|
|
|
268 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st
|
|
|
269 ```
|
|
|
270
|
|
7
|
271
|
|
9
|
272 <!--
|
|
|
273 これは途中省略してよさそう
|
|
|
274 -->
|
|
|
275
|
|
11
|
276 # Binary Tree の3種類の Invariant
|
|
|
277 Tree Invariant
|
|
|
278 - Binary Tree が Key の順序に沿って構成されていることを表すData構造
|
|
9
|
279
|
|
11
|
280 Stack Invariant
|
|
|
281 - Stackが木の昇順に構成されていることを表す
|
|
9
|
282
|
|
11
|
283 Replace Tree
|
|
|
284 - 2つの木の1つのnodeが入れ替わっていることを示す
|
|
9
|
285
|
|
11
|
286 # Tree Invariant
|
|
|
287 - Invariant というよりも可能な Binary Tree 全体の集合を表す型
|
|
|
288 - 制約付きのBinary Tree
|
|
9
|
289 ```
|
|
|
290 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
|
|
|
291 t-leaf : treeInvariant leaf
|
|
|
292 t-single : (key : N) → (value : A) → treeInvariant (node key value leaf leaf)
|
|
|
293 t-right : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁)
|
|
|
294 → treeInvariant (node key₁ value₁ t₁ t₂)
|
|
|
295 → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
|
|
|
296 t-left : {key key₁ : N} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁)
|
|
|
297 → treeInvariant (node key value t₁ t₂)
|
|
|
298 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf )
|
|
|
299 t-node : {key key₁ key₂ : N} → {value value₁ value₂ : A}
|
|
|
300 → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂)
|
|
|
301 → treeInvariant (node key value t₁ t₂)
|
|
|
302 → treeInvariant (node key₂ value₂ t₃ t₄)
|
|
|
303 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
|
|
|
304 ```
|
|
|
305
|
|
|
306 <!--
|
|
11
|
307 t-leaf はコンストラクタ
|
|
|
308
|
|
|
309
|
|
9
|
310 コードの解説
|
|
|
311 省略した方がたぶん絶対良い
|
|
|
312 right と left なんかはほとんど対照的なので省略とかでよさそう
|
|
|
313 あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう
|
|
|
314 -->
|
|
|
315
|
|
|
316
|
|
11
|
317 # Stack Invariant
|
|
|
318 - StackにはTreeを辿った履歴が残っている
|
|
|
319 - 辿り方はKeyの値に依存する
|
|
|
320 - 実際のStackよりも豊富な情報を持っている<!--Keyの比較が入っているから-->
|
|
|
321
|
|
9
|
322 ```
|
|
|
323 data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A)
|
|
|
324 → (stack : List (bt A)) → Set n where
|
|
|
325 s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
|
|
|
326 s-right : {tree tree0 tree₁ : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)}
|
|
|
327 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st
|
|
|
328 → stackInvariant key tree tree0 (tree ∷ st)
|
|
|
329 s-left : {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)}
|
|
|
330 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st
|
|
|
331 → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
|
|
|
332 ```
|
|
|
333
|
|
11
|
334 # Replace Tree
|
|
|
335 - 木の特定のnodeが正しく置き換えられているか
|
|
9
|
336 ```
|
|
|
337 data replacedTree {n : Level} {A : Set n} (key : N) (value : A) : (before after : bt A) → Set n where
|
|
|
338 r-leaf : replacedTree key value leaf (node key value leaf leaf)
|
|
|
339 r-node : {value₁ : A} → {t t₁ : bt A}
|
|
|
340 → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
|
|
|
341 r-right : {k : N } {v1 : A} → {t t1 t2 : bt A}
|
|
|
342 → k < key → replacedTree key value t2 t
|
|
|
343 → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t)
|
|
|
344 r-left : {k : N } {v1 : A} → {t t1 t2 : bt A}
|
|
|
345 → key < k → replacedTree key value t1 t
|
|
|
346 → replacedTree key value (node k v1 t1 t2) (node k v1 t t2)
|
|
|
347 ```
|
|
7
|
348
|
|
11
|
349 # find の Hoare Condition
|
|
|
350 findPでは treeInvariant をつかって stackInvariant を生成する
|
|
|
351 停止性を証明する木の深さの不等式も証明する
|
|
|
352 ```
|
|
|
353 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
|
|
|
354 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
355 → (next : (tree1 : bt A) → (stack : List (bt A))
|
|
|
356 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
357 → bt-depth tree1 < bt-depth tree → t )
|
|
|
358 → (exit : (tree1 : bt A) → (stack : List (bt A))
|
|
|
359 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
360 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
361 ```
|
|
|
362
|
|
|
363 # Hoare Condition の拡張
|
|
|
364 testなどでは仮定が入ることがある
|
|
|
365 Hoare Conditionを拡張可能な部分があるrecordで定義する
|
|
|
366 Cが拡張される部分で, これはDataの継続に相当する
|
|
|
367 Code Gear に継続があるように Data Gearにも継続がある
|
|
9
|
368 ```
|
|
11
|
369 record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A))
|
|
|
370 (C : ℕ → bt A → List (bt A) → Set n) : Set n where
|
|
|
371 field
|
|
|
372 tree0 : bt A
|
|
|
373 ti0 : treeInvariant tree0
|
|
|
374 ti : treeInvariant tree
|
|
|
375 si : stackInvariant key tree tree0 stack
|
|
|
376 ci : C key tree stack -- data continuation
|
|
|
377 ```
|
|
|
378
|
|
|
379 # 拡張部分の記述と推論
|
|
|
380 拡張部分はrecord findPC で定義する
|
|
|
381 拡張部分の推論はrecord findExt で定義する
|
|
|
382 ```
|
|
|
383 record findPC {n : Level} {A : Set n} (value : A) (key1 : ℕ) (tree : bt A ) (stack : List (bt A)) : Set n where
|
|
|
384 field
|
|
|
385 tree1 : bt A
|
|
|
386 ci : replacedTree key1 value tree1 tree
|
|
|
387
|
|
|
388 record findExt {n : Level} {A : Set n} (key : ℕ) (C : ℕ → bt A → List (bt A) → Set n) : Set (Level.suc n) where
|
|
|
389 field
|
|
|
390 c1 : {key₁ : ℕ} {tree tree₁ : bt A } {st : List (bt A)} {v1 : A}
|
|
|
391 → findPR key (node key₁ v1 tree tree₁) st C → key < key₁ → C key tree (tree ∷ st)
|
|
|
392 c2 : {key₁ : ℕ} {tree tree₁ : bt A } {st : List (bt A)} {v1 : A}
|
|
|
393 → findPR key (node key₁ v1 tree tree₁) st C → key > key₁ → C key tree₁ (tree₁ ∷ st)
|
|
9
|
394 ```
|
|
7
|
395
|
|
11
|
396 # replade Node の Invariant
|
|
|
397 repraceTree は置き換えるべきnodeが実行時に決まるので関数を挟んだInvariantになる
|
|
|
398 ```
|
|
|
399 child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A
|
|
|
400 child-replaced key leaf = leaf
|
|
|
401 child-replaced key (node key₁ value left right) with <-cmp key key₁
|
|
|
402 ... | tri< a ¬b ¬c = left
|
|
|
403 ... | tri≈ ¬a b ¬c = node key₁ value left right
|
|
|
404 ... | tri> ¬a ¬b c = right
|
|
|
405
|
|
|
406 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A )
|
|
|
407 (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
|
|
|
408 field
|
|
|
409 tree0 : bt A
|
|
|
410 ti : treeInvariant tree0
|
|
|
411 si : stackInvariant key tree tree0 stack
|
|
|
412 ri : replacedTree key value (child-replaced key tree ) repl
|
|
|
413 ci : C tree repl stack -- data continuation
|
|
|
414 ```
|
|
|
415
|
|
|
416 # 最終的な証明コード
|
|
|
417 insertしたkeyをfindすると元の値が取れてくることを証明する
|
|
|
418 insertTreeSpec0が仕様
|
|
|
419 conteinsTreeがtestコードかつ証明になっている
|
|
|
420 証明の詳細はコードのHoara condition の証明に入っている
|
|
|
421 ```
|
|
|
422 insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A)
|
|
|
423 → top-value tree ≡ just value → ⊤
|
|
|
424 insertTreeSpec0 _ _ _ = tt
|
|
|
425
|
|
|
426 containsTree : {n : Level} {A : Set n} → (tree tree1 : bt A) → (key : ℕ) → (value : A)
|
|
|
427 → treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
|
|
|
428 containsTree {n} {A} tree tree1 key value P RT =
|
|
|
429 TerminatingLoopS (bt A ∧ List (bt A) )
|
|
|
430 {λ p → findPR key (proj1 p) (proj2 p) (findPC value ) } (λ p → bt-depth (proj1 p))
|
|
|
431 ⟪ tree , tree ∷ [] ⟫ ?
|
|
|
432 $ λ p P loop → findPPC1 key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
|
|
|
433 $ λ t1 s1 P2 found? → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2)
|
|
|
434 ```
|
|
|
435
|
|
|
436 # replace Tree の性質
|
|
|
437 Replace Tree 自体は Tree に特定の値が入っていることを示すData構造になっている
|
|
|
438 これをHoare条件として持ち歩くことにより、Binary Treeの詳細に立ち入らず何が入っているかを指定できる
|
|
|
439
|
|
|
440 これにより木を用いるプログラムでの証明を記述できる
|
|
|
441 insert Tree や Find Node の停止性も証明されている
|
|
7
|
442
|
|
|
443 # 今後の研究方針
|
|
11
|
444 - Deleteの実装
|
|
|
445 - Red Black Tree の実装
|
|
|
446 - 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
|
|
|
447 - Contextを用いた並列実行時のプログラムの正しさの証明
|
|
|
448 - syncronized queue
|
|
|
449 - concarent tree
|
|
|
450 - xv.6への適用
|
|
9
|
451 - モデル検査
|
|
7
|
452
|
|
|
453 # まとめ
|
|
|
454 - Gears Agda にて Binary Tree を検証することができた
|
|
|
455 - Gears Agda における Termination を使用しない実装の仕方を確率した
|
|
|
456 - Hoare Logic による検証もできるようになった
|
|
|
457 - 今後は Red Black Tree の検証をすすめる
|
|
|
458 - モデル検査をしたい
|
|
|
459
|
|
11
|
460 <!-- 英語版も欲しい-->
|
