summaryrefslogtreecommitdiff
path: root/Test/dafny0/runtest.bat
Commit message (Expand)AuthorAge
* Added support for automatic generation of function requirements via the :auto...Gravatar Bryan Parno2014-01-08
* Fixed pretty printing of calc statements to use the new(-since-long) format.Gravatar Rustan Leino2013-12-17
* Add support for the "include" keyword, which accepts a (possibly relative) pathGravatar Bryan Parno2013-12-10
* Let compiler complain about body-less functions and methods, even if these ar...Gravatar Rustan Leino2013-11-14
* Set up call-graph to keep track of edges between functions and methods. (To ...Gravatar Rustan Leino2013-08-04
* Make functions and predicates be opaque outside the defining module -- only t...Gravatar Rustan Leino2013-07-29
* Computations!Gravatar Unknown2013-07-04
* Changed ranking function for Seq, so that it's compatible with data types.Gravatar Unknown2013-06-26
* Beefed up assign/let-such-that to generate possible witnesses for set/multise...Gravatar Rustan Leino2013-03-25
* Support for copredicates and prefix predicates in comethods.Gravatar Rustan Leino2012-12-04
* Parse prefix predicates/methodsGravatar Rustan Leino2012-11-24
* New feature:Gravatar Rustan Leino2012-10-11
* Fixed some goof-ups in the test script editsGravatar Rustan Leino2012-10-04
* Added Test/dafny3 and another test file for iterators (hey, you can even run ...Gravatar Rustan Leino2012-10-04
* MergeGravatar Rustan Leino2012-10-04
|\
* | Dafny: compile iteratorsGravatar Rustan Leino2012-09-26
* | Dafny: added test cases for resolving iteratorsGravatar Rustan Leino2012-09-25
| * Bugfix in the translation of calc statements (oops), added more resolution an...Gravatar Nadia Polikarpova2012-09-21
|/
* Dafny: improved checking of inherited postconditions (in refinements)Gravatar Unknown2012-09-10
* Dafny: allow 'decreases *' (that is, non-terminating recursion) on tail-recur...Gravatar Rustan Leino2012-09-09
* Dafny: support opening modules into the local scopeGravatar Jason Koenig2012-07-30
* Dafny: fixed bug in which old locals were not properly forbidden from being m...Gravatar Jason Koenig2012-07-12
* Dafny: More work on the coinduction principleGravatar Rustan Leino2012-07-09
* Dafny: equality-support test cases. This is just a snapshot--some things sti...Gravatar Unknown2012-06-22
* Dafny: cleaned up test scripts a littleGravatar Unknown2012-06-14
* Dafny: liberalized equality to work when the types could possibly be the sameGravatar Jason Koenig2012-06-13
* Dafny: Added maps to regression tests.Gravatar Unknown2012-05-29
* Dafny: added support for co-recursive callsGravatar Rustan Leino2012-05-01
* Dafny: fixed resolution bug for inductive datatypes (previous check did not h...Gravatar Unknown2012-04-25
* Dafny: allow more skeleton statements in refinementsGravatar Unknown2012-03-02
* Dafny: allow various forms of leaving off type arguments in declarationsGravatar Rustan Leino2012-02-16
* Dafny: Fixed a bug in the printing of let expressions.Gravatar wuestholz2012-01-24
* Dafny: added predicatesGravatar Rustan Leino2012-01-10
* Dafny: added support for simple superposition refinementsGravatar Rustan Leino2012-01-09
* Dafny: firmed up the module systemGravatar Rustan Leino2012-01-05
* Dafny: disengaged old refinement test filesGravatar Rustan Leino2012-01-04
* Dafny: Fixed a bug in the pretty printer.Gravatar wuestholz2011-12-26
* Dafny: Made sure that error locations refer to the Dafny program, even if the...Gravatar wuestholz2011-12-15
* Dafny: added let expressions (syntax: "var x := E0; E1")Gravatar Rustan Leino2011-11-14
* Dafny: added assert/assume expressionsGravatar Rustan Leino2011-11-09
* Dafny: implemented compilation of parallel statementsGravatar Rustan Leino2011-10-25
* Dafny: continued translation of "parallel" statements (Assign and Proof forms...Gravatar Rustan Leino2011-10-24
* Dafny: Fixed a bug in the printer that led to a stack overflow.Gravatar wuestholz2011-08-11
* Fixed regression test failures due to removal of bodiless methods and functions.Gravatar Jason Koenig2011-07-15
* Dafny: Fixed bug in call statements where mutability of out parameters was no...Gravatar Jason Koenig2011-07-06
* Dafny: Updated regression tests to include chaining disjoint operators.Gravatar Jason Koenig2011-07-05
* Added regression tests for new return statements with parameters.Gravatar Jason Koenig2011-06-29
* Added regression test for loop modifies clauses.Gravatar Jason Koenig2011-06-28
* Dafny: retired "use" statementsGravatar Rustan Leino2011-05-27
* Dafny: added chaining operatorsGravatar Rustan Leino2011-05-27
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-08 14:40:44 +0000