debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Removed the old test infrastructure.	wuestholz	2014-07-01
\|
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	Minor clean-up in a couple of test files.	Rustan Leino	2014-02-24
\|
*	Add support for the /verifySeparately flag in Boogie and change most tests ↵	wuestholz	2013-12-18
\| \| \| \|	to use it.
*	Deactivated VC splitting in the tests.	wuestholz	2013-07-05
\|
*	Changed ranking function for Seq, so that it's compatible with data types.	Unknown	2013-06-26
\|
*	Made Test/vstte2012/RingBuffer.dfy and Test/dafny1/ExtensibleArray.dfy more ↵	Rustan Leino	2013-04-22
\| \| \| \| \| \| \|	similar to RingBufferAuto.dfy and ExtensibleArrayAuto.dfy, respectively, so that the effect of {:autocontracts} is more easily seen.
*	The "choose" statement, hacky and specialized as it was, is now gone. Use ↵	Rustan Leino	2013-03-27
\| \| \| \|	the assign-such-that statement instead. For example: x :\| x in S;
*	Updated two test files.	Rustan Leino	2013-03-22
\|
*	Adjustments in the /vcsMaxKeepGoingSplits flag in the test suite	Rustan Leino	2013-03-09
\|
*	Renamed "parallel" statement to "forall" statement, and made the parentheses ↵	Rustan Leino	2013-03-06
\| \| \| \|	around the bound variables optional.
*	Frame expressions are now checked to be well formed.	Rustan Leino	2013-02-13
\| \| \| \|	(A nice consequence of this is that the method IsTotal is no longer needed.)
*	Fixed another specification bug in a test case.	Rustan Leino	2013-01-23
\|
*	Fixed bug in translation of method termination checks, and also fixed a ↵	Rustan Leino	2013-01-23
\| \| \| \|	(previously undetected) specification bug in the test suite.
*	Beefed up loop invariant to prove a functional postcondition in a test case.	Rustan Leino	2012-11-24
\|
*	Beautified a test program	Rustan Leino	2012-11-19
\|
*	renamed "abstract module" to "module facade"	Rustan Leino	2012-10-22
\| \| \| \|	renamed "ghost module" to "abstract module", adding a keyword "abstract"
*	Fixed some goof-ups in the test script edits	Rustan Leino	2012-10-04
\| \| \| \|	Changed the test output to make it easier to spot (in the console output) that everything passed with success or if there were any failures
*	Added Test/dafny3 and another test file for iterators (hey, you can even run ↵	Rustan Leino	2012-10-04
\| \| \| \| \| \|	Iter.dfy!) Fixed migration issues
*	Dafny: fixed merge	Rustan Leino	2012-10-04
\|
*	Dafny: removed allocated, changed semantics of fresh	Jason Koenig	2012-07-29
\| \| \| \| \|	-allocated(x) removed, as really only useful in old(...) -old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).
*	Dafny: reinstated autocontracts	Jason Koenig	2012-07-02
\|
*	Dafny: fixed up test suite (temporarily removed autocontract tests)	Jason Koenig	2012-06-28
\|
*	Dafny: fixed some test cases	Jason Koenig	2012-06-28
\|
*	Dafny: Merge	Jason Koenig	2012-06-27
\|\
\| *	Undo bad merge.	afd	2012-06-27
\| \|
\| *	Merge	Unknown	2012-06-25
\| \|\
\| \| *	Dafny: Since it's no longer true that all types support equality at run-time ↵	Unknown	2012-06-21
\| \| \| \| \| \| \| \| \| \| \| \|	(in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.
\| * \|	Merge	Unknown	2012-06-21
\| \|\\|
\| \| *	Dafny: improved refinement features; added staged version of the proof of ↵	Unknown	2012-06-19
\| \|/ \|/\| \| \| \| \|	the Schorr-Waite algorithm (the staging features, as well as the newly added comments, make the verification much more digestible)
\| *	Merged with default.	chmaria	2012-06-18
\| \|\ \| \|/ \|/\|
* \|	Dafny: cleaned up test scripts a little	Unknown	2012-06-14
\| \|
\| *	Dafny: Added tests.	chmaria	2012-06-12
\|/
*	Dafny: fixed regression tests	Unknown	2012-05-29
\|
*	Dafny: Added maps to regression tests.	Unknown	2012-05-29
\|
*	Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic ↵	Unknown	2012-03-05
\| \| \| \|	specifications
*	Dafny: fixed bug in compilation of let expressions.	Rustan Leino	2012-01-26
\|
*	Dafny: allow definitions and uses of parameter-less predicates to go without ↵	Rustan Leino	2012-01-10
\| \| \| \|	parentheses
*	Merge	Rustan Leino	2011-11-22
\|\
\| *	Dafny: call C# compiler directly from inside Dafny, and optionally produce a ↵	Rustan Leino	2011-11-22
\| \| \| \| \| \| \| \|	.cs file with the new /spillTargetCode switch
* \|	Dafny: Added "type" declaration (syntax: "type X;"), which introduces an ↵	Rustan Leino	2011-11-21
\|/ \| \| \|	arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
*	Dafny: Cleaned up proof of RevConcat in test case	Rustan Leino	2011-11-08
\|
*	Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to ↵	Rustan Leino	2011-11-04
\| \| \| \|	a previous lemma
*	Added some Dafny and Boogie test cases, including Turing's factorial ↵	Rustan Leino	2011-11-03
\| \| \| \|	program, Hoare's classic FIND, and some induction tests for negative integers
*	Dafny induction:	Rustan Leino	2011-10-29
\| \| \| \| \| \| \|	* implemented induction tactic for result-less, non-mutating ghost methods * refine heuristics for determining if a variables is usefully passed to a recursive function * disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy) * added command-line flags /induction and /inductionHeuristic (everything is on by default)
*	Dafny: continued translation of "parallel" statements (Assign and Proof ↵	Rustan Leino	2011-10-24
\| \| \| \| \| \| \|	forms are mostly there, Call is missing and so is compilation) Dafny: included some test cases for the "parallel" statement Dafny: starting changing old "foreach" statements to the new "parallel" statement
*	Dafny: added translation of Assign case of the parallel statement	Rustan Leino	2011-10-22
\| \| \| \|	Dafny: discovered and fixed bug in no-overlap check of multi-dimensional array update, and changed previously incorrect MatrixFun.dfy test case (the new version is also a more efficient program)
*	Dafny: beautification in one test case, and fixed an Answer file	Rustan Leino	2011-09-29
\|
*	Dafny: added Flatten example to test suite	Rustan Leino	2011-09-11
\|
*	Dafny: updated Answer file from recent test additions	Rustan Leino	2011-08-22
\|