debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Added several co-induction examples from a 1996 paper by Larry Paulson.	Rustan Leino	2013-03-15
\|
*	Added explies support to calculations.	Nadia Polikarpova	2013-03-15
\|
*	Added a test case for <==.	Nadia Polikarpova	2013-03-14
\|
*	Adjustments in the /vcsMaxKeepGoingSplits flag in the test suite	Rustan Leino	2013-03-09
\|
*	Disallow allocations in ghost contexts	Rustan Leino	2013-03-06
\|
*	New Answer file from previous change	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.
*	New well-formedness checks for calculations (no cascading).	Nadia Polikarpova	2013-03-05
\|
*	Added side-effects and control-flow checks in hints.	Nadia Polikarpova	2013-03-05
\|
*	Adjustment in test output from previous commit	Rustan Leino	2013-02-21
\|
*	Fixed let-such-that and if-then-else encodings so that they will pass the ↵	Rustan Leino	2013-02-21
\| \| \| \|	subrange tests
*	Added Equals method on Type	Rustan Leino	2013-02-20
\| \| \| \| \|	Fixed some precondition violations Various improvements in Contracts
*	Added tests: parallel calc, better well-formedness checks, calc expression.	Nadia Polikarpova	2013-02-15
\|
*	Support for paren-free guards in if and while statements.	Nadia Polikarpova	2013-02-15
\|
*	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.