summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Expand)AuthorAge
* Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for lite...Gravatar Rustan Leino2014-02-13
* Preliminary support for reals in Dafny specs. No compiler suport yet.Gravatar Bryan Parno2014-02-10
* MergeGravatar Rustan Leino2014-01-08
|\
* | Allow left-hand sides of a let expression to be patterns (like in the case of...Gravatar Rustan Leino2014-01-08
| * Compile assign-such-that for all integers, not just ones where a bound is foundGravatar Rustan Leino2014-01-06
|/
* Print and translate "match" expressions in general positions, not just at the...Gravatar Rustan Leino2014-01-03
* Embellished axioms about GenericAlloc and DtAlloc.Gravatar Rustan Leino2014-01-03
* Fix some things due to changes in Boogie (execution engine API, 'UnivBackPred...Gravatar wuestholz2013-12-09
* Fixed build failures due to changes in Boogie.Gravatar wuestholz2013-11-23
* Fixed typo in build scriptGravatar Rustan Leino2013-08-06
* MergeGravatar Rustan Leino2013-08-06
|\
| * Updated 'PrepareDafnyZip.bat'.Gravatar wuestholz2013-08-05
* | Unified function/method context heightsGravatar Rustan Leino2013-08-04
|/
* Changed the encoding of recursive functions. Previous, three hardcoded layer...Gravatar Rustan Leino2013-08-02
* Axioms that relate (multi)set cardinality with (multi)set difference.Gravatar Rustan Leino2013-07-16
* Computations!Gravatar Unknown2013-07-04
* Changed ranking function for Seq, so that it's compatible with data types.Gravatar Unknown2013-06-26
* Beefed up axioms about cardinality and the empty (multi)set, which fixes Issu...Gravatar Rustan Leino2013-06-20
* Removed the set cardinality/subset axiom (with no trigger, it caused test sui...Gravatar Rustan Leino2013-04-02
* Updated cardinality axioms for sets.Gravatar Nadia Polikarpova2013-03-30
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ...Gravatar Rustan Leino2013-03-27
* First take on set, multiset and map cardinality.Gravatar Nadia Polikarpova2013-03-22
* Bumped version to 1.6.1, to be released as a binary and on rise4fun.Gravatar Rustan Leino2013-03-10
* Disallow allocations in ghost contextsGravatar Rustan Leino2013-03-06
* Encode codatatype equalities by predefined copredicates, including their pref...Gravatar Rustan Leino2013-01-15
* Include BVD in build (to copy it into the Dafny\Binaries directory)Gravatar Unknown2012-10-30
* Test cases for co-inductive proofs, and an axiom that makes some of them poss...Gravatar Rustan Leino2012-10-19
* Added some axioms to try to recover boxed data. In particular, any element '...Gravatar Unknown2012-10-17
* Change the encoding of proof certificates to make the two levels explicitGravatar Unknown2012-10-12
* New feature:Gravatar Rustan Leino2012-10-11
* Fixed some build/migration issuesGravatar Rustan Leino2012-10-04
* Dafny: fixed mergeGravatar Rustan Leino2012-10-04
* MergeGravatar Rustan Leino2012-10-04
|\
* | Dafny: complete implementation of iteratorsGravatar Rustan Leino2012-10-03
* | Dafny: more part of verifying iteratorsGravatar Rustan Leino2012-10-03
* | Dafny: incomplete snapshot of verification of iteratorsGravatar Rustan Leino2012-10-02
| * Dafny: removed div/mod axioms, since Boogie now interprets div/modGravatar Unknown2012-09-28
| * Boogie: new syntax for integer division and modulus: use div and mod instead ...Gravatar boehmes2012-09-27
|/
* Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ...Gravatar Unknown2012-09-12
* Dafny: Implemented abstract modulesGravatar Jason Koenig2012-06-26
* Dafny: beefed up allocation axioms for boxes stored in fieldsGravatar Unknown2012-06-12
* Dafny: Added map comprehensions and updated display syntaxGravatar Unknown2012-05-31
* Dafny: added finite mapsGravatar Unknown2012-05-25
* Dafny: fully qualify (with module names) names of types in the translation in...Gravatar Rustan Leino2012-01-05
* Dafny: moved definition of class.array into prelude, anticipating writing axi...Gravatar Rustan Leino2011-11-09
* Dafny: removed support for assigning to an array-range (that is, an assignmen...Gravatar Rustan Leino2011-10-26
* Fixed axiom for Take/Update commuting.Gravatar Jason Koenig2011-07-19
* Strengthened axioms for multisets and sequences.Gravatar Jason Koenig2011-07-14
* Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi...Gravatar Jason Koenig2011-07-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 17:42:12 +0000