dafnyは、失敗したアサーションのカウンタの例を表示できますか？

Question

私は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は、このような例を単独で提供できますか？

Answer 1

ビジュアルスタジオ内線でDafnyを実行すると、失敗したアサーションの横に赤い点が表示されます。赤い点をクリックすると、確認のデバッグビューが表示されます。これはカウンタの例を示します（変数の評価を伴う実行トレースです）。

Answer 2

Visual Studioのコードのプラグインが用意されました：https://marketplace.visualstudio.com/items?itemName=FunctionalCorrectness.dafny-vscode

あなたはカウンターの例を示すために、F7を押すことができますが、それはあなたの例のために非常に読みやすいではありません：コマンドラインで

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