CODEWITHSUNDEEP
dafny
Pablo M. S. Farias
Pablo M. S. Farias

Reputation: 121

Trivial Assertions about Sets not Verifying in Dafny

Tutorial Collections contains the following code

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

which, however, currently does not verify in the Dafny system available at rise4fun:

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

This simpler example

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

doesn't verify either:

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

I think both examples should verify; am I missing something?

Upvotes: 2

Views: 160

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

These are both true. There was a missing condition in Dafny's encoding that made these not verify. I fixed it. Thanks for the bug report.

Rustan

Upvotes: 3

Related Questions