debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	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.
*	New logical encoding of types with Is and IsAlloc	Dan Rosén	2014-07-07
\|
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	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;
*	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.
*	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)
*	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: don't require parentheses in syntax of "choose" statements	Rustan Leino	2011-04-05
\|
*	Dafny: added "choose" operator on sets	rustanleino	2011-03-26
\|
*	Dafny: improved and corrected physical/ghost distinction	rustanleino	2011-03-26
\|
*	Dafny: Fix type bug in SplitExpr translation.	rustanleino	2010-06-08
\|
*	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.