view Todo.txt @ 524:5f684d39832e

add Todo.txt
author ryokka
date Fri, 05 Jan 2018 17:23:06 +0900
parents
children 7d9af1d4b5af
line wrap: on
line source

Fri Jan  5 16:43:26 JST 2018

    unbalanced binary search tree の動作を調べる

    RedBlackTree の put を完成させる

    RedBlackTree の Deletion を完成させる

                 unbalanced binary search tree と同様の動作をする

                  木の深さの最小と最大の差が2倍を超えない

    CodeGear/DataGear が構成する圏を定義する

    goto を定義して meta 計算を可能にする

    DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする

    実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する

    Monad の合成に必要な規則を上の圏上に定義する

    synchronizedQueue の仕様をCTLを使って定義する

    Gearsで記述したsynchornizedQueueを検証する

    gotoを用いてモデル検査と証明の組み合わせを実現する