Mercurial > hg > Gears > GearsAgda
view Todo.txt @ 793:08e04ed15468
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 21 Oct 2023 18:51:25 +0900 |
parents | 2955d5b7debd |
children | 91137bc52ddd |
line wrap: on
line source
Mon Jul 3 19:04:29 JST 2023 Red Black Tree の Invariant を完成させる GearsOS のコードとの対応を取る (既にバグがあることがわかってる) バグはメタ部分にある pointer (CbCはCだから pointer がある) heap (CbCは GC もってない。なので、メモリリークしてる) Meta計算部分を含む Invariant になる ここまで複雑で実用になる? 部分ではそんなに難しくはない? Wed May 4 22:07:32 JST 2022 Context memory に DataGear を Binary Tree で入れる。List で良いのだが Libaryの Data.Tree.Binary には insert はない ( まぁ、alloc / read / update くらいで map で書けるとか?) 共有データは、memory に入れる free はしない(?) Sun May 1 15:04:57 JST 2022 Model checking goto 先の番号を stub に書くのは変 process : context が別々 thread : context 一緒、goto 先が異なる context は共有 実行は codeGear は atomic shared file descriptor など single phils direct connection single thread no shared data multi process phils separate process shared context multi threaded phils shared process serate next atomic codeGear execution Thu May 17 15:26:56 JST 2018 findNode -> replaceNode -> getRedBlackTree だが findNode -> P0 -> replaceNode -> P1 -> getRedBlackTree という形で証明しても良い。一挙に証明するのは,可能だろうけど、良くないはず。 Sun May 6 17:54:50 JST 2018 do1 a $ \b -> do2 b next を、do1 と do2 に分離することはできる? Mon Apr 30 17:15:16 JST 2018 Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい Mon Mar 26 17:43:06 JST 2018 Decidable を使って Compare の場合分けを行う Decidable を使うと Eq から x ≡ y の証明を取り出すことができる 場合分けには Trichotomous を使う compareTri を完成させる Done Fri Jan 5 16:43:26 JST 2018 unbalanced binary search tree の動作を調べる RedBlackTree の put を完成させる RedBlackTree の Deletion を完成させる unbalanced binary search tree と同様の動作をする 木の深さの最小と最大の差が2倍を超えない CodeGear/DataGear が構成する圏を定義する goto を定義して meta 計算を可能にする DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする 実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する Monad の合成に必要な規則を上の圏上に定義する synchronizedQueue の仕様をCTLを使って定義する Gearsで記述したsynchornizedQueueを検証する gotoを用いてモデル検査と証明の組み合わせを実現する Wed Aug 27 17:52:00 JST 2019 別で定義した TriCotomos や \=? などの Relation の関数を Agdaで定義してあるものに置き換える,まとめる HoareLogic をベースにした SingleLinkedStack の作成 HoareLogic ベースの Tree の証明