summaryrefslogtreecommitdiff
path: root/Test/dafny4/Answer
Commit message (Expand)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Support the transition from "modify Frame;" to "modify Frame { Body }" by ref...Gravatar Rustan Leino2014-04-04
* MergeGravatar Nada Amin2014-03-12
|\
* | Improve computations, in particular compositionality. Isolated useless litera...Gravatar Nada Amin2014-03-12
| * Added a test case from the ACL2 bookGravatar Rustan Leino2014-03-10
|/
* Moved the (long running) CloudMake test files to their own directoryGravatar Rustan Leino2014-02-28
* Added CloudMake formalization and proofs to the test suiteGravatar Rustan Leino2014-02-26
* Added examples mentioned in a paper on circular coinduction.Gravatar Rustan Leino2014-02-25
* New test file: dafny4/NumberRepresentations.dfyGravatar Rustan Leino2014-02-13
* Added to the test suite a Dafny version of Basics.v from the "Software Founda...Gravatar Rustan Leino2014-02-13
* Added examples from the Kozen and Silva paper "Practical Coinduction".Gravatar Rustan Leino2014-02-10
* Some simplifications to the proof of GHC MergeSort.Gravatar Rustan Leino2014-02-01
* Added an alternative statement of the prime theoremGravatar Rustan Leino2014-01-24
* Proof that there is no bound on the size of prime numbersGravatar Rustan Leino2014-01-11
* Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle...Gravatar Rustan Leino2014-01-08