Mercurial > hg > Gears > GearsAgda

changeset 784:2955d5b7debd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merge
author Moririn < Moririn@cr.ie.u-ryukyu.ac.jp>
date Mon, 21 Aug 2023 19:06:34 +0900
parents dca93aef5e36 (current diff) f7e1704305df (diff)
children c3cce455e4e7
files Todo.txt hoareBinaryTree1.agda
diffstat 1 files changed, 15 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/Todo.txt	Mon Aug 21 19:01:36 2023 +0900
+++ b/Todo.txt	Mon Aug 21 19:06:34 2023 +0900
@@ -1,3 +1,18 @@
+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 で良いのだが