Mercurial > hg > Members > Moririn
annotate Todo.txt @ 780:0b791ae19543 default tip
test
| author | Moririn < Moririn@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 10 Jul 2023 20:19:13 +0900 |
| parents | 68904fdaab71 c588b77bc197 |
| children |
| rev | line source |
|---|---|
| 710 | 1 Wed May 4 22:07:32 JST 2022 |
| 2 | |
| 3 Context memory に DataGear を Binary Tree で入れる。List で良いのだが | |
| 4 Libaryの Data.Tree.Binary には insert はない ( まぁ、alloc / read / update くらいで map で書けるとか?) | |
| 5 共有データは、memory に入れる | |
| 6 free はしない(?) | |
| 7 | |
| 709 | 8 Sun May 1 15:04:57 JST 2022 |
| 9 | |
| 10 Model checking | |
| 11 | |
| 12 goto 先の番号を stub に書くのは変 | |
| 13 | |
| 14 process : context が別々 | |
| 15 thread : context 一緒、goto 先が異なる | |
| 16 context は共有 実行は codeGear は atomic | |
| 17 shared file descriptor など | |
| 18 | |
| 19 single phils direct connection single thread | |
| 20 no shared data | |
| 21 | |
| 22 multi process phils separate process | |
| 23 shared context | |
| 24 | |
| 25 multi threaded phils shared process | |
| 26 serate next | |
| 27 atomic codeGear execution | |
| 28 | |
| 29 | |
|
578
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
30 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
|
31 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
32 findNode -> replaceNode -> getRedBlackTree だが |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
33 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
34 findNode -> P0 -> replaceNode -> P1 -> getRedBlackTree |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
35 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
36 という形で証明しても良い。一挙に証明するのは,可能だろうけど、良くないはず。 |
|
7bacba816277
use list base simple stack
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
575
diff
changeset
|
37 |
| 573 | 38 Sun May 6 17:54:50 JST 2018 |
| 39 | |
| 40 do1 a $ \b -> do2 b next を、do1 と do2 に分離することはできる? | |
| 41 | |
| 42 | |
| 43 Mon Apr 30 17:15:16 JST 2018 | |
| 44 | |
| 45 Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない | |
| 46 やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい | |
| 47 | |
| 553 | 48 Mon Mar 26 17:43:06 JST 2018 |
| 49 | |
| 573 | 50 Decidable を使って Compare の場合分けを行う |
| 553 | 51 Decidable を使うと Eq から x ≡ y の証明を取り出すことができる |
| 52 場合分けには Trichotomous を使う | |
| 573 | 53 compareTri を完成させる Done |
| 553 | 54 |
| 524 | 55 Fri Jan 5 16:43:26 JST 2018 |
| 56 | |
| 57 unbalanced binary search tree の動作を調べる | |
| 58 | |
| 59 RedBlackTree の put を完成させる | |
| 60 | |
| 61 RedBlackTree の Deletion を完成させる | |
| 62 | |
| 63 unbalanced binary search tree と同様の動作をする | |
| 64 | |
| 65 木の深さの最小と最大の差が２倍を超えない | |
| 66 | |
| 67 CodeGear/DataGear が構成する圏を定義する | |
| 68 | |
| 69 goto を定義して meta 計算を可能にする | |
| 70 | |
| 71 DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする | |
| 72 | |
| 73 実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する | |
| 74 | |
| 75 Monad の合成に必要な規則を上の圏上に定義する | |
| 76 | |
| 77 synchronizedQueue の仕様をCTLを使って定義する | |
| 78 | |
| 79 Gearsで記述したsynchornizedQueueを検証する | |
| 80 | |
| 81 gotoを用いてモデル検査と証明の組み合わせを実現する | |
| 82 | |
| 83 | |
| 575 | 84 Wed Aug 27 17:52:00 JST 2019 |
| 85 | |
| 86 別で定義した TriCotomos や \=? などの Relation の関数を | |
| 87 Agdaで定義してあるものに置き換える,まとめる | |
| 88 | |
| 89 HoareLogic をベースにした SingleLinkedStack の作成 | |
| 90 | |
| 91 HoareLogic ベースの Tree の証明 |