summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Update dependencies and Standards-VersionGravatar Benjamin Barenblat2016-04-06
* Add gbp.confGravatar Benjamin Barenblat2015-08-30
* Get rid of Built-UsingGravatar Benjamin Barenblat2015-08-30
* Move release to unstableGravatar Benjamin Barenblat2015-08-30
* Package Dafny for experimentalGravatar Benjamin Barenblat2015-08-14
* Version 1.9.5.20511Gravatar leino2015-05-11
* Don't include arrow types among ordered types.Gravatar leino2015-05-11
* Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and Kle...Gravatar leino2015-05-10
* Additional test case for inductive predicatesGravatar leino2015-05-07
* Added "inductive lemma" methodsGravatar leino2015-05-07
* Added inductive predicatesGravatar leino2015-05-06
* Improved generation of .reads axioms (correcting an incorrect answer and corr...Gravatar leino2015-05-01
* Answer fileGravatar leino2015-05-01
* Improved encoding of a property of reads clauses to make things more easily p...Gravatar leino2015-05-01
* Added to the test suite a Dafny encoding of Chapter 3 from the Nipkow and Kle...Gravatar leino2015-04-29
* Bumped version to 1.9.4.20428Gravatar leino2015-04-29
* Added a test where Dafny verifies something that the Juggernaut tool can inferGravatar leino2015-04-28
* MergeGravatar leino2015-04-28
|\
* | Changes to the VerifyThis2015 test programsGravatar leino2015-04-28
| * added notice about vim-loves-dafny.Gravatar Michael Lowell Roberts2015-04-27
| * Fix issue #72. Add the constructor questionmark to a function's axiom if theGravatar qunyanm2015-04-24
* | Fixed bug in tuplesGravatar leino2015-04-24
| * Rearranged handling ambiguously named declarations, so that the multitudes of...Gravatar Rustan Leino2015-04-22
| * Fix issue #70. Check the ctors for equality before marking them as duplicates.Gravatar qunyanm2015-04-21
| * Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap.Gravatar qunyanm2015-04-20
| * Fix issue #69. If we can't find a member in classMembers, search the staticGravatar qunyanm2015-04-17
| * HashCode for Set/MultiSet/Map should be independent of the order of theGravatar qunyanm2015-04-17
| * Change GetHashCode for Set, MultiSet and MapGravatar qunyanm2015-04-16
| * Fix issue #71. When substitute the forall's variables for those of theGravatar qunyanm2015-04-16
| * Fix issue #68. Change GetHashCode implementation for Sequence.Gravatar qunyanm2015-04-14
|/
* Completed problems from the VerifyThis 2015 program verification competitionGravatar leino2015-04-14
* Fix issue #67. Check SupportsEquality before determining whether to emit EqualsGravatar qunyanm2015-04-13
* Include axioms about $Is and $IsAlloc for traitsGravatar leino2015-04-07
* Support calls to static trait methods/functions via the classGravatar leino2015-04-07
* MergeGravatar leino2015-04-07
|\
* | Revised look-up and compilation of inherited trait members (static functions/...Gravatar leino2015-04-07
| * Make sure that PrintTopLevelDecls receives program FullName, not just Name, s...Gravatar chrishaw2015-04-07
|/
* Changed version to 1.9.3.20406 and updated copyright year to include 2015.Gravatar leino2015-04-06
* Copy z3.exe and Z3-LICENSE.txt (from Binaries directory to Source/DafnyExtens...Gravatar leino2015-04-06
* MergeGravatar leino2015-04-06
|\
| * MergeGravatar qunyanm2015-04-06
| |\
| * | Add z3.exe and z3-license.txt to dafny binary and extension distribution.Gravatar qunyanm2015-04-06
* | | Fixed missing case in previous check-inGravatar leino2015-04-05
| |/ |/|
* | Fixed compilation of static members in traitsGravatar leino2015-04-05
* | Fixed some bugs in override axioms (but still missing support for classes wit...Gravatar leino2015-04-05
* | Whitespace deltas in test files (in particular, removing tabs and adjusting s...Gravatar leino2015-04-03
* | MergeGravatar leino2015-04-03
|\|
* | Added test cases and fixes for overrides termination checksGravatar leino2015-04-03
| * Eliminate redundant checks of newtype and opaque function well-formedness fro...Gravatar chrishaw2015-04-02
|/
* Reflect cleaner syntax in some test programsGravatar leino2015-03-31