Mon Mar 26 17:43:06 JST 2018

    Decidable を使って Compare の場合分けを行う
    Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
    場合分けには Trichotomous を使う
    compareTri を完成させる               

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を用いてモデル検査と証明の組み合わせを実現する