Mercurial > hg > Members > Moririn

annotate Todo.txt @ 561:1bbbd787472e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
trichotomos on ≤′ done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Mar 2018 10:17:07 +0900
parents 7d9af1d4b5af
children 8777baeb90f8
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
553
7d9af1d4b5af add compareTri
ryokka
parents: 524
diff changeset
1 Mon Mar 26 17:43:06 JST 2018
7d9af1d4b5af add compareTri
ryokka
parents: 524
diff changeset
2
7d9af1d4b5af add compareTri
ryokka
parents: 524
diff changeset
3 Decidable を使って Compare の場合分けを行う
7d9af1d4b5af add compareTri
ryokka
parents: 524
diff changeset
4 Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
7d9af1d4b5af add compareTri
ryokka
parents: 524
diff changeset
5 場合分けには Trichotomous を使う
7d9af1d4b5af add compareTri
ryokka
parents: 524
diff changeset
6 compareTri を完成させる
7d9af1d4b5af add compareTri
ryokka
parents: 524
diff changeset
7
524
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
8 Fri Jan 5 16:43:26 JST 2018
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
9
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
10 unbalanced binary search tree の動作を調べる
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
11
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
12 RedBlackTree の put を完成させる
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
13
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
14 RedBlackTree の Deletion を完成させる
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
15
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
16 unbalanced binary search tree と同様の動作をする
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
17
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
18 木の深さの最小と最大の差が２倍を超えない
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
19
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
20 CodeGear/DataGear が構成する圏を定義する
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
21
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
22 goto を定義して meta 計算を可能にする
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
23
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
24 DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
25
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
26 実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
27
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
28 Monad の合成に必要な規則を上の圏上に定義する
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
29
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
30 synchronizedQueue の仕様をCTLを使って定義する
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
31
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
32 Gearsで記述したsynchornizedQueueを検証する
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
33
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
34 gotoを用いてモデル検査と証明の組み合わせを実現する
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
35
5f684d39832e add Todo.txt
ryokka
parents:
diff changeset
36