summaryrefslogtreecommitdiff
path: root/Test/dafny1/TerminationDemos.dfy
Commit message (Collapse)AuthorAge
* Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
|
* Dafny: added some test cases that use natGravatar Rustan Leino2011-05-16
|
* Dafny: implemented a more precise scheme for allowing use of a function's ↵Gravatar rustanleino2011-02-03
| | | | rep axiom
* Dafny: added ensures clauses to functionsGravatar rustanleino2011-02-02
|
* Dafny: Improved default decreases clauses for methods and functionsGravatar rustanleino2010-11-25
| | | | | Dafny: Don't display "alloc" field in BVD Chalice: Fixed error-message parsing error in VS mode
* Boogie:Gravatar rustanleino2010-06-08
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it). * Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it). Dafny: * Split off some tests from Test/dafny0 into Test/dafny1. * Added Test/dafny1/UltraFilter.dfy.