debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Added a test case from the ACL2 book	Rustan Leino	2014-03-10
\|
*	Moved the (long running) CloudMake test files to their own directory	Rustan Leino	2014-02-28
\|
*	Added CloudMake formalization and proofs to the test suite	Rustan Leino	2014-02-26
\|
*	Added examples mentioned in a paper on circular coinduction.	Rustan Leino	2014-02-25
\|
*	Added further assistance in coming up with decreases clauses in SCCs with ↵	Rustan Leino	2014-02-24
\| \| \| \|	co-recursive calls.
*	Refactored code for dealing with SCCs in the call graph.	Rustan Leino	2014-02-24
\| \| \| \|	Fixed bug.
*	Minor clean-up in a couple of test files.	Rustan Leino	2014-02-24
\|
*	Fixed bugs in co-call checks	Rustan Leino	2014-02-23
\|
*	Added another colemma-calls-function-recursively test	Rustan Leino	2014-02-23
\|
*	Fixed some checking of recursive method/copredicate calls	Rustan Leino	2014-02-23
\|
*	Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵	Rustan Leino	2014-02-23
\| \| \| \|	-> "prefix lemma")
*	Allow unary minus on reals	Rustan Leino	2014-02-13
\|
*	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 ↵	Rustan Leino	2014-02-13
\| \| \| \|	Foundations" book (Pierce et al.)
*	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).
*	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 ↵	Rustan Leino	2014-01-14
\| \| \| \| \| \| \| \|	traces into preconditions of called functions
\| *	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 ↵	Rustan Leino	2014-01-09
\|/ \| \| \|	axioms for functions with match'es are no longer specialized
*	Dafny renditions of sorting algorithms proved in other provers (Coq, ↵	Rustan Leino	2014-01-08
\| \| \| \|	Isabelle, F*)
*	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.
\| *	:autoReq now works with static functions.	Bryan Parno	2014-01-08
\| \| \| \| \| \| \| \|	This required fixing a small bug in how StaticReceiverExpr's were being handled
\| *	Add autoReq support for matches.	Bryan Parno	2014-01-08
\| \| \| \| \| \| \| \|	Add better handling of resolved data types in autoReq.
\| *	Added support for automatic generation of function requirements via the ↵	Bryan Parno	2014-01-08
\|/ \| \| \|	:autoReq attribute.
*	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", ↵	Rustan Leino	2014-01-03
\| \| \| \| \| \|	sequences, or roll-it-yourself maps. Instead, use "nat", List, and "map". Use VC splitting to combat performance issues.
*	Allow "match" expressions anywhere	Rustan Leino	2014-01-03
\|
*	Added proper parsing for StmtExpr's in all contexts.	Rustan Leino	2013-12-30
\| \| \| \| \| \|	Adjusted printer accordingly. Fixed bug in Substituter for CalcStmt in StmtExpr's. Always show terminating semi-colon in hover-text for default decreases clauses.
*	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 ↵	Rustan Leino	2013-12-18
\| \| \| \|	and use a sorting routine parameterized with a comparison function
*	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 ↵	wuestholz	2013-12-18
\| \| \| \|	to use it.
*	Fixed pretty printing of calc statements to use the new(-since-long) format.	Rustan Leino	2013-12-17
\| \| \| \| \|	Disallow dangling operator in calc (which had also allowed soundness bug). Don't reprove the test files in dafny0 after testing their pretty printing.