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.
*	Fix bug in translation of 'new' for arrays	Rustan Leino	2014-10-29
\|
*	Improved axiom that knows that array-to-sequence converstion depends only on ↵	Rustan Leino	2014-06-04
\| \| \| \|	those heap location that hold the array elements
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-29
\|
*	Added axiom to transfer array element-type information onto the elements ↵	Rustan Leino	2014-03-20
\| \| \| \| \| \|	themselves. Other serendipitous axiom improvements.
*	Fixed problem with propagating allocation information about array elements.	Rustan Leino	2014-03-20
\| \| \| \|	Improved situation with (reducing bogosity of) type checking of "object".
*	Dafny: Added "type" declaration (syntax: "type X;"), which introduces an ↵	Rustan Leino	2011-11-21
\| \| \| \|	arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
*	Dafny: fixed bug in reads checking of array-to-sequence conversions	Rustan Leino	2011-11-08
\|
*	Dafny: fixed bug in translator when LHS of a call was an array element or a nat	Rustan Leino	2011-09-30
\|
*	Dafny: fixed bug in looking at the arguments of the :induction attribute	Rustan Leino	2011-08-18
\|
*	Fixed failing regression tests.	Jason Koenig	2011-07-14
\|
*	Added multiset from sequence axioms, removed array range RHSs. Fixed issue ↵	Jason Koenig	2011-07-13
\| \| \| \|	with duplicate array.Length functions in generated Boogie file.
*	Added s[..] syntax in anticipation of sequence forming operation. (also ↵	Jason Koenig	2011-07-11
\| \| \| \|	updated regression tests.)
*	Dafny: Allow field selections and array-element selection as LHSs of ↵	Unknown	2011-04-05
\| \| \| \|	assignments where RHS is not just an expression
*	Dafny:	rustanleino	2010-09-17
\| \| \| \| \| \|	* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation) * Changed syntax of array length from \|a\| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays. * Internally, this meant adding support for built-in classes and readonly fields
*	Dafny:	rustanleino	2010-05-21
	* Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks