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