summaryrefslogtreecommitdiff
Commit message (Collapse)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
| | | | | See Debian bug #688251. There are no licensing issues with Boogie, so we don’t need to be aware of the original source.
* 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
| | | | | | 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 ↵Gravatar leino2015-05-10
| | | | | | Klein book on semantics. It includes many uses of inductive predicates and inductive lemmas.
* 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 ↵Gravatar leino2015-05-01
| | | | corresponding incorrectly recorded desired answer)
* Answer fileGravatar leino2015-05-01
|
* Improved encoding of a property of reads clauses to make things more easily ↵Gravatar leino2015-05-01
| | | | provable.
* Added to the test suite a Dafny encoding of Chapter 3 from the Nipkow and ↵Gravatar leino2015-04-29
| | | | Klein book on semantics
* 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
| | | | | | | | function has a MemberSelectExpr that accesses a type with only one constructor.
* | Fixed bug in tuplesGravatar leino2015-04-24
| |
| * Rearranged handling ambiguously named declarations, so that the multitudes ↵Gravatar Rustan Leino2015-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.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
| | | | | | | | members of the enclosing module or its imports.
| * HashCode for Set/MultiSet/Map should be independent of the order of theGravatar qunyanm2015-04-17
| | | | | | | | elements.
| * 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
| | | | | | | | fn in fixupRevealLemma substitute the types as well.
| * 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
| | | | or == for equality testing.
* 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 ↵Gravatar leino2015-04-07
| | | | | | | | functions/methods don't work yet)
| * Make sure that PrintTopLevelDecls receives program FullName, not just Name, ↵Gravatar chrishaw2015-04-07
|/ | | | so that printMode NoIncludes/NoGhost works
* 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 ↵Gravatar leino2015-04-06
| | | | Source/DafnyExtension directory) as pre-build events
* 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 ↵Gravatar leino2015-04-05
| | | | | | | | | | | | | | with type parameters). Resolve ClassDecl.TraitsTyp as types. Moved declaration of TraitParent and NoTraitAtAll to prelude.
* | Whitespace deltas in test files (in particular, removing tabs and adjusting ↵Gravatar leino2015-04-03
| | | | | | | | some indentation)
* | MergeGravatar leino2015-04-03
|\|
* | Added test cases and fixes for overrides termination checksGravatar leino2015-04-03
| | | | | | | | Removed syntactic presence checks for specifications--these will be checked semantically by the verifier
| * Eliminate redundant checks of newtype and opaque function well-formedness ↵Gravatar chrishaw2015-04-02
|/ | | | from included files
* Reflect cleaner syntax in some test programsGravatar leino2015-03-31
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 15:51:43 +0000