4

Dafnyを使って以下のプログラムの正誤を証明しようとしています。

datatype List<T> = Nil | Cons(T, List)
function tail(l:List):List
{
    match l
    case Nil => Nil
    case Cons(x,xs) => xs
}
method check(l:List) 
{
    assert(expr(l)!=2);
}
function expr(l : List):int
{
    if(l == Nil) then 0 
    else if(tail(l)==Nil) then 1 
    else if(tail(tail(l)) == Nil) then 2 
    else 3
}

Dafny は、アサーションが正しくないことを証明することに成功しました。ただし、アサーションが失敗した例は示していません。Dafny だけでそのような例を挙げることができますか?

4

2 に答える 2

4

現在、ビジュアル スタジオ コード用のプラグインがあります: https://marketplace.visualstudio.com/items?itemName=FunctionalCorrectness.dafny-vscode

を押しF7てカウンターの例を表示できますが、あなたの例ではあまり読みにくいです:

ダフニーのスクリーンショット

コマンドラインでは、次のmvオプションを使用できますDafny.exe -mv:model.bvd myfile.dfy。これにより、モデルが という名前のファイルに保存されますmodel.bvdが、上のスクリーンショットよりもさらに読みにくくなっています (プラグインが何らかの後処理を行っているようです)。

于 2017-07-11T09:29:43.733 に答える
2

Visual Studio 拡張機能で Dafny を実行すると、失敗したアサーションの横に赤い点が表示されます。赤い点をクリックすると、検証デバッグ ビューが表示されます。これは、カウンターの例 (変数の評価を伴う実行トレース) を示しているはずです。

于 2016-10-02T10:12:21.653 に答える