debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
...
*	Dafny: fixed up test suite (temporarily removed autocontract tests)	Jason Koenig	2012-06-28
\|
*	Dafny: fixed some test cases	Jason Koenig	2012-06-28
\|
*	Undo bad merge.	afd	2012-06-27
\|
*	Merge	Unknown	2012-06-25
\|\
\| *	Dafny: Since it's no longer true that all types support equality at run-time ↵	Unknown	2012-06-21
\| \| \| \| \| \| \| \|	(in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.
* \|	Merged with default.	chmaria	2012-06-18
\|\\|
\| *	Dafny: fixed a couple of compiler bugs	Unknown	2012-06-14
\| \|
\| *	Dafny: cleaned up test scripts a little	Unknown	2012-06-14
\| \|
\| *	Dafny: added another version of the majority finding algorithm to the test suite	Unknown	2012-06-12
\| \|
\| *	Dafny: beefed up allocation axioms for boxes stored in fields	Unknown	2012-06-12
\| \|
* \|	Dafny: Added tests.	chmaria	2012-06-12
\| \|
\| *	Dafny: added some test programs	Rustan Leino	2012-06-08
\|/
*	Dafny: support assign-such-that in var declarations in refinements	Unknown	2012-03-15
\|
*	Dafny: added StoreAndRetrieve refinement example	Unknown	2012-03-15
\|
*	Dafny: implemented thresholds for the new interval domain (/infer:j)	Rustan Leino	2011-12-12
\|
*	Dafny tests: Disabled SnapshotableTrees.dfy for now while performance issues ↵	Rustan Leino	2011-12-07
\| \| \| \|	are being investigated
*	Dafny: call C# compiler directly from inside Dafny, and optionally produce a ↵	Rustan Leino	2011-11-22
\| \| \| \|	.cs file with the new /spillTargetCode switch
*	Added some Dafny and Boogie test cases, including Turing's factorial ↵	Rustan Leino	2011-11-03
\| \| \| \|	program, Hoare's classic FIND, and some induction tests for negative integers
*	Dafny: Commented out SnapshotableTrees.Node.FunctionalInsert while ↵	Rustan Leino	2011-10-26
\| \| \| \|	performance issues with the prover and going into SMTLib2 mode are being investigated.
*	Dafny: fixed performance-buggy translation of exists, and also added some ↵	Rustan Leino	2011-10-19
\| \| \| \|	other features in SplitExpr (such as induction on existential quantifiers)
*	Dafny: added COST Verification Competition challenge programs to test suite	Rustan Leino	2011-10-07
\|
*	Dafny: Updated snapshotable tree to remove IsReadonly precondition for ↵	Rustan Leino	2011-09-30
\| \| \| \|	CreateIterator.
*	Dafny: beautification in one test case, and fixed an Answer file	Rustan Leino	2011-09-29
\|
*	Dafny: Added TreeBarrier as a test case	peter mueller peter.mueller@inf.ethz.ch	2011-09-29
\|
*	Dafny: added Snapshotable Trees example	Rustan Leino	2011-09-11