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