debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Implement workarounds for some tests that fail with /autoTriggers.	Clément Pit--Claudel	2015-08-28
\| \| \| \| \| \|	The issues here are mostly with induction (wrt. to trigger selection and quantifier splitting) and with expressions like P(i, j-1) where no good choices are available.
*	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
\|
*	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)
*	Merge	Rustan Leino	2011-05-27
\|\
\| *	Dafny: permanently changed the syntax of "datatype" declarations to what ↵	Rustan Leino	2011-05-27
\| \| \| \| \| \| \| \|	previously was an alternative syntax
* \|	Dafny: fixed bug in induction-tactic heuristic (should never pick values ↵	Rustan Leino	2011-05-26
\| \| \| \| \| \| \| \|	whose type is a type parameter)
\| *	Dafny: retired the "call" keyword	Rustan Leino	2011-05-26
\| \|
\| *	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: Alternative (and candidate replacement) syntax for declaring datatypes	Rustan Leino	2011-04-20
\| \| \| \|	Dafny: Additional induction test cases
*	Dafny: fixed bug in induction over integers	Unknown	2011-04-04
\| \| \| \|	Dafny: added pow2 example
*	Dafny: compile quantifiers	rustanleino	2011-03-26
\| \| \| \| \| \|	Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges
*	Dafny: Added heuristic for when to turn on the induction tactic	rustanleino	2011-03-05
\|
*	Dafny:	rustanleino	2011-03-04
	* Add support for an {:induction} attribute on universal quantifiers over one bound variable. It causes the universally quantified formulas to be proved by induction. * For a user-defined function F, introduce not just F and F#limited, but also F#2 (which sits "above" F, just as F sits "above" F#limited) * In base case of SplitExpr, make use of F#2 functions (unless already inside an inlined predicate)