Can't always prove s == s[0..|s|]

Sep 24, 2015 at 2:12 AM
Consider the following code (found http://rise4fun.com/Dafny/UKVz).
method m0(s:seq<int>) { assert s == s[0..|s|]; }
// method m1(s:seq<int>) ensures s == s[0..|s|]; { assert s == s[0..|s|]; }
// method m2(s:seq<int>) ensures s == s[0..|s|]; {}
Execution results in
Dafny program verifier finished with 2 verified, 0 errors
But if I comment m0 and uncomment either m1 or m2 then Dafny is unable to prove the same property as the one asserted in m0 (I'm using Dafny online. What happens is that it yields no result).

Why?

Thanks
Sep 24, 2015 at 5:46 PM
Might be try to install Dafny on your machine. all verified, no problem.
Sep 24, 2015 at 6:44 PM
Thanks for confirming that you can get them all to be proven when running Dafny locally (I'm not in a position to set it up that way yet). So I guess it must have been a (temporary?) consequence of using the online version.
Coordinator
Sep 25, 2015 at 1:55 AM
Your programs verify for me, too, both online (http://rise4fun.com/Dafny/YCX0) and locally.

Btw, there is a new spiffy emacs mode for Dafny with installers for all platforms. We will release these shortly. Would you be in a position to use Dafny that way?

Rustan
Sep 25, 2015 at 5:12 PM
rustanleino wrote:
Your programs verify for me, too, both online (http://rise4fun.com/Dafny/YCX0) and locally.
Good, because I found that behavior quite surprising.
Btw, there is a new spiffy emacs mode for Dafny with installers for all platforms.
Great!
We will release these shortly. Would you be in a position to use Dafny that way?
Yes, I have been working exclusively in Emacs of late.
Sep 29, 2015 at 8:01 PM
rustanleino wrote:
... Dafny with installers for all platforms. We will release these shortly.
Might it be possible to bump up the timeout a little for Dafny online in the meantime? :)

Thanks,
Patrice

p.s. Rustan: did you get my e-mail of Sep. 19?
Coordinator
Oct 12, 2015 at 9:21 PM
The new release is out. Give it a whirl.

Rustan