summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Expand)AuthorAge
* 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
* Multiset forming operators added.Gravatar Jason Koenig2011-07-11
* Partial implementation of multisets.Gravatar Jason Koenig2011-07-11
* Dafny: Dafny now uses the Euclidean definition of division. (Verifier and run...Gravatar Jason Koenig2011-07-08
* Dafny: Fixed axioms for Seq#Contains vs. the sequence building functionsGravatar Rustan Leino2011-06-29
* Dafny: fixed soundness problem with HeapSucc axiomGravatar Rustan Leino2011-06-01
* Dafny: To help verifications involving sequences of (boxed) booleans along, a...Gravatar Rustan Leino2011-05-16
* Dafny: added "choose" operator on setsGravatar rustanleino2011-03-26
* Dafny:Gravatar rustanleino2011-02-17
* Dafny: replaced the user-defined $ite function with Boogie's built-in if-then...Gravatar rustanleino2011-02-03
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
* Dafny: a partial first crack at a Dafny model-viewer provider, including capt...Gravatar rustanleino2010-11-01
* Dafny:Gravatar rustanleino2010-09-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 03:16:37 +0000