debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
...
\| *	Implemented missing routine in runtime system (real-to-int conversion)	leino	2014-07-21
\|/
*	Merge	Dan Rosén	2014-07-07
\|\
* \|	New logical encoding of types with Is and IsAlloc	Dan Rosén	2014-07-07
\| \|
\| *	Added some axioms about seq-to-multiset conversions	Rustan Leino	2014-06-24
\| \|
\| *	Specialized Lit function for int and real (leaving all other cases ↵	Rustan Leino	2014-06-10
\| \| \| \| \| \| \| \| \| \| \| \|	polymorphic). This reduces the number of int<->U conversions that Boogie adds, which avoids a looping problem in Z3. (Regrettably, the test suite seems to have become rather unstable. Sometimes everything verifies and sometimes there is some looping forever.)
\| *	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
*	Compile reals	Rustan Leino	2014-04-13
\|
*	Improvements in sequence axioms to make checking more automatic.	Rustan Leino	2014-04-02
\| \| \| \|	Minor changes in a test file.
*	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".
*	Removed an apparently unneeded trigger.	Rustan Leino	2014-03-06
\|
*	Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for ↵	Rustan Leino	2014-02-13
\| \| \| \| \| \|	literals. Added axiom to better handle DtAlloc/GenericAlloc correspondence (which improves handling of computations).
*	Preliminary support for reals in Dafny specs. No compiler suport yet.	Bryan Parno	2014-02-10
\|
*	Merge	Rustan Leino	2014-01-08
\|\
* \|	Allow left-hand sides of a let expression to be patterns (like in the case ↵	Rustan Leino	2014-01-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	of a match expression). Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator. Fixed compilation of match expressions, to allow them anywhere.
\| *	Compile assign-such-that for all integers, not just ones where a bound is found	Rustan Leino	2014-01-06
\|/
*	Print and translate "match" expressions in general positions, not just at ↵	Rustan Leino	2014-01-03
\| \| \| \|	the top-level of function bodies. (Note, resolver also needs to allow this before the user can take advantage of this.)
*	Embellished axioms about GenericAlloc and DtAlloc.	Rustan Leino	2014-01-03
\|
*	Fix some things due to changes in Boogie (execution engine API, ↵	wuestholz	2013-12-09
\| \| \| \|	'UnivBackPred2.smt2' no longer needed).
*	Fixed build failures due to changes in Boogie.	wuestholz	2013-11-23
\|
*	Fixed typo in build script	Rustan Leino	2013-08-06
\|
*	Merge	Rustan Leino	2013-08-06
\|\
\| *	Updated 'PrepareDafnyZip.bat'.	wuestholz	2013-08-05
\| \|
* \|	Unified function/method context heights	Rustan Leino	2013-08-04
\|/
*	Changed the encoding of recursive functions. Previous, three hardcoded ↵	Rustan Leino	2013-08-02
\| \| \| \| \| \|	layers were used: F#2, F, and F#limited. Now, recursive functions take a layer argument, which is specified by Peano numbers. Also, cleaned up and made more consistent the emission of axioms regarding functions.
*	Axioms that relate (multi)set cardinality with (multi)set difference.	Rustan Leino	2013-07-16
\| \| \| \|	Removed three redundant multiset axioms.
*	Computations!	Unknown	2013-07-04
\| \| \| \| \| \| \|	Generates 'computing' axioms for both all formals and just decreasing formals. Supported are literal datatypes, booleans and numbers. The axioms are given a weight of 10, which seems enough for Z3 to give up when it is sane to do so.
*	Changed ranking function for Seq, so that it's compatible with data types.	Unknown	2013-06-26
\|
*	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).
*	Removed the set cardinality/subset axiom (with no trigger, it caused test ↵	Rustan Leino	2013-04-02
\| \| \| \|	suite to fail; even with a restrictive trigger, it added a few minutes to the test suite)
*	Updated cardinality axioms for sets.	Nadia Polikarpova	2013-03-30
\|
*	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;
*	Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ↵	Rustan Leino	2013-03-27
\| \| \| \| \| \|	in compiling assign-such-that statements Added run-time support for printing sets, multisets, maps, and sequences
*	First take on set, multiset and map cardinality.	Nadia Polikarpova	2013-03-22
\|
*	Bumped version to 1.6.1, to be released as a binary and on rise4fun.	Rustan Leino	2013-03-10
\|
*	Disallow allocations in ghost contexts	Rustan Leino	2013-03-06
\|
*	Encode codatatype equalities by predefined copredicates, including their ↵	Rustan Leino	2013-01-15
\| \| \| \|	prefix versions
*	Include BVD in build (to copy it into the Dafny\Binaries directory)	Unknown	2012-10-30
\| \| \| \|	Batch file for producing a binary distributions
*	Test cases for co-inductive proofs, and an axiom that makes some of them ↵	Rustan Leino	2012-10-19
\| \| \| \|	possible
*	Added some axioms to try to recover boxed data. In particular, any element ↵	Unknown	2012-10-17
\| \| \| \|	'x' of a set in the encoding satisfies Box(Unbox(x))==x. The soundness and performance of the axiomatization are dicey, so the axioms are made available only to method in-parameters.
*	Change the encoding of proof certificates to make the two levels explicit	Unknown	2012-10-12
\| \| \| \|	Restrict what conclusions comethods are allowed to have
*	New feature:	Rustan Leino	2012-10-11
\| \| \| \| \| \| \|	* Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with) Code restructuring: * New set of Boogie procedure stubs generated for each other * Start of improvements around TrSplitExpr
*	Fixed some build/migration issues	Rustan Leino	2012-10-04
\|
*	Dafny: fixed merge	Rustan Leino	2012-10-04
\|
*	Merge	Rustan Leino	2012-10-04
\|\
* \|	Dafny: complete implementation of iterators	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: more part of verifying iterators	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: incomplete snapshot of verification of iterators	Rustan Leino	2012-10-02
\| \|
\| *	Dafny: removed div/mod axioms, since Boogie now interprets div/mod	Unknown	2012-09-28
\| \| \| \| \| \| \| \| \| \|	Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support
\| *	Boogie: new syntax for integer division and modulus: use div and mod instead ↵	boehmes	2012-09-27
\|/ \| \| \|	of / and %