Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add the beginning of a new testing infrastructure | 2015-06-08 | |
| | | | | | | | | | | | | runTests.py reads lit-style annotations, so we will be able to retain lit compatibility. This new framework adds: * Precise timings * Proper support for interrupting using Ctrl+C * Much better reporting (including tracking of error codes, and merging of successive reports for performance tracking) * No dependency on lit, OutputCheck, or Diff * Pretty colors! | ||
* | Fix the Seq#Contain axiom; it should talk about T, not ref. | 2015-06-07 | |
| | |||
* | Generate #requires function for OpaqueFunction. | 2015-06-04 | |
| | |||
* | Added {:auto_generated} trigger, which indicates that a declaration was not ↵ | 2015-06-02 | |
| | | | | explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations. | ||
* | Merge | 2015-05-29 | |
|\ | |||
| * | Add an infinite set collection type. | 2015-05-29 | |
| | | |||
* | | Improvements in traits test case | 2015-05-29 | |
| | | |||
* | | Improvements to Nipkow and Klein test cases: Changed imap to map, removed ↵ | 2015-05-29 | |
| | | | | | | | | need for Total | ||
* | | Merge | 2015-05-29 | |
|\| | |||
* | | Bug fix in type-antecedent for traits in allocation axioms | 2015-05-29 | |
| | | |||
| * | Merge | 2015-05-29 | |
| |\ | |||
| * | | Changes to ComputeFreeVariables--bug fix as well as beautification | 2015-05-29 | |
| | | | |||
| | * | Fix build break. Part of the change was not checked in last check-in somehow. | 2015-05-19 | |
| | | | |||
| | * | Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination. | 2015-05-18 | |
| | | | |||
| | * | DafnyExtension: Added experimental support for diagnosing timeouts. | 2015-05-18 | |
| | | | |||
| | * | Updated test output after change in Boogie. | 2015-05-17 | |
| | | | |||
| | * | Fix issue #79. Allow tuple pattern matching with parenthesis only. | 2015-05-15 | |
| | | | |||
| | * | Allow MatchExpr and MatchStmt to have nested patterns. Such as | 2015-05-14 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | function last<T>(xs: List<T>): T requires xs != Nil { match xs case Cons(y, Nil) => y case Cons(y, Cons(z, zs)) => last(Cons(z, zs)) } And function minus(x: Nat, y: Nat): Nat { match (x, y) case (Zero, _) => Zero case (Suc(_), Zero) => x case (Suc(a), Suc(b)) => minus(a, b) } | ||
| | * | Update the configuration manager so the Debug build actually builds the ↵ | 2015-05-13 | |
| | | | | | | | | | | | | | | | | | | Debug version of the projects (rather than Checked). The Checked build still builds the Checked version of the projects. | ||
| | * | Fixed typo in the Dafny Emacs mode. | 2015-05-12 | |
| |/ |/| | |||
* | | Version 1.9.5.20511 | 2015-05-11 | |
| | | |||
* | | Don't include arrow types among ordered types. | 2015-05-11 | |
| | | | | | | | | | | | | Fix bug with not seeing imap's because of type synonyms. Don't show semi-colon after "decreases" in hover text. Minor cosmetic change in a test case. | ||
* | | Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and ↵ | 2015-05-10 | |
| | | | | | | | | | | | | Klein book on semantics. It includes many uses of inductive predicates and inductive lemmas. | ||
* | | Additional test case for inductive predicates | 2015-05-07 | |
| | | |||
* | | Added "inductive lemma" methods | 2015-05-07 | |
| | | |||
* | | Added inductive predicates | 2015-05-06 | |
| | | |||
* | | Improved generation of .reads axioms (correcting an incorrect answer and ↵ | 2015-05-01 | |
| | | | | | | | | corresponding incorrectly recorded desired answer) | ||
* | | Answer file | 2015-05-01 | |
| | | |||
* | | Improved encoding of a property of reads clauses to make things more easily ↵ | 2015-05-01 | |
| | | | | | | | | provable. | ||
* | | Added to the test suite a Dafny encoding of Chapter 3 from the Nipkow and ↵ | 2015-04-29 | |
| | | | | | | | | Klein book on semantics | ||
* | | Bumped version to 1.9.4.20428 | 2015-04-29 | |
| | | |||
* | | Added a test where Dafny verifies something that the Juggernaut tool can infer | 2015-04-28 | |
| | | |||
* | | Merge | 2015-04-28 | |
|\| | |||
* | | Changes to the VerifyThis2015 test programs | 2015-04-28 | |
| | | |||
| * | added notice about vim-loves-dafny. | 2015-04-27 | |
| | | |||
| * | Fix issue #72. Add the constructor questionmark to a function's axiom if the | 2015-04-24 | |
| | | | | | | | | function has a MemberSelectExpr that accesses a type with only one constructor. | ||
* | | Fixed bug in tuples | 2015-04-24 | |
| | | |||
| * | Rearranged handling ambiguously named declarations, so that the multitudes ↵ | 2015-04-22 | |
| | | | | | | | | | | | | | | | | of ambiguous names that arise when layers of modules are opened-imported don't cause gross memory waste. In particular, previously, the names of many such ambiguous declarations were shown to exceed 1 million characters, the way they had been constructed. Now, multiple imports of the same declaration are immediatley resolved as not being ambiguous. | ||
| * | Fix issue #70. Check the ctors for equality before marking them as duplicates. | 2015-04-21 | |
| | | |||
| * | Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap. | 2015-04-20 | |
| | | |||
| * | Fix issue #69. If we can't find a member in classMembers, search the static | 2015-04-17 | |
| | | | | | | | | members of the enclosing module or its imports. | ||
| * | HashCode for Set/MultiSet/Map should be independent of the order of the | 2015-04-17 | |
| | | | | | | | | elements. | ||
| * | Change GetHashCode for Set, MultiSet and Map | 2015-04-16 | |
| | | |||
| * | Fix issue #71. When substitute the forall's variables for those of the | 2015-04-16 | |
| | | | | | | | | fn in fixupRevealLemma substitute the types as well. | ||
| * | Fix issue #68. Change GetHashCode implementation for Sequence. | 2015-04-14 | |
|/ | |||
* | Completed problems from the VerifyThis 2015 program verification competition | 2015-04-14 | |
| | |||
* | Fix issue #67. Check SupportsEquality before determining whether to emit Equals | 2015-04-13 | |
| | | | | or == for equality testing. | ||
* | Include axioms about $Is and $IsAlloc for traits | 2015-04-07 | |
| | |||
* | Support calls to static trait methods/functions via the class | 2015-04-07 | |
| | |||
* | Merge | 2015-04-07 | |
|\ |