| Commit message (Expand) | Author | Age |
* | Fixed typo in build script | Rustan Leino | 2013-08-06 |
* | Merge | Rustan Leino | 2013-08-06 |
|\ |
|
| * | Updated 'PrepareDafnyZip.bat'. | wuestholz | 2013-08-05 |
* | | Unified function/method context heights | Rustan Leino | 2013-08-04 |
|/ |
|
* | Changed the encoding of recursive functions. Previous, three hardcoded layer... | Rustan Leino | 2013-08-02 |
* | Axioms that relate (multi)set cardinality with (multi)set difference. | Rustan Leino | 2013-07-16 |
* | Computations! | Unknown | 2013-07-04 |
* | Changed ranking function for Seq, so that it's compatible with data types. | Unknown | 2013-06-26 |
* | Beefed up axioms about cardinality and the empty (multi)set, which fixes Issu... | Rustan Leino | 2013-06-20 |
* | Removed the set cardinality/subset axiom (with no trigger, it caused test sui... | Rustan Leino | 2013-04-02 |
* | Updated cardinality axioms for sets. | Nadia Polikarpova | 2013-03-30 |
* | The "choose" statement, hacky and specialized as it was, is now gone. Use th... | Rustan Leino | 2013-03-27 |
* | Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ... | Rustan Leino | 2013-03-27 |
* | First take on set, multiset and map cardinality. | Nadia Polikarpova | 2013-03-22 |
* | Bumped version to 1.6.1, to be released as a binary and on rise4fun. | Rustan Leino | 2013-03-10 |
* | Disallow allocations in ghost contexts | Rustan Leino | 2013-03-06 |
* | Encode codatatype equalities by predefined copredicates, including their pref... | Rustan Leino | 2013-01-15 |
* | Include BVD in build (to copy it into the Dafny\Binaries directory) | Unknown | 2012-10-30 |
* | Test cases for co-inductive proofs, and an axiom that makes some of them poss... | Rustan Leino | 2012-10-19 |
* | Added some axioms to try to recover boxed data. In particular, any element '... | Unknown | 2012-10-17 |
* | Change the encoding of proof certificates to make the two levels explicit | Unknown | 2012-10-12 |
* | New feature: | Rustan Leino | 2012-10-11 |
* | Fixed some build/migration issues | Rustan Leino | 2012-10-04 |
* | Dafny: fixed merge | Rustan Leino | 2012-10-04 |
* | Merge | Rustan Leino | 2012-10-04 |
|\ |
|
* | | Dafny: complete implementation of iterators | Rustan Leino | 2012-10-03 |
* | | Dafny: more part of verifying iterators | Rustan Leino | 2012-10-03 |
* | | Dafny: incomplete snapshot of verification of iterators | Rustan Leino | 2012-10-02 |
| * | Dafny: removed div/mod axioms, since Boogie now interprets div/mod | Unknown | 2012-09-28 |
| * | Boogie: new syntax for integer division and modulus: use div and mod instead ... | boehmes | 2012-09-27 |
|/ |
|
* | Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ... | Unknown | 2012-09-12 |
* | Dafny: Implemented abstract modules | Jason Koenig | 2012-06-26 |
* | Dafny: beefed up allocation axioms for boxes stored in fields | Unknown | 2012-06-12 |
* | Dafny: Added map comprehensions and updated display syntax | Unknown | 2012-05-31 |
* | Dafny: added finite maps | Unknown | 2012-05-25 |
* | Dafny: fully qualify (with module names) names of types in the translation in... | Rustan Leino | 2012-01-05 |
* | Dafny: moved definition of class.array into prelude, anticipating writing axi... | Rustan Leino | 2011-11-09 |
* | Dafny: removed support for assigning to an array-range (that is, an assignmen... | Rustan Leino | 2011-10-26 |
* | Fixed axiom for Take/Update commuting. | Jason Koenig | 2011-07-19 |
* | Strengthened axioms for multisets and sequences. | Jason Koenig | 2011-07-14 |
* | Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi... | Jason Koenig | 2011-07-13 |
* | Multiset forming operators added. | Jason Koenig | 2011-07-11 |
* | Partial implementation of multisets. | Jason Koenig | 2011-07-11 |
* | Dafny: Dafny now uses the Euclidean definition of division. (Verifier and run... | Jason Koenig | 2011-07-08 |
* | Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions | Rustan Leino | 2011-06-29 |
* | Dafny: fixed soundness problem with HeapSucc axiom | Rustan Leino | 2011-06-01 |
* | Dafny: To help verifications involving sequences of (boxed) booleans along, a... | Rustan Leino | 2011-05-16 |
* | Dafny: added "choose" operator on sets | rustanleino | 2011-03-26 |
* | Dafny: | rustanleino | 2011-02-17 |
* | Dafny: replaced the user-defined $ite function with Boogie's built-in if-then... | rustanleino | 2011-02-03 |