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