Mercurial > hg > Papers > 2023 > moririn-sigos
changeset 4:854b01e2ce98
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 17 Apr 2023 20:31:28 +0900 |
| parents | 16a733cb4a61 |
| children | 7cb97e1d76c0 |
| files | main.pdf rbtree.ind |
| diffstat | 2 files changed, 150 insertions(+), 97 deletions(-) [+] |
line wrap: on
line diff
--- a/rbtree.ind Mon Apr 17 18:36:55 2023 +0900 +++ b/rbtree.ind Mon Apr 17 20:31:28 2023 +0900 @@ -1,6 +1,6 @@ -title: GearsAgdaによる Red Black Tree の検証 --author: 森逸汰 and 河野真治 +-author: 森逸汰 and 河野真治 --abstract: @@ -16,9 +16,9 @@ by implementing Hoare Logic on Agda. We want to extend this to the verification of RedBlack Trees and concurrent execution on these trees. By expanding the invariant, we can verify RedBlack -Trees. Concurrent execution can be achieved by formalizing +Trees. Concurrent execution can be achieved by formalizing Model Checking on GearsAgda. Considerations need to be made -for this. +for this. --検証された Red Black Treeの重要性 @@ -45,9 +45,9 @@ このような場合に有効なのは invariant (ループや再帰で不変な条件/命題)を見つけることであり、 古典的には Hoare Logic として知られている。この論文では、実際に、簡単な while program -の証明と、二分木、そして Red Black Tree \cite{red-black-tree}のinvariantについて考察する。 +の証明と、二分木、そして Red Black Tree のinvariantについて考察する。 -GearsAgda \clite{gearAgda}は、Gears OS\cite{gearsos}に採用されている CbC (Continuation based C)\cite{cbc}をAgdaで記述する +GearsAgda \cite{gearsAgda}は、Gears OS\cite{gearsOs}に採用されている CbC (Continuation based C)\cite{cbc-github}をAgdaで記述する 方法である。これを用いることにより、CbCに直接対応した Hoare Logic よりも柔軟な 証明法を使うことができる。例えば、プログラムの停止性は、CbCの実行単位である Code Gearに対して、ループで減少する自然数を対応させることで容易に示すことが @@ -104,7 +104,8 @@ である。これにより、 - initTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : (en : Env c10 ) → vari en ≡ c10 → t) → t + initTest : {l : Level} {t : Set l} → (c10 : ℕ) + → (Code : (en : Env c10 ) → vari en ≡ c10 → t) → t initTest c10 next = next (record {vari = c10 ; varn = 0 }) refl という風に初期化が正しく値を設定していることを証明付きで書ける。ここで @@ -131,7 +132,7 @@ --古典的な手法 -プログラムを検証する方法としては、Hoare Logic \cite{hoare} が知られている。これは、プログラムを command で記述し、 +プログラムを検証する方法としては、Hoare Logic \cite{Girard:1989:PT:64805,agda2-hoare} が知られている。これは、プログラムを command で記述し、 前提に成立する条件 Pre と 実行後に成立する条件 Post との {Pre} command {Post} @@ -177,8 +178,8 @@ whileLoop にinvariantの証明を足し、軽量継続で loop を分割すると、停止性を codeGear の段階で Agda が判断する必要がなくなる。 - whileLoopSeg : {l : Level} {t : Set l} → (c10 : ℕ ) → (env : Env c10 ) - → (next : (e1 : Env c10 ) → varn e1 < varn env → t) + whileLoopSeg : {l : Level} {t : Set l} → (c10 : ℕ ) → (env : Env c10 ) + → (next : (e1 : Env c10 ) → varn e1 < varn env → t) → (exit : (e1 : Env c10 ) → vari e1 ≡ c10 → t) → t whileLoopSeg c10 env next exit with ( suc zero ≤? (varn env) ) whileLoopSeg c10 env next exit | no p = exit env ? @@ -191,20 +192,26 @@ TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → ( reduce : Index → ℕ) → (loop : (r : Index) → (next : (r1 : Index) → reduce r1 < reduce r → t ) → t) - → (r : Index) → t + → (r : Index) → t TerminatingLoopS {_} {t} Index reduce loop r with <-cmp 0 (reduce r) - ... | tri≈ ¬a b ¬c = loop r (λ r1 lt → ⊥-elim (lemma3 b lt) ) - ... | tri< a ¬b ¬c = loop r (λ r1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) lt1 ) where + ... | tri≈ ¬a b ¬c = loop r (λ r1 lt → ⊥-elim (lemma3 b lt) ) + ... | tri< a ¬b ¬c = loop r (λ r1 lt1 + → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) lt1 ) where TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → reduce r1 < reduce r → t - TerminatingLoop1 zero r r1 n≤j lt = loop r1 (λ r2 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 zero r r1 n≤j lt = loop r1 (λ r2 lt1 → ⊥-elim (lemma5 n≤j lt1)) TerminatingLoop1 (suc j) r r1 n≤j lt with <-cmp (reduce r1) (suc j) - ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a lt - ... | tri≈ ¬a b ¬c = loop r1 (λ r2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) lt1 ) - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a lt + ... | tri≈ ¬a b ¬c = loop r1 (λ r2 lt1 → TerminatingLoop1 j r1 r2 + (subst (λ k → reduce r2 < k ) b lt1 ) lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) ここで、\verb+tri≈+などは、二つの自然数を比較した <,=,> の三つの場合を表す data である。 -\verb+<-cmp 0 (reduce r)+ で、その三つの場合を作っている。そして、 \verb+... | tri> ¬a ¬b c = \+という形 -で受ける。\verb+⊥-elim ( nat-≤> c n≤j ) +は、矛盾の削除則である。 + <-cmp 0 (reduce r) +で、その三つの場合を作っている。そして、 + ... | tri> ¬a ¬b c = +という形で受ける。 + ⊥-elim ( nat-≤> c n≤j ) +は、矛盾の削除則である。 TerminatingLoopS では、loop からの脱出は記述されていない。indexが 0 以下になることはありえないので、 loop はその前に終了しているはずである。それは、whileLoopSeg でのreduce の証明がそれを @@ -215,9 +222,10 @@ 実際の証明は proofGearsTermS : (c10 : ℕ ) → ⊤ - proofGearsTermS c10 = - TerminatingLoopS (Env c10) (λ env → varn env) (λ n2 loop → whileLoopSeg c10 n2 loop (λ ne pe → whileTestSpec1 c10 ne pe ) ) - record { varn = 0 ; vari = c10 ; n+i=c = refl } + proofGearsTermS c10 = + TerminatingLoopS (Env c10) (λ env → varn env) (λ n2 loop + → whileLoopSeg c10 n2 loop (λ ne pe → whileTestSpec1 c10 ne pe ) ) + record { varn = 0 ; vari = c10 ; n+i=c = refl } というようになる。最初の初期化の証明と同じように、プログラムは値の部分にあり実際に実行されていて、 それが仕様を満たしている証明を\verb+whileTestSpec1 c10 ne pe+が受け取っている。loop 変数が @@ -263,76 +271,103 @@ data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where t-leaf : treeInvariant leaf t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf) - t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key₁ value₁ t₁ t₂) + t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) + → treeInvariant (node key₁ value₁ t₁ t₂) → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) - t-left : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key value t₁ t₂) + t-left : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) + → treeInvariant (node key value t₁ t₂) → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) - t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂) + t-node : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} + → (key < key₁) → (key₁ < key₂) → treeInvariant (node key value t₁ t₂) → treeInvariant (node key₂ value₂ t₃ t₄) → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) これが二分木のデータ構造と invariant の実装になる。これは、invariant というよりは、順序付された二分木の可能な値全部の集合 -であり、二分木の表示的意味論\cite{}そのものになっている。 +であり、二分木の表示的意味論そのものになっている。 -ここで、\reb+(key < key₁)+は、Agdaの型であり、そこには順序を示す data 構造が配る。つまり、二分木の順序は木の構成時に証明する +ここで、\verb+(key < key₁)+は、Agdaの型であり、そこには順序を示す data 構造が配る。つまり、二分木の順序は木の構成時に証明する 必要がある。 さらに、stack が木をたどった順に構成されていることと、木が置き換わっていることを示す invariant が必要である。 - data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where + data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) + → (stack : List (bt A)) → Set n where s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ []) s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} - → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st) + → 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₁ : ℕ } → {v1 : A } → {st : List (bt A)} - → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st) + → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st + → stackInvariant key tree₁ tree0 (tree₁ ∷ st) - data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt A ) → Set n where + data replacedTree {n : Level} {A : Set n} (key : ℕ) (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-node : {value₁ : A} → {t t₁ : bt A} + → replacedTree key value (node key value₁ t t₁) (node key value t t₁) r-right : {k : ℕ } {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) + → k < key → replacedTree key value t2 t + → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) r-left : {k : ℕ } {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) + → key < k → replacedTree key value t1 t + → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 木の構造は同じ順序を持っていても、同じ形にはならない。このreplacedTree は、そういう場合が考慮されていない。 - - 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 - findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl) - findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁ - findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl) - findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st) + + 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 + findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl) + findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁ + findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl) + ... | tri< a ¬b ¬c = next tree (tree ∷ st) ⟪ ? , ? ⟫ ? - findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) + ... | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) ⟪ ? , ? ⟫ ? ここでも、実際の証明は? と省略している。ここで、木の深さをloopの停止条件として使っている。 - replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) + replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) + → (value : A) → (tree : bt A) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) - → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value (child-replaced key tree) tree1 → t) → t + → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 + → replacedTree key value (child-replaced key tree) tree1 → t) → t -repplaceのプログラムはさらに煩雑なので型だけを示す。 +repaceのプログラムはさらに煩雑なので型だけを示す。 最終的に、これらを loop connector で接続して証明付きのプログラムが完成する。 - - insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree - → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t - insertTreeP {n} {m} {A} {t} tree key value P0 exit = - TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ P0 , s-nil ⟫ - $ λ p P loop → findP key (proj1 p) tree (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + + insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) + → (key : ℕ) → (value : A) → treeInvariant tree + → (exit : (tree repl : bt A) + → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t + insertTreeP {n} {m} {A} {t} tree key value P0 exit = + TerminatingLoopS (bt A ∧ List (bt A) ) + {λ p → treeInvariant (proj1 p) + ∧ stackInvariant key (proj1 p) tree (proj2 p) } + (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ P0 , s-nil ⟫ + $ λ p P loop → findP key (proj1 p) tree (proj2 p) P + (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) $ λ t s P C → replaceNodeP key value t C (proj1 P) $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A ) - {λ p → replacePR key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) } - (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt } + {λ p → replacePR key value (proj1 (proj2 p)) + (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) } + (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ + record { tree0 = tree ; ti = P0 + ; si = proj2 P ; ri = R ; ci = lift tt } $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1 - (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) - $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫ + (λ key value {tree1} repl1 stack P2 lt + → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) + $ λ tree repl P → exit tree repl + ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫ このプログラムは順序付きの二分木のinvariantと、それが置換されているinvariantを返すので、そこから、 必要な仕様をすべて導出することができる。例えば、木がソートされていること、置換したもの以外は保存されていることなどである。 @@ -343,21 +378,28 @@ 赤黒木は、バランスした二分木の実装の一つである。木のノードに赤と黒の状態を持たせ、黒のノードの個数を左右でバランスさせる。 これをそのまま invariant として記述する。この時、木の深さは b-depth で直接的に記述できる。 - data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where - rb-leaf : (key : ℕ) → RBTree A key Black 0 - rb-single : (key : ℕ) → (value : A) → (c : Color) → RBTree A key c 1 - t-right-red : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } → RBTree A key₁ Black d → RBTree A key Red d - t-right-black : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ }→ RBTree A key₁ c d → RBTree A key Black (suc d) - t-left-red : (key₁ : ℕ) { key : ℕ} → (value : A) → key < key₁ → {d : ℕ} → RBTree A key Black d - → RBTree A key₁ Red d - t-left-black : (key₁ : ℕ) {key : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ} → RBTree A key c d - → RBTree A key₁ Black (suc d) - t-node-red : (key₁ : ℕ) { key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {d : ℕ} - → RBTree A key Black d - → RBTree A key₂ Black d - → RBTree A key₁ Red d - t-node-black : (key₁ : ℕ) {key key₂ : ℕ} → (value : A) → key < key₁ → key₁ < key₂ → {c c1 : Color} {d : ℕ} - → RBTree A key c d + data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color + → (b-depth : ℕ) → Set n where + rb-leaf : (key : ℕ) → RBTree A key Black 0 + rb-single : (key : ℕ) → (value : A) → (c : Color) → RBTree A key c 1 + t-right-red : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ → {d : ℕ } + → RBTree A key₁ Black d → RBTree A key Red d + t-right-black : (key : ℕ) {key₁ : ℕ} → (value : A) → key < key₁ + → {c : Color} → {d : ℕ }→ RBTree A key₁ c d → RBTree A key Black (suc d) + t-left-red : (key₁ : ℕ) { key : ℕ} → (value : A) → key < key₁ → {d : ℕ} + → RBTree A key Black d + → RBTree A key₁ Red d + t-left-black : (key₁ : ℕ) {key : ℕ} → (value : A) → key < key₁ → {c : Color} → {d : ℕ} + → RBTree A key c d + → RBTree A key₁ Black (suc d) + t-node-red : (key₁ : ℕ) { key key₂ : ℕ} → (value : A) + → key < key₁ → key₁ < key₂ → {d : ℕ} + → RBTree A key Black d + → RBTree A key₂ Black d + → RBTree A key₁ Red d + t-node-black : (key₁ : ℕ) {key key₂ : ℕ} → (value : A) + → key < key₁ → key₁ < key₂ → {c c1 : Color} {d : ℕ} + → RBTree A key c d → RBTree A key₂ c1 d → RBTree A key₁ Black (suc d) @@ -371,35 +413,45 @@ 行う。なので、replaceTree には回転を扱う部分を追加する必要がある。さらに、stack には、二つのノードを明示する invariant が 必要になる。 - - data rbstackInvariant2 {n : Level} {A : Set n} {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) : - {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (parent : RBTree A k1 c1 d1) (grand : RBTree A k2 c2 d2) Set n where - s-head : rbstackInvariant2 orig ? orig + + data rbstackInvariant2 {n : Level} {A : Set n} {key : ℕ} {c : Color} {d : ℕ} + (orig : RBTree A key c d ) : + {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (parent : RBTree A k1 c1 d1) + (grand : RBTree A k2 c2 d2) Set n where + s-head : rbstackInvariant2 orig ? orig s-right : rbstackInvariant2 orig ? ? → rbstackInvariant2 orig ? ? s-left : rbstackInvariant2 orig ? ? → rbstackInvariant2 orig ? ? replaceTree は、RBTree をそのまま使うとかなり煩雑になる。 まず、 - - findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (tree1 : RBTree A key1 c1 d1 ) - → rbstackInvariant tree key1 - → (next : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key1 → rbt-depth A tree0 < rbt-depth A tree1 → t ) - → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) → rbstackInvariant tree key1 - → (rbt-depth A tree ≡ 0 ) ∨ ( rbt-key A tree ≡ just key ) → t ) → t + + findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} + → {c c1 : Color} + → (tree : RBTree A key c d ) (tree1 : RBTree A key1 c1 d1 ) + → rbstackInvariant tree key1 + → (next : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) + → rbstackInvariant tree key1 → rbt-depth A tree0 < rbt-depth A tree1 → t ) + → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree0 : RBTree A key0 c0 d0 ) + → rbstackInvariant tree key1 + → (rbt-depth A tree ≡ 0 ) ∨ ( rbt-key A tree ≡ just key ) → t ) → t findRBPで置き換える部分までの stackを構成する。この時に、脱出条件として、ノードのキーが等しいか、leaf であることを要求する。 replaceRBP : {n m : Level} {A : Set n} {t : Set m} - → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} - → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 ) + → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} + {c0 c1 c2 : Color} + → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) + ( repl : RBTree A key2 c2 d2 ) → (si : rbstackInvariant orig key1) → (ri : replacedTree key value (RB→bt A tree) (RB→bt A repl)) - → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) + → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} + → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) → (si1 : rbstackInvariant orig k1) → (ri : replacedTree key value (RB→bt A tree1) (RB→bt A repl1)) → rbsi-len orig si1 < rbsi-len orig si → t ) - → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) + → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) + → (repl1 : RBTree A k2 c2 d2 ) → (ri : replacedTree key value (RB→bt A orig) (RB→bt A repl1)) → t ) → t @@ -434,23 +486,24 @@ Context には、dataGear 全部の他に、詳細とメタレベルの変換を行う codeGearの stub、次に実行する codeGearの番号 が入っている。また、実行が失敗した時の例外処理を担当するcodeGearの番号も入っている。 - - record Context : Set where + + record Context : Set where field - next : Code - fail : Code - - c_Phil-API : Phil-API - c_AtomicNat-API : AtomicNat-API - + next : Code + fail : Code + + c_Phil-API : Phil-API + c_AtomicNat-API : AtomicNat-API + mbase : ℕ - memory : bt Data - error : Data + memory : bt Data + error : Data fail_next : Code codeGearの番号は\verb+code_table+で管理される。 - code_table : {n : Level} {t : Set n} → Code → Context → ( Code → Context → t) → t + code_table : {n : Level} {t : Set n} → Code + → Context → ( Code → Context → t) → t OS(あるいは分散計算を含む並行実行全体)は、単純に List Context で表される。