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
\|
*	Cleaned up some no longer needed parentheses in test file	Rustan Leino	2014-04-15
\|
*	Add support for the /verifySeparately flag in Boogie and change most tests ↵	wuestholz	2013-12-18
\| \| \| \|	to use it.
*	Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ↵	Rustan Leino	2013-04-01
\| \| \| \| \| \| \|	where more type information is known Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement. Fixed numerous places where some recursive checks did not reach.
*	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: Updated a test that would take a long time (almost 2h) to verify with ↵	wuestholz	2012-09-18
\| \| \| \|	Z3 4.1.
*	Dafny: cleaned up test scripts a little	Unknown	2012-06-14
\|
*	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: retired the "call" keyword	Rustan Leino	2011-05-26
\|
*	Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵	Rustan Leino	2011-05-11
\| \| \| \|	avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
*	Dafny: Allow field selections and array-element selection as LHSs of ↵	Unknown	2011-04-05
\| \| \| \|	assignments where RHS is not just an expression
*	Dafny: Added support for an initializing call as part of the new-allocation ↵	rustanleino	2011-03-27
\| \| \| \| \| \| \| \| \| \| \|	syntax. What you previously would have written like: c := new C; call c.Init(x, y); you can now write as: c := new C.Init(x, y);
*	Dafny: compile quantifiers	rustanleino	2011-03-26
\| \| \| \| \| \|	Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges
*	Dafny: Fixed error in printing an error message. Changed "function method" ↵	rustanleino	2011-01-11
\| \| \| \|	to "function" in a test case.
*	Dafny: Improved default decreases clauses for methods and functions	rustanleino	2010-11-25
\| \| \| \| \|	Dafny: Don't display "alloc" field in BVD Chalice: Fixed error-message parsing error in VS mode
*	Dafny: Updated VSComp2010/Answer to correspond to recently updated test file	rustanleino	2010-11-21
\|
*	Chalice: white space delta in test file	rustanleino	2010-11-17
\| \| \| \|	Dafny: Simplified VSComp2010/Problem4-Queens.dfy from using an inductive ghost-method lemmas to just using an assert
*	Dafny:	rustanleino	2010-09-17
\| \| \| \| \| \|	* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation) * Changed syntax of array length from \|a\| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays. * Internally, this meant adding support for built-in classes and readonly fields
*	Dafny: Added Dafny solutions to the VSComp 2010 problems	rustanleino	2010-09-01