debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Updated a test in dafny2 with the new calc syntax.	Nadia Polikarpova	2013-02-14
\|
*	Merge	Nadia Polikarpova	2013-02-13
\|\
\| *	Frame expressions are now checked to be well formed.	Rustan Leino	2013-02-13
\| \| \| \| \| \| \| \|	(A nice consequence of this is that the method IsTotal is no longer needed.)
* \|	Merge	Nadia Polikarpova	2013-02-14
\|\\|
\| *	Report error if type of a quantified variable cannot be inferred	Rustan Leino	2013-02-11
\| \|
* \|	Merge	Nadia Polikarpova	2013-02-12
\|\\|
\| *	Reverted some accidental changes to a test case	Rustan Leino	2013-02-11
\| \|
* \|	Changed calc syntax (custom operators are now written before the hint)	Nadia Polikarpova	2013-02-08
\|/
*	Added some test cases that show exmaples that iterate over set elements.	Rustan Leino	2013-02-02
\|
*	Renamed a variable in some test cases	Rustan Leino	2013-02-02
\|
*	Fixed another specification bug in a test case.	Rustan Leino	2013-01-23
\|
*	Fixed bug in translation of method termination checks, and also fixed a ↵	Rustan Leino	2013-01-23
\| \| \| \|	(previously undetected) specification bug in the test suite.
*	Split verification of quantifier expressions into #2 for checked and #1 for ↵	Rustan Leino	2013-01-23
\| \| \| \| \| \|	assumed. Fixed cases where token was not being updated for refinement.
*	Examples from co-induction paper	Rustan Leino	2013-01-22
\|
*	Translate let-such-that expressions	Rustan Leino	2013-01-22
\|
*	More automatic co-induction for comethods	Rustan Leino	2013-01-20
\|
*	Added some co- test cases. Fixed some bugs.	Rustan Leino	2013-01-20
\|
*	Fixed the problem with the previous check-in.	Rustan Leino	2013-01-18
\|
*	Some additional resolution checks for co stuff.	Unknown	2013-01-18
\| \| \| \|	Beefed up some test cases.
*	Proper support for inlining codatatype equalities	Rustan Leino	2013-01-18
\|
*	Removed the syntactic form copredicate #-form with the implicit argument.	Rustan Leino	2013-01-16
\| \| \| \|	Added syntactic support for codatatype #-form equalities.
*	Encode codatatype equalities by predefined copredicates, including their ↵	Rustan Leino	2013-01-15
\| \| \| \|	prefix versions
*	Support for copredicates and prefix predicates in comethods.	Rustan Leino	2012-12-04
\| \| \| \| \| \|	(Missing from the co support are (prefix) equalities of codatatypes, various restrictions on the use of co/prefix-predicates, and tactic support for applying the (prefix-)induction automatically.)
*	Parse prefix predicates/methods	Rustan Leino	2012-11-24
\|
*	Beefed up loop invariant to prove a functional postcondition in a test case.	Rustan Leino	2012-11-24
\|
*	fixed type resolution bug (http://boogie.codeplex.com/discussions/403801)	Rustan Leino	2012-11-20
\|
*	Beautified a test program	Rustan Leino	2012-11-19
\|
*	renamed "abstract module" to "module facade"	Rustan Leino	2012-10-22
\| \| \| \|	renamed "ghost module" to "abstract module", adding a keyword "abstract"
*	allow a refinement to introduce "return" statements, at the price of ↵	Rustan Leino	2012-10-22
\| \| \| \| \| \|	re-verifying the postcondition at that time let refined classes inherit attributes
*	added some calculational proofs from Dijkstra's writings	Rustan Leino	2012-10-21
\|
*	Test cases for co-inductive proofs, and an axiom that makes some of them ↵	Rustan Leino	2012-10-19
\| \| \| \|	possible
*	added two "calc" proofs (by Nadia) of the MajorityVote example	Unknown	2012-10-19
\|
*	fixed and improved scheme for inferring type parameters	Rustan Leino	2012-10-19
\|
*	Added a test case for "all cases of a datatype"	Unknown	2012-10-17
\|
*	Included "all cases of a datatype" property for method in-parameters (see ↵	Unknown	2012-10-17
\| \| \| \|	http://boogie.codeplex.com/discussions/397616).
*	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.
*	Added/fixed decreases clauses that use multisets or maps.	Unknown	2012-10-16
\|
*	Change the encoding of proof certificates to make the two levels explicit	Unknown	2012-10-12
\| \| \| \|	Restrict what conclusions comethods are allowed to have
*	Removed some old code for the defunct array-range assignments	Rustan Leino	2012-10-11
\|
*	Removed the old (though automatic) coinduction principle	Rustan Leino	2012-10-11
\|
*	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
*	improved and fixed compilation and resolution of assign-such-that statements	Rustan Leino	2012-10-05
\|
*	Longer output lines to indicate failures in regression test suite	Rustan Leino	2012-10-05
\|
*	Support default (which, here, means nameless) class-instance constructors	Rustan Leino	2012-10-05
\|
*	Fixed some goof-ups in the test script edits	Rustan Leino	2012-10-04
\| \| \| \|	Changed the test output to make it easier to spot (in the console output) that everything passed with success or if there were any failures
*	Added Test/dafny3 and another test file for iterators (hey, you can even run ↵	Rustan Leino	2012-10-04
\| \| \| \| \| \|	Iter.dfy!) Fixed migration issues
*	changed default decreases clause for functions with a reads clause: use the ↵	Rustan Leino	2012-10-04
\| \| \| \|	reads clause followed by the list of parameters
*	Fixed some build/migration issues	Rustan Leino	2012-10-04
\|
*	Dafny: fixed merge	Rustan Leino	2012-10-04
\|
*	Merge	Rustan Leino	2012-10-04
\|\