debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires	qunyanm	2016-03-28
\| \| \| \| \|	it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run.
*	Stop pretty-print from emitting deprecated semi-colons.	qunyanm	2015-03-05
\|
*	Language change: All functions and methods declared lexically outside any ↵	leino	2014-12-12
\| \| \| \| \| \| \| \| \| \|	class are now automatically static, and fields are no longer allowed to be declared there. Stated differently, all heap state must now be declared inside an explicitly declared class, and functions and methods declared outside any class can be viewed as belonging to the module. The motivating benefit of this change is to no longer need the 'static' keyword when declaring a module of functions and methods.
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	Dafny: permanently changed the syntax of "datatype" declarations to what ↵	Rustan Leino	2011-05-27
\| \| \| \|	previously was an alternative syntax
*	Dafny:	Rustan Leino	2011-05-26
\| \| \| \| \| \|	* fixed ghost/non-ghost story for breaks and returns * changed compilation/translation to always use goto's to implement Dafny's breaks * introduced "break break" statements
*	Dafny: retired the "call" keyword	Rustan Leino	2011-05-26
\|
*	Dafny:	Rustan Leino	2011-05-21
\| \| \| \| \| \| \| \| \| \|	* started rewriting parsing of qualified identifiers in expressions * annoyingly, had to introduce AST nodes for concrete syntax * previous syntax for invoking datatype constructors: #List.Cons(h, t) new syntax: List.Cons(h, t) or, if only one datatype has a constructor named Cons: Cons(h, t) * Removed type parameters for datatype constructors from the grammar * Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)
*	Dafny: every decreases clause implicitly ends with a never-ending sequence ↵	rustanleino	2011-02-03
\| \| \| \|	of TOP elements; this reduces the need for manually supplied decreases clauses (see the Outer/Inner example in Test/dafny0/Termination.dfy and the Substitute/SubstSeq example in Test/dafny1/Substitution.dfy).
*	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: Added two additional heuristics for guessing missing loop decreases ↵	rustanleino	2010-06-11
\| \| \| \|	clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
*	Boogie:	rustanleino	2010-06-08
	* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it). * Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it). Dafny: * Split off some tests from Test/dafny0 into Test/dafny1. * Added Test/dafny1/UltraFilter.dfy.