些細なアサーションは

Question

チュートリアルCollectionsは、次のコードが、現在rise4funで利用可能Dafnyシステムで検証されない、

method m() 
{ 
    assert (set x | x in {0,1,2,3,4,5} && x < 3) == {0,1,2}; 
} 

が含まれていDafnyで確認ではありません

method m() { assert (set x : nat | x in {0}) == {0}; } 

は確認していませんer：

stdin.dfy(1,21): Warning: /!\ No terms found to trigger on. 
stdin.dfy(1,45): Error: assertion violation 
Dafny program verifier finished with 0 verified, 1 error 

私は両方の例で検証する必要があります。私は何かを欠いている？

Answer 1

これらはどちらも真です。 Dafnyのエンコーディングに欠落していた条件があり、これが検証されませんでした。それを私が直した。バグレポートをありがとう。

ルスタン