debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Propagate literals through equality operations.	Nada Amin	2014-03-19
\|
*	Merge	Rustan Leino	2014-03-17
\|\
* \|	Fixed resolution bug where "var x := x" was allowed.	Rustan Leino	2014-03-17
\| \|
* \|	AST refactoring:	Rustan Leino	2014-03-17
\| \| \| \| \| \| \| \| \| \|	Changed VarDecl to no longer inherit from Statement. Removed ConcreteSyntaxStatement and changed VarDeclStmt's superclass be Statement.
\| *	Merge	Nada Amin	2014-03-12
\| \|\ \| \|/ \|/\|
\| *	Improve computations, in particular compositionality. Isolated useless ↵	Nada Amin	2014-03-12
\| \| \| \| \| \| \| \|	literals around if-then-else as a surprising source of practical hanging.
* \|	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.