debian-dafny - Debian packaging for Dafny

	Commit message (Expand)	Author	Age
*	New test file: dafny4/NumberRepresentations.dfy	Rustan Leino	2014-02-13
*	Added to the test suite a Dafny version of Basics.v from the "Software Founda...	Rustan Leino	2014-02-13
*	Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for lite...	Rustan Leino	2014-02-13
*	Updated test suite after a Boogie bug fix for reals	Rustan Leino	2014-02-10
*	Add basic tests for reals	Bryan Parno	2014-02-10
*	Preliminary support for reals in Dafny specs. No compiler suport yet.	Bryan Parno	2014-02-10
*	Added examples from the Kozen and Silva paper "Practical Coinduction".	Rustan Leino	2014-02-10
*	Provide more detailed feedback for errors involving if-then-else	Bryan Parno	2014-02-03
*	Some simplifications to the proof of GHC MergeSort.	Rustan Leino	2014-02-01
*	Added an alternative statement of the prime theorem	Rustan Leino	2014-01-24
*	Fix a bug in the interaction between opaque and generics	Bryan Parno	2014-01-23
*	Merge	Rustan Leino	2014-01-14
\|\
* \|	Improve error information by generating "Related location" information that t...	Rustan Leino	2014-01-14
\| *	Improve autoReq's interactions with opaque	Bryan Parno	2014-01-13
\|/
*	Proof that there is no bound on the size of prime numbers	Rustan Leino	2014-01-11
*	Fixed spurious complaint about assignment to non-ghost variable	Rustan Leino	2014-01-11
*	Merge	Rustan Leino	2014-01-11
\|\
\| *	A better fix to deal with StaticReceiverTypes affected by autoReq.	Bryan Parno	2014-01-10
* \|	GHC-MergeSort: removed lemmas and proof steps rendered unnecessary now that a...	Rustan Leino	2014-01-09
\|/
*	Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle...	Rustan Leino	2014-01-08
*	Merge	Rustan Leino	2014-01-08
\|\
* \|	Allow left-hand sides of a let expression to be patterns (like in the case of...	Rustan Leino	2014-01-08
\| *	:autoReq now works with static functions.	Bryan Parno	2014-01-08
\| *	Add autoReq support for matches.	Bryan Parno	2014-01-08
\| *	Added support for automatic generation of function requirements via the :auto...	Bryan Parno	2014-01-08
\|/
*	More thoroughly check for nested assume statements during compilation	Rustan Leino	2014-01-05
*	Added ghost let expressions.	Rustan Leino	2014-01-05
*	Renamed a constructor in a test file	Rustan Leino	2014-01-03
*	Removed unused declaration	Rustan Leino	2014-01-03
*	Changed BreadthFirstSearch example to no longer use "inductive naturals", seq...	Rustan Leino	2014-01-03
*	Allow "match" expressions anywhere	Rustan Leino	2014-01-03
*	Added proper parsing for StmtExpr's in all contexts.	Rustan Leino	2013-12-30
*	Add pretty-printing flag to the dafny3 test script.	wuestholz	2013-12-19
*	Added test3/GenericSort.dfy, which shows how modules can be used to write and...	Rustan Leino	2013-12-18
*	Add an assertion to a test case to make it less flaky (hopefully).	wuestholz	2013-12-18
*	Added missing file (sorry)	Rustan Leino	2013-12-18
*	Add support for the /verifySeparately flag in Boogie and change most tests to...	wuestholz	2013-12-18
*	Fixed pretty printing of calc statements to use the new(-since-long) format.	Rustan Leino	2013-12-17
*	Don't expand {:opaque} for inherited functions. (Note, more design is still ...	Rustan Leino	2013-12-17
*	Merge	Rustan Leino	2013-12-17
\|\
* \|	Don't inline opaque functions.	Rustan Leino	2013-12-17
\| *	Merge	Rustan Leino	2013-12-16
\| \|\ \| \|/ \|/\|
\| *	Fixed bug where free conditions preceded checked conditions (for inlined pred...	Rustan Leino	2013-12-16
* \|	Pass assert/assume attributes down to Boogie	Rustan Leino	2013-12-16
* \|	Add support for the :axiom attribute for ghost methods.	Bryan Parno	2013-12-13
* \|	Added support for opaque function definitions, indicated via the {:opaque} at...	Bryan Parno	2013-12-13
* \|	Add support for the "include" keyword, which accepts a (possibly relative) path	Bryan Parno	2013-12-10
* \|	Update an 'Answer' file.	wuestholz	2013-12-10
* \|	Change a test program to verify faster (by a factor of 10-25).	wuestholz	2013-12-10
* \|	Updated an 'Answer' file.	wuestholz	2013-12-03
\|/