debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Changed logical order of requires and reads clauses on functions. Reads clauses	Rustan Leino	2015-06-15
\| \| \| \| \|	can now assume the precondition (as had also been the case back in the days when reads clauses had to be self framing).
*	Do postponsed reads checking also for the body of functions -- see ↵	Rustan Leino	2015-06-15
\| \| \| \| \| \|	Test/dafny0/Reads.dfy for benefits. (Unfortunately, this loses track of the "postcondition might not hold on this return path" locations, see Test/dafny0/FunctionSpecifications.dfy.)
*	Some more reads tests	Rustan Leino	2015-06-15
\|
*	More reads tests	Rustan Leino	2015-06-15
\|
*	Postpone reads checks of function preconditions until after the entire ↵	leino	2015-06-15
\| \| \| \|	precondition has otherwise been checked for well-formedness
*	More tests of reads-clause checking	Rustan Leino	2015-06-15
\|
*	Combined some common routines into CheckWellformedAndAssume, which also ↵	leino	2015-06-12
\| \| \| \|	allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)
*	Add higher-order-functions and some other goodies	Dan Rosén	2014-08-11
	* The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter