summaryrefslogtreecommitdiff
path: root/Test/dafny3
Commit message (Expand)AuthorAge
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
* MergeGravatar Clément Pit--Claudel2015-09-02
|\
* | Implement workarounds for some tests that fail with /autoTriggers.Gravatar Clément Pit--Claudel2015-08-28
* | Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
| * Fixed spelling mistake in test fileGravatar Rustan Leino2015-08-28
|/
* Changed dafny3/Filter.dfy to use higher-order functions instead of the previo...Gravatar leino2015-08-12
* Change the induction heuristic for lemmas to also look in precondition for cl...Gravatar leino2015-08-12
* Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ...Gravatar Rustan Leino2015-07-28
* Fix encoding in Dijkstra.pyGravatar Clément Pit--Claudel2015-07-20
* Reflect cleaner syntax in some test programsGravatar leino2015-03-31
* This changeset changes the default visibility of a function/predicate body ou...Gravatar leino2015-03-09
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* Rewrote two tests to make triggering better (while waiting for better automat...Gravatar Rustan Leino2014-08-12
* Another variation of GenericSort, this time instantiating with "int"Gravatar Rustan Leino2014-07-14
* Tidy up two files in test suiteGravatar Dan Rosen2014-07-07
* MergeGravatar Dan Rosén2014-07-07
|\
* | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| * Removed the old test infrastructure.Gravatar wuestholz2014-07-01
|/
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Improvements in sequence axioms to make checking more automatic.Gravatar Rustan Leino2014-04-02
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -...Gravatar Rustan Leino2014-02-23
* Add pretty-printing flag to the dafny3 test script.Gravatar wuestholz2013-12-19
* Added test3/GenericSort.dfy, which shows how modules can be used to write and...Gravatar Rustan Leino2013-12-18
* Added missing file (sorry)Gravatar Rustan Leino2013-12-18
* Add support for the /verifySeparately flag in Boogie and change most tests to...Gravatar wuestholz2013-12-18
* Don't inline opaque functions.Gravatar Rustan Leino2013-12-17
* Added some test cases: theorem about infinite and finite trees.Gravatar Rustan Leino2013-07-27
* Syntactic improvements in two tests.Gravatar Rustan Leino2013-07-16
* Added some test cases having to do with finite/infinite treesGravatar Rustan Leino2013-07-10
* Fixed soundness bug with co-recursive calls: co-recursive calls may now no l...Gravatar Rustan Leino2013-06-29
* Updated two test files.Gravatar Rustan Leino2013-03-22
* Finished support for ==# in calc, changed Paulson example to use it.Gravatar Nadia Polikarpova2013-03-20
* Added a coinductive/inductive Filter example to the test suiteGravatar Rustan Leino2013-03-18
* Added several co-induction examples from a 1996 paper by Larry Paulson.Gravatar Rustan Leino2013-03-15
* Renamed "parallel" statement to "forall" statement, and made the parentheses ...Gravatar Rustan Leino2013-03-06
* Changed calc syntax (custom operators are now written before the hint)Gravatar Nadia Polikarpova2013-02-08
* Added some test cases that show exmaples that iterate over set elements.Gravatar Rustan Leino2013-02-02
* Examples from co-induction paperGravatar Rustan Leino2013-01-22
* More automatic co-induction for comethodsGravatar Rustan Leino2013-01-20
* Added some co- test cases. Fixed some bugs.Gravatar Rustan Leino2013-01-20
* Removed the syntactic form copredicate #-form with the implicit argument.Gravatar Rustan Leino2013-01-16
* renamed "abstract module" to "module facade"Gravatar Rustan Leino2012-10-22
* allow a refinement to introduce "return" statements, at the price of re-verif...Gravatar Rustan Leino2012-10-22
* added some calculational proofs from Dijkstra's writingsGravatar Rustan Leino2012-10-21
* Test cases for co-inductive proofs, and an axiom that makes some of them poss...Gravatar Rustan Leino2012-10-19
* Support default (which, here, means nameless) class-instance constructorsGravatar Rustan Leino2012-10-05
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 02:30:40 +0000