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.
*	Type parameters in method/function signatures are no longer auto-declared. ↵	Rustan Leino	2015-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \|	Although convenient and concise, the auto-declare behavior has on many occasions caused confusion when a type name has accidentally been mistyped (and Dafny had then accepted and auto-declared the name). Note, the behavior of filling in missing type parameters is still supported. This mode, although unusual (even original?) in languages, is different from the auto- declare behavior. For auto-declare, identifiers could be used in the program without having a declaration. For fill-in parameters, the implicitly declared type parameters remain anonymous.
*	Assume type properties of values that are created by a havoc assignment. ↵	Rustan Leino	2015-01-27
\| \| \| \| \| \|	Such assignments are part of assign-such-that statements, and thus this also fixes Issue 52.
*	Allow underscores in numeric literals (and in field/destructor names that ↵	leino	2014-10-23
\| \| \| \| \| \|	are written as numeric strings). The underscores have no semantic meaning, but can help a human parse the numbers.
*	Changed variable names in test case	leino	2014-10-13
\|
*	Some more test cases for associativity and short-circuitness of <==	leino	2014-10-13
\|
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	Pass assert/assume attributes down to Boogie	Rustan Leino	2013-12-16
\|
*	Add support for hexidecimal numbers.	parno	2013-07-30
\|
*	Axioms that relate (multi)set cardinality with (multi)set difference.	Rustan Leino	2013-07-16
\| \| \| \|	Removed three redundant multiset axioms.
*	Beefed up axioms about cardinality and the empty (multi)set, which fixes ↵	Rustan Leino	2013-06-20
\| \| \| \| \| \|	Issue 17 on dafny.codeplex.com. Added information that allows multiset members to be unboxed as needed (mimicking what was already done for sets).
*	Fixed some omitted cases in Substitute (and added "assume false" to catch ↵	Rustan Leino	2013-05-21
\| \| \| \|	any other, later)
*	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.
*	Added a test case for <==.	Nadia Polikarpova	2013-03-14
\|
*	Merge	Jason Koenig	2012-06-13
\|\
* \|	Dafny: allow parallel assignments to assign to the same LHS if the RHS match.	Jason Koenig	2012-06-13
\|/
*	Dafny: Added Euclidean regression test (Verifier only).	Jason Koenig	2011-07-08
\|
*	Dafny: translate call statements with fancy LHSs	Rustan Leino	2011-05-31
\|
*	Dafny: Translate general LHSs for var and := (not yet for call, no ↵	Rustan Leino	2011-05-30
\| \| \| \|	compilation yet)
*	Dafny:	Rustan Leino	2011-05-27
\| \| \| \| \|	* fixed bug in allowing ghost out-parameters of ghost methods * added test case for verifying calls of the form MyClass.M(...)
*	Dafny: added chaining operators	Rustan Leino	2011-05-27
\|
*	Dafny: retired the "call" keyword	Rustan Leino	2011-05-26
\|
*	Dafny: allow class names to be used when referring to static functions (and, ↵	Rustan Leino	2011-05-21
	soon, methods), and test cases for new name resolution rules