debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Changed computation of ghosts until pass 2 of resolution.	leino	2015-09-28
\| \| \| \| \| \| \|	Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions.
*	Preliminary refactoring of ghost-statement computations to after type checking	leino	2015-09-20
\|
*	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;
*	Disallow allocations in ghost contexts	Rustan Leino	2013-03-06
\|
*	Renamed "parallel" statement to "forall" statement, and made the parentheses ↵	Rustan Leino	2013-03-06
\| \| \| \|	around the bound variables optional.
*	Dafny: Changed the semantics of the assign-such-that statement "x :\| P;" to ↵	Unknown	2012-06-13
\| \| \| \|	check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
*	Dafny: fixed lack of assign-such-that restriction in parallel statement	Unknown	2012-03-15
\|
*	Dafny: parallel statements:	Rustan Leino	2012-01-17
\| \| \| \| \| \| \|	- removed the awkward restriction that method postconditions cannot use old/fresh if there's no modifies clause and no out-parameters; instead, implemented parallel statements to handle these cases - also allow old/fresh in ensures clauses of parallel statements - allow TypeRhs and choose expressions in Call/Proof parallel statements - disallow calls to non-ghost methods in parallel statements (since those may do "print" statements and we don't want to allow those to take place in parallel; besides, the compiler wants to omit the parallel statement altogether and could not do so if there were print statements)
*	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: implemented compilation of parallel statements	Rustan Leino	2011-10-25
	Dafny: beefed up resolution of parallel statements