summaryrefslogtreecommitdiff
path: root/Test/dafny0/runtest.bat
Commit message (Expand)AuthorAge
* Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codepl...Gravatar Rustan Leino2013-03-05
* 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
* Dafny: allow class names to be used when referring to static functions (and, ...Gravatar Rustan Leino2011-05-21
* Dafny: let verifier, not the resolver, check for missing cases in match expre...Gravatar Rustan Leino2011-05-19
* Dafny: added set comprehension expressionsGravatar Rustan Leino2011-05-18
* Dafny: forbid "decreases *" on ghost loopsGravatar Rustan Leino2011-05-12
* Dafny: added type "nat"Gravatar Rustan Leino2011-04-19
* Dafny: Allow field selections and array-element selection as LHSs of assignme...Gravatar Unknown2011-04-05
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
* Dafny:Gravatar rustanleino2011-02-17
* Dafny: allow self-calls in function postconditions--these simply refer to the...Gravatar rustanleino2011-02-03
* Dafny:Gravatar rustanleino2010-09-17
* Dafny: better error reporting on resolution of refinements. Replace assertion...Gravatar kyessenov2010-07-14
* Dafny: added Carrol Morgan's calculator regression test.Gravatar kyessenov2010-07-02
* Dafny: added a regression test for the refinement extension.Gravatar kyessenov2010-07-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 12:43:53 +0000