index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
/
dafny3
Commit message (
Expand
)
Author
Age
*
Removed the old test infrastructure.
wuestholz
2014-07-01
*
Set up the same test infrastructure as in Boogie.
wuestholz
2014-05-29
*
Improvements in sequence axioms to make checking more automatic.
Rustan Leino
2014-04-02
*
Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -...
Rustan Leino
2014-02-23
*
Add pretty-printing flag to the dafny3 test script.
wuestholz
2013-12-19
*
Added test3/GenericSort.dfy, which shows how modules can be used to write and...
Rustan Leino
2013-12-18
*
Added missing file (sorry)
Rustan Leino
2013-12-18
*
Add support for the /verifySeparately flag in Boogie and change most tests to...
wuestholz
2013-12-18
*
Don't inline opaque functions.
Rustan Leino
2013-12-17
*
Added some test cases: theorem about infinite and finite trees.
Rustan Leino
2013-07-27
*
Syntactic improvements in two tests.
Rustan Leino
2013-07-16
*
Added some test cases having to do with finite/infinite trees
Rustan Leino
2013-07-10
*
Fixed soundness bug with co-recursive calls: co-recursive calls may now no l...
Rustan Leino
2013-06-29
*
Updated two test files.
Rustan Leino
2013-03-22
*
Finished support for ==# in calc, changed Paulson example to use it.
Nadia Polikarpova
2013-03-20
*
Added a coinductive/inductive Filter example to the test suite
Rustan Leino
2013-03-18
*
Added several co-induction examples from a 1996 paper by Larry Paulson.
Rustan Leino
2013-03-15
*
Renamed "parallel" statement to "forall" statement, and made the parentheses ...
Rustan Leino
2013-03-06
*
Changed calc syntax (custom operators are now written before the hint)
Nadia Polikarpova
2013-02-08
*
Added some test cases that show exmaples that iterate over set elements.
Rustan Leino
2013-02-02
*
Examples from co-induction paper
Rustan Leino
2013-01-22
*
More automatic co-induction for comethods
Rustan Leino
2013-01-20
*
Added some co- test cases. Fixed some bugs.
Rustan Leino
2013-01-20
*
Removed the syntactic form copredicate #-form with the implicit argument.
Rustan Leino
2013-01-16
*
renamed "abstract module" to "module facade"
Rustan Leino
2012-10-22
*
allow a refinement to introduce "return" statements, at the price of re-verif...
Rustan Leino
2012-10-22
*
added some calculational proofs from Dijkstra's writings
Rustan Leino
2012-10-21
*
Test cases for co-inductive proofs, and an axiom that makes some of them poss...
Rustan Leino
2012-10-19
*
Support default (which, here, means nameless) class-instance constructors
Rustan Leino
2012-10-05
*
Fixed some goof-ups in the test script edits
Rustan Leino
2012-10-04
*
Added Test/dafny3 and another test file for iterators (hey, you can even run ...
Rustan Leino
2012-10-04