|
573
|
1 Sun May 6 17:54:50 JST 2018
|
|
|
2
|
|
|
3 do1 a $ \b -> do2 b next を、do1 と do2 に分離することはできる?
|
|
|
4
|
|
|
5
|
|
|
6 Mon Apr 30 17:15:16 JST 2018
|
|
|
7
|
|
|
8 Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない
|
|
|
9 やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい
|
|
|
10
|
|
553
|
11 Mon Mar 26 17:43:06 JST 2018
|
|
|
12
|
|
573
|
13 Decidable を使って Compare の場合分けを行う
|
|
553
|
14 Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
|
|
|
15 場合分けには Trichotomous を使う
|
|
573
|
16 compareTri を完成させる Done
|
|
553
|
17
|
|
524
|
18 Fri Jan 5 16:43:26 JST 2018
|
|
|
19
|
|
|
20 unbalanced binary search tree の動作を調べる
|
|
|
21
|
|
|
22 RedBlackTree の put を完成させる
|
|
|
23
|
|
|
24 RedBlackTree の Deletion を完成させる
|
|
|
25
|
|
|
26 unbalanced binary search tree と同様の動作をする
|
|
|
27
|
|
|
28 木の深さの最小と最大の差が２倍を超えない
|
|
|
29
|
|
|
30 CodeGear/DataGear が構成する圏を定義する
|
|
|
31
|
|
|
32 goto を定義して meta 計算を可能にする
|
|
|
33
|
|
|
34 DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする
|
|
|
35
|
|
|
36 実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する
|
|
|
37
|
|
|
38 Monad の合成に必要な規則を上の圏上に定義する
|
|
|
39
|
|
|
40 synchronizedQueue の仕様をCTLを使って定義する
|
|
|
41
|
|
|
42 Gearsで記述したsynchornizedQueueを検証する
|
|
|
43
|
|
|
44 gotoを用いてモデル検査と証明の組み合わせを実現する
|
|
|
45
|
|
|
46
|
