debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Fix some tests by locally disabling auto triggers	Clément Pit--Claudel	2015-08-28
\|
*	Renamed "ghost method" to "lemma" in a couple of test files	Rustan Leino	2015-07-24
\|
*	Stop pretty-print from emitting deprecated semi-colons.	qunyanm	2015-03-05
\|
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	Updated two test files.	Rustan Leino	2013-03-22
\|
*	Dafny: fixed regression tests	Unknown	2012-05-29
\|
*	Dafny: fixed bug in compilation of let expressions.	Rustan Leino	2012-01-26
\|
*	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
*	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: updated test files (will soon update Answer files as well)	Rustan Leino	2011-08-22
\|
*	Dafny: added reverse*reverse=id example to test suite	Rustan Leino	2011-08-04
\|
*	Dafny: re-ran parser generator to include semicolon-less body-less ↵	Rustan Leino	2011-07-26
\| \| \| \|	functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)
*	Merge	Rustan Leino	2011-07-21
\|\
* \|	Dafny: call previous lemma instead of restating it	Rustan Leino	2011-07-21
\| \|
\| *	Fixed regression test failures due to removal of bodiless methods and functions.	Jason Koenig	2011-07-15
\|/
*	Dafny: allow constructors only inside classes, removed semi-colons at end of ↵	Rustan Leino	2011-07-11
\| \| \| \|	body-less functions/methods
*	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-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: added manual proofs for 5 theorems in Rippling.dfy	Rustan Leino	2011-04-12
\|
*	Dafny: Fixed typo in P16 of Rippling benchmarks, which now makes it (true ↵	rustanleino	2011-03-07
\| \| \| \|	and) verifiable
*	Dafny:	rustanleino	2011-03-06
	* Support for induction over more than 1 variable * Added many of the Rippling induction benchmarks * Fixed bug in case handling