Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Change behavior of 'decreases *', which can be applied to loops and methods. ↵ | Rustan Leino | 2014-08-19 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now, loops that may possibly do an infinite number of iterations (that is, loops marked with 'decreases *') and calls to methods marked with 'decreases *' are allowed only in methods that themselves are marked with 'decreases *'. As before, ghost loops and ghost methods are not allowed to be marked with 'decreases *'. Previously, 'decreases *' was allowed on a method only if the method was tail recursive; this is no longer so. Note, however, that if the method is not tail recursive and engages in infinite recursion, then it will eventually run out of stack space. Previously, a 'decreases *' was not inherited in a refining module; this is no longer so. That is, 'decreases *' is now inherited. To refine a possibly non-terminating method or loop, the refining version simply provides a decreases clause that does not mention '*'. Note that if the refined method is not recursive, it still needs to have _some_ decreases clause in order not to inherit the 'decreases *' from the refined method, but the expression stated in the decreases clause can be arbitrary (for example, one can write 'decreases true' or 'decreases 7' or 'decreases x' for some 'x' in scope). Note, in the new design, a method needs to be declared with 'decreases *' if it may recurse forever _or_ if it contains a possibly infinite loop. Note that the absence of 'decreases *' on a loop does not mean the loop will terminate, but it does mean that the loop will iterate a finite number of times (the subtle distinction here is that a loop without a 'decreases *' is allowed to contain a nested loop that has a 'decreases *' -- provided the enclosing method is also declared with 'decreases *', as previously mentioned). | ||
* | Add higher-order-functions and some other goodies | Dan Rosén | 2014-08-11 |
| | | | | | | | | | | | | | | | | * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter | ||
* | Improved AnalyzeList encoding in a way that performs way better. | Rustan Leino | 2014-07-09 |
| | | | | Cleaned up file to use some improved Dafny constructs. | ||
* | Merge | Dan Rosén | 2014-07-07 |
|\ | |||
* | | New logical encoding of types with Is and IsAlloc | Dan Rosén | 2014-07-07 |
| | | |||
| * | Removed the old test infrastructure. | wuestholz | 2014-07-01 |
| | | |||
* | | Made the snapshotable trees test "unsupported" instead of "unresolved". | wuestholz | 2014-06-05 |
| | | |||
| * | Made the snapshotable trees test "unsupported" instead of "unresolved". | wuestholz | 2014-06-05 |
|/ | |||
* | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
| | |||
* | Renamed a constructor in a test file | Rustan Leino | 2014-01-03 |
| | |||
* | Add support for the /verifySeparately flag in Boogie and change most tests ↵ | wuestholz | 2013-12-18 |
| | | | | to use it. | ||
* | Update an 'Answer' file. | wuestholz | 2013-12-10 |
| | |||
* | Change a test program to verify faster (by a factor of 10-25). | wuestholz | 2013-12-10 |
| | |||
* | Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ↵ | Rustan Leino | 2013-04-01 |
| | | | | | | | where more type information is known Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement. Fixed numerous places where some recursive checks did not reach. | ||
* | Renamed "parallel" statement to "forall" statement, and made the parentheses ↵ | Rustan Leino | 2013-03-06 |
| | | | | around the bound variables optional. | ||
* | Added tests: parallel calc, better well-formedness checks, calc expression. | Nadia Polikarpova | 2013-02-15 |
| | |||
* | Updated a test in dafny2 with the new calc syntax. | Nadia Polikarpova | 2013-02-14 |
| | |||
* | Merge | Nadia Polikarpova | 2013-02-14 |
|\ | |||
| * | Report error if type of a quantified variable cannot be inferred | Rustan Leino | 2013-02-11 |
| | | |||
* | | Changed calc syntax (custom operators are now written before the hint) | Nadia Polikarpova | 2013-02-08 |
|/ | |||
* | renamed "abstract module" to "module facade" | Rustan Leino | 2012-10-22 |
| | | | | renamed "ghost module" to "abstract module", adding a keyword "abstract" | ||
* | added two "calc" proofs (by Nadia) of the MajorityVote example | Unknown | 2012-10-19 |
| | |||
* | improved and fixed compilation and resolution of assign-such-that statements | Rustan Leino | 2012-10-05 |
| | |||
* | Fixed some goof-ups in the test script edits | Rustan Leino | 2012-10-04 |
| | | | | Changed the test output to make it easier to spot (in the console output) that everything passed with success or if there were any failures | ||
* | Added Test/dafny3 and another test file for iterators (hey, you can even run ↵ | Rustan Leino | 2012-10-04 |
| | | | | | | Iter.dfy!) Fixed migration issues | ||
* | Use expression splitting for checking calculation steps | Nadia Polikarpova | 2012-09-23 |
| | |||
* | Allow multiple calc/block statements in a hint. Removed the empty calc test ↵ | Nadia Polikarpova | 2012-09-19 |
| | | | | from dafny2/Calculations, as it actually belongs in dafny0. | ||
* | Allow empty calc statements | Nadia Polikarpova | 2012-09-19 |
| | |||
* | Dafny: some test cases for "calc" (very cool!) | Unknown | 2012-09-17 |
| | |||
* | Dafny: added MonotonicHeapstate refinement example | Unknown | 2012-08-09 |
| | |||
* | Dafny: updated test suite to new syntax | Jason Koenig | 2012-07-30 |
| | |||
* | Dafny: restored soundness for refinement by disallowing certain updates and ↵ | Jason Koenig | 2012-07-11 |
| | | | | method calls | ||
* | Dafny: reinstated autocontracts | Jason Koenig | 2012-07-02 |
| | |||
* | Dafny: fixed up test suite (temporarily removed autocontract tests) | Jason Koenig | 2012-06-28 |
| | |||
* | Dafny: fixed some test cases | Jason Koenig | 2012-06-28 |
| | |||
* | Undo bad merge. | afd | 2012-06-27 |
| | |||
* | Merge | Unknown | 2012-06-25 |
|\ | |||
| * | Dafny: Since it's no longer true that all types support equality at run-time ↵ | Unknown | 2012-06-21 |
| | | | | | | | | (in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation. | ||
* | | Merged with default. | chmaria | 2012-06-18 |
|\| | |||
| * | Dafny: fixed a couple of compiler bugs | Unknown | 2012-06-14 |
| | | |||
| * | Dafny: cleaned up test scripts a little | Unknown | 2012-06-14 |
| | | |||
| * | Dafny: added another version of the majority finding algorithm to the test suite | Unknown | 2012-06-12 |
| | | |||
| * | Dafny: beefed up allocation axioms for boxes stored in fields | Unknown | 2012-06-12 |
| | | |||
* | | Dafny: Added tests. | chmaria | 2012-06-12 |
| | | |||
| * | Dafny: added some test programs | Rustan Leino | 2012-06-08 |
|/ | |||
* | Dafny: support assign-such-that in var declarations in refinements | Unknown | 2012-03-15 |
| | |||
* | Dafny: added StoreAndRetrieve refinement example | Unknown | 2012-03-15 |
| | |||
* | Dafny: implemented thresholds for the new interval domain (/infer:j) | Rustan Leino | 2011-12-12 |
| | |||
* | Dafny tests: Disabled SnapshotableTrees.dfy for now while performance issues ↵ | Rustan Leino | 2011-12-07 |
| | | | | are being investigated | ||
* | Dafny: call C# compiler directly from inside Dafny, and optionally produce a ↵ | Rustan Leino | 2011-11-22 |
| | | | | .cs file with the new /spillTargetCode switch |