メタ計算を用いた 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

チェックする仕様

__code verifySpecificationFinish(struct Context* context) {
    if (context->data[AkashaInfo]->akashaInfo.maxHeight >
        2*context->data[AkashaInfo]->akashaInfo.minHeight)
    {
        context->next = Exit;
        goto meta(context, ShowTrace);
    }
    goto meta(context, DuplicateIterator);
}

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 を記述した成果

まとめ

今後の課題