termination metric

http://rise4fun.com/Dafny/yLsls Why the hover text in MVS says only "decreases" for the outermost while?

Id #174 | Release: None | Updated: Oct 11, 2016 at 2:30 PM by jiplucap | Created: Oct 11, 2016 at 2:02 PM by jiplucap

Assertion violation - induction hypothesis

Please, some help with the following assertion violation http://rise4fun.com/Dafny/cLnNL

Id #173 | Release: None | Updated: Oct 3, 2016 at 4:01 PM by jiplucap | Created: Sep 20, 2016 at 10:21 AM by jiplucap

attribute parsing does not allow type parameters

If f is a polymorphic function with one type argument, then (for example) f<int> is a legal expression in Dafny. Depending on the context, f may also be a legal expression, provided that the type ...

Id #172 | Release: None | Updated: Jun 18, 2016 at 12:18 AM by rustanleino | Created: Jun 18, 2016 at 12:18 AM by rustanleino

Empty set membership assertion produces Boogie error

The code assert forall x:int :: x !in {}; produces the following error message stdin.dfy(2,9): Error: trigger must mention all quantified variables, but does not mention: x#1 1 name resolution err...

Id #171 | Release: None | Updated: Jun 17, 2016 at 10:44 PM by laurejt | Created: Jun 17, 2016 at 10:44 PM by laurejt

Something wrong in release notes

In the release notes for version 1.9.7 we can read "/autoTriggers:1 is default in Visual Studio IDE (soon to become the default also in the Emacs IDE and from the command line)". However, /autoTrig...

Id #163 | Release: None | Updated: May 7, 2016 at 1:08 PM by ruvus | Created: May 7, 2016 at 9:55 AM by ruvus

hover text about triggers

The hover text "no terms found to trigger on" seems to suggest that the related quantifier cannot be proved because "we have not triggers on disposal", though the corresponding assertion is not vio...

Id #158 | Release: None | Updated: Apr 20, 2016 at 2:39 PM by jiplucap | Created: Apr 20, 2016 at 11:15 AM by jiplucap

A timed out

Please, have a look to the lemma proof: http://rise4fun.com/Dafny/jead I cannot think what is the problem there!!! Some help, please?

Id #157 | Release: None | Updated: May 6, 2016 at 11:51 PM by rustanleino | Created: Apr 14, 2016 at 3:13 PM by jiplucap

Strange parsing interaction between calc statements and set displays

The following code fails to parse. Is this the intended behavior? method Main() { calc { {0}; {} + {0}; // Error at the beginning of this line } }

Id #156 | Release: None | Updated: Apr 12, 2016 at 1:12 AM by wilcoxjay | Created: Apr 12, 2016 at 1:12 AM by wilcoxjay

Dafny flaged as a Trojan by 360

After downloading the latest Dafny version for windows, the zip was flagged as containing a Trojan. See the attachment for details.

Id #154 | Release: None | Updated: Apr 11, 2016 at 3:43 PM by Tapanito | Created: Apr 11, 2016 at 3:43 PM by Tapanito

Different verification results under equivalent if conditions

The following example is tested in the latest build of Dafny and also at rise4fun: lemma SetLemma1<T> (s1: set<T>, s2: set<T>) requires s1 < s2 ensures |s1| < |s2| { var e :| e in s2 - s1; // Wi...

Id #153 | Release: None | Updated: Apr 19, 2016 at 7:51 PM by ericpony | Created: Apr 9, 2016 at 6:20 PM by ericpony