debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	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.
*	Added ghost let expressions.	Rustan Leino	2014-01-05
\|
*	Make ModuleDefinition inherit from TopLevelDecl instead of just Declaration	Bryan Parno	2014-01-03
\|
*	Merge	Rustan Leino	2013-12-30
\|\
* \|	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.
\| *	Changed the iterator class hover text back to the iterator name (which is ↵	Rustan Leino	2013-12-20
\|/ \| \| \|	consistent with everything else), not the "iterator" keyword
*	Added an .EndTok for every statement. (Note, in some places, especially in ↵	Rustan Leino	2013-12-19
\| \| \| \| \| \| \|	VarDecl statements, there's often no good .EndTok information.) Used the .EndTok in CaptureState information. In other words, move the blue dots in the IDE to after the statement just executed. Removed /!/ comments in some parts of the source code -- CodeContracts reveal this information.
*	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.
*	Add support for the :axiom attribute for ghost methods.	Bryan Parno	2013-12-13
\| \| \| \| \| \|	This suppresses compiler errors for ghost methods and functions without bodies. Also changed the parser to complain about bodyless methods and functions without bodies if /noCheating:1 is specified.
*	Add support for the "include" keyword, which accepts a (possibly relative) path	Bryan Parno	2013-12-10
\| \| \| \| \|	to another Dafny file. That file's functions and methods are included but not checked. This is intended to support incremental verification on a per-file basis.
*	Added support for attributes on variable declarations.	wuestholz	2013-11-18
\|
*	Allow calls to side-effect-free ghost methods from expressions	Rustan Leino	2013-08-06
\|
*	Merged PredicateExpr and CalcExpr into a single StmtExpr	Rustan Leino	2013-08-06
\| \| \| \|	In that process, added a SubstStmt method (and entourage) for substituting into statements
*	Introduced keywords "lemma" (like a "ghost method", but not allowed to have ↵	Rustan Leino	2013-08-02
\| \| \| \|	a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
*	Regenerated Parser after a merge.	Nadia Polikarpova	2013-07-31
\|
*	Add support for hexidecimal numbers.	parno	2013-07-30
\|
*	Fixed build failure.	wuestholz	2013-07-25
\|
*	Allow field names to be sequences of digits (this is nice, for example, to ↵	Rustan Leino	2013-07-24
\| \| \| \|	define a Tuple with fields .0 and .1)
*	Because of neighboring parse conflict handlers, must call ResetPeek()	Rustan Leino	2013-07-10
\|
*	Fixed parsing bug in "if" and "while" guards	Rustan Leino	2013-07-10
\|
*	Made the semi-colon after "type" and "module" declarations optional.	Rustan Leino	2013-05-10
\|
*	Make semi-colon after datatype/codatatype declaration optional (in the ↵	Rustan Leino	2013-04-19
\| \| \| \|	future, it will not be allowed at all)
*	The "choose" statement, hacky and specialized as it was, is now gone. Use ↵	Rustan Leino	2013-03-27
\| \| \| \|	the assign-such-that statement instead. For example: x :\| x in S;
*	Finished support for ==# in calc, changed Paulson example to use it.	Nadia Polikarpova	2013-03-20
\|
*	Added explies support to calculations.	Nadia Polikarpova	2013-03-15
\|
*	Added the <== operator.	Nadia Polikarpova	2013-03-14
\|
*	Renamed "parallel" statement to "forall" statement, and made the parentheses ↵	Rustan Leino	2013-03-06
\| \| \| \|	around the bound variables optional.
*	Support for paren-free guards in if and while statements.	Nadia Polikarpova	2013-02-15
\|
*	First take on calc expressions.	Nadia Polikarpova	2013-02-14
\|
*	Changed calc syntax (custom operators are now written before the hint)	Nadia Polikarpova	2013-02-08
\|
*	"!!" can now be parsed as two "!". More concise parsing for "!in".	Nadia Polikarpova	2013-02-07
\|
*	Added parsing and resolution of a new let-such-that expression. Translation ↵	Rustan Leino	2013-01-21
\| \| \| \|	has yet to be implemented.
*	Added some co- test cases. Fixed some bugs.	Rustan Leino	2013-01-20
\|
*	Removed the syntactic form copredicate #-form with the implicit argument.	Rustan Leino	2013-01-16
\| \| \| \|	Added syntactic support for codatatype #-form equalities.
*	Improved error message for making the mistake of saying 'returns' instead of ↵	Rustan Leino	2012-11-25
\| \| \| \|	'yields' for an iterator
*	Parse prefix predicates/methods	Rustan Leino	2012-11-24
\|
*	renamed "abstract module" to "module facade"	Rustan Leino	2012-10-22
\| \| \| \|	renamed "ghost module" to "abstract module", adding a keyword "abstract"
*	New feature:	Rustan Leino	2012-10-11
\| \| \| \| \| \| \|	* Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with) Code restructuring: * New set of Boogie procedure stubs generated for each other * Start of improvements around TrSplitExpr
*	Support default (which, here, means nameless) class-instance constructors	Rustan Leino	2012-10-05
\|
*	Put all sources under \Source directory	Rustan Leino	2012-10-04