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

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

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

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

Continuation based C

CodeSegment

cs

DataSegment

ds

メタ計算

meta

Meta CodeSegment

mcs

Meta DataSegment

mds

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

赤黒木

rbtree

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);
}

data CodeSegment (A B : Set) : Set where
  cs : (A -> B) -> CodeSegment 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 を記述した成果

まとめ

今後の課題