Mercurial > hg > Gears > GearsAgda

changeset 524:5f684d39832e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add Todo.txt
author ryokka
date Fri, 05 Jan 2018 17:23:06 +0900
parents 8fbc3ef749b6
children 0696b9846415
files Todo.txt
diffstat 1 files changed, 29 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Todo.txt	Fri Jan 05 17:23:06 2018 +0900
@@ -0,0 +1,29 @@
+Fri Jan  5 16:43:26 JST 2018
+
+    unbalanced binary search tree の動作を調べる
+
+    RedBlackTree の put を完成させる
+
+    RedBlackTree の Deletion を完成させる
+
+                 unbalanced binary search tree と同様の動作をする
+
+                  木の深さの最小と最大の差が２倍を超えない
+
+    CodeGear/DataGear が構成する圏を定義する
+
+    goto を定義して meta 計算を可能にする
+
+    DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする
+
+    実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する
+
+    Monad の合成に必要な規則を上の圏上に定義する
+
+    synchronizedQueue の仕様をCTLを使って定義する
+
+    Gearsで記述したsynchornizedQueueを検証する
+
+    gotoを用いてモデル検査と証明の組み合わせを実現する
+
+