proofGearsTermS : {c10 : N} → ⊤
proofGearsTermS {c10} = whileTest' {_} {_} {c10} (λ n p → conversion1 n p (λ n1 p1 →
TerminatingLoopS Env (λ env → varn env)(λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop
(λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 ))
conversion1はPre Condition をPost Conditionに変換する
⊤
test との違い
test では実数を与えた際の出力が仕様に沿ったものであるかを検証する
コーナーケースで仕様に沿った動きをしていない場合を考慮できない
今回の定理証明を用いた証明では実数を必要としない
そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる
Binary Tree
時間が余りそうならやる
Gears Agda による BinaryTree の実装
CbCと並行した実装をするため、Stackを明示した実装をする
find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
→ (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
find key leaf st _ exit = exit leaf st
find key (node key₁ v1 tree tree₁) st next exit with <-cmp key key₁
find key n st _ exit | tri≈ ¬a b ¬c = exit n st
find key n@(node key₁ v1 tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st)
find key n@(node key₁ v1 tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
置き換えるnodeまでTreeを辿り、Stackに逆順にTreeを積んでいく
Gears Agda による BinaryTree の実装 replace node
置き換えたnodeをStackを解消しながらTreeを再構成する
replace : {n m : Level} {A : Set n} {t : Set m}
→ (key : N) → (value : A) → bt A → List (bt A)
→ (next : N → A → bt A → List (bt A) → t )
→ (exit : bt A → t) → t
replace key value repl [] next exit = exit repl -- can't happen
replace key value repl (leaf ∷ []) next exit = exit repl
replace key value repl (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁
... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right )
... | tri≈ ¬a b ¬c = exit (node key₁ value left right )
... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl )
replace key value repl (leaf ∷ st) next exit = next key value repl st
replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st
... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st
... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st
data stackInvariant {n : Level} {A : Set n} (key : N) : (top orig : bt A)
→ (stack : List (bt A)) → Set n where
s-single : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
s-right : {tree tree0 tree₁ : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)}
→ key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st
→ stackInvariant key tree tree0 (tree ∷ st)
s-left : {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)}
→ key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st
→ stackInvariant key tree₁ tree0 (tree₁ ∷ st)
Replace Tree
木の特定のnodeが正しく置き換えられているか
data replacedTree {n : Level} {A : Set n} (key : N) (value : A) : (before after : bt A) → Set n where
r-leaf : replacedTree key value leaf (node key value leaf leaf)
r-node : {value₁ : A} → {t t₁ : bt A}
→ replacedTree key value (node key value₁ t t₁) (node key value t t₁)
r-right : {k : N } {v1 : A} → {t t1 t2 : bt A}
→ k < key → replacedTree key value t2 t
→ replacedTree key value (node k v1 t1 t2) (node k v1 t1 t)
r-left : {k : N } {v1 : A} → {t t1 t2 : bt A}
→ key < k → replacedTree key value t1 t
→ replacedTree key value (node k v1 t1 t2) (node k v1 t t2)
findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
→ treeInvariant tree ∧ stackInvariant key tree tree0 stack
→ (next : (tree1 : bt A) → (stack : List (bt A))
→ treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
→ bt-depth tree1 < bt-depth tree → t )
→ (exit : (tree1 : bt A) → (stack : List (bt A))
→ treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
→ (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
Hoare Condition の拡張
testなどでは仮定が入ることがある
Hoare Conditionを拡張可能な部分があるrecordで定義する
Cが拡張される部分で, これはDataの継続に相当する
Code Gear に継続があるように Data Gearにも継続がある
record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A))
(C : ℕ → bt A → List (bt A) → Set n) : Set n where
field
tree0 : bt A
ti0 : treeInvariant tree0
ti : treeInvariant tree
si : stackInvariant key tree tree0 stack
ci : C key tree stack -- data continuation
record findPC {n : Level} {A : Set n} (value : A) (key1 : ℕ) (tree : bt A ) (stack : List (bt A)) : Set n where
field
tree1 : bt A
ci : replacedTree key1 value tree1 tree
record findExt {n : Level} {A : Set n} (key : ℕ) (C : ℕ → bt A → List (bt A) → Set n) : Set (Level.suc n) where
field
c1 : {key₁ : ℕ} {tree tree₁ : bt A } {st : List (bt A)} {v1 : A}
→ findPR key (node key₁ v1 tree tree₁) st C → key < key₁ → C key tree (tree ∷ st)
c2 : {key₁ : ℕ} {tree tree₁ : bt A } {st : List (bt A)} {v1 : A}
→ findPR key (node key₁ v1 tree tree₁) st C → key > key₁ → C key tree₁ (tree₁ ∷ st)
child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A
child-replaced key leaf = leaf
child-replaced key (node key₁ value left right) with <-cmp key key₁
... | tri< a ¬b ¬c = left
... | tri≈ ¬a b ¬c = node key₁ value left right
... | tri> ¬a ¬b c = right
record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A )
(stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
field
tree0 : bt A
ti : treeInvariant tree0
si : stackInvariant key tree tree0 stack
ri : replacedTree key value (child-replaced key tree ) repl
ci : C tree repl stack -- data continuation
insertTreeSpec0 : {n : Level} {A : Set n} → (tree : bt A) → (value : A)
→ top-value tree ≡ just value → ⊤
insertTreeSpec0 _ _ _ = tt
containsTree : {n : Level} {A : Set n} → (tree tree1 : bt A) → (key : ℕ) → (value : A)
→ treeInvariant tree1 → replacedTree key value tree1 tree → ⊤
containsTree {n} {A} tree tree1 key value P RT =
TerminatingLoopS (bt A ∧ List (bt A) )
{λ p → findPR key (proj1 p) (proj2 p) (findPC value ) } (λ p → bt-depth (proj1 p))
⟪ tree , tree ∷ [] ⟫ ?
$ λ p P loop → findPPC1 key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
$ λ t1 s1 P2 found? → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2)
replace Tree の性質
Replace Tree 自体は Tree に特定の値が入っていることを示すData構造になっている
これをHoare条件として持ち歩くことにより、Binary Treeの詳細に立ち入らず何が入っているかを指定できる
これにより木を用いるプログラムでの証明を記述できる
insert Tree や Find Node の停止性も証明されている
今後の研究方針
Deleteの実装
Red Black Tree の実装
今回定義した条件はそのまま Red Black Tree の検証に使用できるはず
Contextを用いた並列実行時のプログラムの正しさの証明
synchronized queue
concurrent tree
xv.6への適用
モデル検査
まとめ
Gears Agda にて Binary Tree を検証することができた
Gears Agda における Termination を使用しない実装の仕方を確立した
Hoare Logic による検証もできるようになった
今後は Red Black Tree の検証をすすめる
モデル検査をしたい
Page 1 of 29
研究目的
```
sample1 : (A : Set ) → Set
sample1 a = a
sample2 : (A : Set ) → (B : Set ) → Set
sample2 a b = b
```
findは全部書いても大丈夫そう
これは途中省略してよさそう
t-leaf はコンストラクタ
コードの解説
省略した方がたぶん絶対良い
right と left なんかはほとんど対照的なので省略とかでよさそう
あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう