Mercurial > hg > Members > Moririn
annotate Todo.txt @ 677:681577b60c35
child-replaced
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Nov 2021 09:06:31 +0900 |
| parents | 7bacba816277 |
| children | 6a805c8c1e53 |
| rev | line source |
|---|---|
|
578
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
1 <<<<<<< working copy |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
2 Thu May 17 15:26:56 JST 2018 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
3 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
4 findNode -> replaceNode -> getRedBlackTree だが |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
5 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
6 findNode -> P0 -> replaceNode -> P1 -> getRedBlackTree |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
7 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
8 という形で証明しても良い。一挙に証明するのは,可能だろうけど、良くないはず。 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
9 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
10 ||||||| base |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
11 ======= |
| 575 | 12 |
| 13 | |
|
578
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
14 >>>>>>> destination |
| 573 | 15 Sun May 6 17:54:50 JST 2018 |
| 16 | |
| 17 do1 a $ \b -> do2 b next を、do1 と do2 に分離することはできる? | |
| 18 | |
| 19 | |
| 20 Mon Apr 30 17:15:16 JST 2018 | |
| 21 | |
| 22 Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない | |
| 23 やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい | |
| 24 | |
| 553 | 25 Mon Mar 26 17:43:06 JST 2018 |
| 26 | |
| 573 | 27 Decidable を使って Compare の場合分けを行う |
| 553 | 28 Decidable を使うと Eq から x ≡ y の証明を取り出すことができる |
| 29 場合分けには Trichotomous を使う | |
| 573 | 30 compareTri を完成させる Done |
| 553 | 31 |
| 524 | 32 Fri Jan 5 16:43:26 JST 2018 |
| 33 | |
| 34 unbalanced binary search tree の動作を調べる | |
| 35 | |
| 36 RedBlackTree の put を完成させる | |
| 37 | |
| 38 RedBlackTree の Deletion を完成させる | |
| 39 | |
| 40 unbalanced binary search tree と同様の動作をする | |
| 41 | |
| 42 木の深さの最小と最大の差が２倍を超えない | |
| 43 | |
| 44 CodeGear/DataGear が構成する圏を定義する | |
| 45 | |
| 46 goto を定義して meta 計算を可能にする | |
| 47 | |
| 48 DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする | |
| 49 | |
| 50 実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する | |
| 51 | |
| 52 Monad の合成に必要な規則を上の圏上に定義する | |
| 53 | |
| 54 synchronizedQueue の仕様をCTLを使って定義する | |
| 55 | |
| 56 Gearsで記述したsynchornizedQueueを検証する | |
| 57 | |
| 58 gotoを用いてモデル検査と証明の組み合わせを実現する | |
| 59 | |
| 60 | |
| 575 | 61 Wed Aug 27 17:52:00 JST 2019 |
| 62 | |
| 63 別で定義した TriCotomos や \=? などの Relation の関数を | |
| 64 Agdaで定義してあるものに置き換える,まとめる | |
| 65 | |
| 66 HoareLogic をベースにした SingleLinkedStack の作成 | |
| 67 | |
| 68 HoareLogic ベースの Tree の証明 |