summaryrefslogtreecommitdiff
path: root/Binaries/DafnyPrelude.bpl
Commit message (Expand)AuthorAge
* Various DafnyPrelude.bpl cleanup.Gravatar leino2014-11-01
* Improved power of axioms Seq#FromArrayGravatar leino2014-10-31
* Add an option to use reduce Z3's knowledge of non-linear arithmetic.Gravatar Bryan Parno2014-10-24
* Comparisons and well-founded order of charGravatar leino2014-10-21
* Added types "char" and "string" (the latter being a synonym for "seq<char>").Gravatar leino2014-10-20
* Fixed bugs in previous check-inGravatar leino2014-08-25
* Added .Trunc field to real-based typesGravatar leino2014-08-21
* Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
* MergeGravatar Dan Rosén2014-07-07
|\
* | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| * Added some axioms about seq-to-multiset conversionsGravatar Rustan Leino2014-06-24
| * Specialized Lit function for int and real (leaving all other cases polymorphi...Gravatar Rustan Leino2014-06-10
| * Improved axiom that knows that array-to-sequence converstion depends only on ...Gravatar Rustan Leino2014-06-04
|/
* Improvements in sequence axioms to make checking more automatic.Gravatar Rustan Leino2014-04-02
* Added axiom to transfer array element-type information onto the elements them...Gravatar Rustan Leino2014-03-20
* Fixed problem with propagating allocation information about array elements.Gravatar Rustan Leino2014-03-20
* Removed an apparently unneeded trigger.Gravatar Rustan Leino2014-03-06
* 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
* 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
* 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
* First take on set, multiset and map cardinality.Gravatar Nadia Polikarpova2013-03-22
* Disallow allocations in ghost contextsGravatar Rustan Leino2013-03-06
* Encode codatatype equalities by predefined copredicates, including their pref...Gravatar Rustan Leino2013-01-15
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 03:14:06 +0000