メタ計算を用いた Continuation based C の検証手法
Yasutaka Higa

プログラミング言語とソフトウェアの信頼性

二つのアプローチを用いたソフトウェア検証

モデル検査的アプローチについての流れ

Continuation based C

CodeSegment

goto

DataSegment

csds

メタ計算

meta

Meta CodeSegment

Meta DataSegment

並列に信頼性高く動作する GearsOS

赤黒木

GearsOS における赤黒木の利用例(ノードの挿入)

put

仕様の記述とその確認

既存のモデル検査器 spin

既存のモデル検査器 CBMC

メタ計算ライブラリ akasha

akashaPut

チェックする仕様

void verifySpecification(struct Context* context, struct Tree* tree) {
    assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1)));
        goto meta(context, EnumerateInputs);
    }

akasha と CBMC の比較

定理証明的なアプローチの流れ

定理証明を Continuation based C へ適用するには

Agda と DataSegment

__code cs0(int a, int b){
  goto cs1(a+b);
}

record ds0 : Set where
  field
    a : Int
    b : Int

Agda と CodeSegment

__code cs0(int a, int b){
  goto cs1(a+b);
}

cs0 : CodeSegment ds0 ds1
cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))

メタレベルの型付け

Agda 上のメタ計算

main : ds1
main = goto cs0 (record {a = 100 ; b = 50})

main : Meta
main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})

Agda 上に CbC を記述した成果

まとめ

今後の課題