debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
...
\| *	DafnyExtension: report out-of-time and out-of-memory errors	Rustan Leino	2012-08-17
\|/
*	DafnyExtension: toward some fixes	Unknown	2012-08-17
\|
*	DafnyExtension: simplified display of type names and field names	Unknown	2012-08-17
\|
*	DafnyExtension: various improvements	Unknown	2012-08-16
\|
*	DafnyExtension: improvements	Rustan Leino	2012-08-15
\|
*	DafnyExtension: do verification in a non-UI thread	Rustan Leino	2012-08-15
\|
*	DafnyExtension: fixed more missing cases for hover texts	Unknown	2012-08-15
\|
*	Dafny: fixed some bugs in the newly added DafnyExtension code	Unknown	2012-08-15
\|
*	Dafny: added Statement.SubExpressions getter	Unknown	2012-08-15
\| \| \| \|	DafnyExtension: added hover text for identifiers
*	Dafny: added Statement.SubExpressions getter	Unknown	2012-08-15
\| \| \| \|	DafnyExtension: added hover text for identifiers
*	Dafny: removed the defunct "havoc" keyword from various source-code highlighters	Unknown	2012-08-15
\|
*	Dafny emacs mode: changed a menu name (Does anyone ever use this menu anyhow?)	Unknown	2012-08-14
\|
*	Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension ↵	Unknown	2012-08-14
\| \| \| \|	crashing after certain deletes)
*	DafnyExtension: hide execution-trace output, show split-expr related error ↵	Rustan Leino	2012-08-10
\| \| \| \|	locations, set a 10-second timeout
*	DafnyExtension: improvements	Rustan Leino	2012-08-08
\|
*	DafnyExtension: fixed build issues; added support for some refinement features	Rustan Leino	2012-08-08
\|
*	Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and ↵	Unknown	2012-08-08
\| \| \| \|	visually indicates a non-verified buffer
*	Dafny VS Extension: edited to make it build with new AST types, fixed some ↵	Unknown	2012-08-02
\| \| \| \|	bugs, added a temporary progress indicator
*	Dafny: removed allocated keyword, changed module import syntax. "opened" ↵	Jason Koenig	2012-07-30
\| \| \| \|	keyword is parsed but ignored.
*	Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ↵	Jason Koenig	2012-07-10
\| \| \| \|	parallel syntax, other minor fixes
*	Dafny: added copredicates	Rustan Leino	2012-07-03
\|
*	Dafny: Merge	Jason Koenig	2012-06-27
\|\
* \|	Dafny: Implemented abstract modules	Jason Koenig	2012-06-26
\| \|
\| *	Dafny: equality-support test cases. This is just a snapshot--some things ↵	Unknown	2012-06-22
\|/ \| \| \|	still to be fixed up.
*	Dafny: removed support for the old keyword "unlimited" (all functions are ↵	Unknown	2012-06-11
\| \| \| \|	limited)
*	Dafny: added finite maps	Unknown	2012-05-25
\|
*	Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵	Unknown	2012-04-25
\| \| \| \| \| \| \|	handle generic datatypes correctly) Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code) Dafny: added "codatatype" declaration (syntax only for now)
*	Dafny VSX: fixed compilation inconsistency	Rustan Leino	2012-01-10
\|
*	Dafny: added predicates	Rustan Leino	2012-01-10
\|
*	Dafny: Start of new refinement features -- clean out old ones	Rustan Leino	2012-01-04
\|
*	Merge	Rustan Leino	2011-11-22
\|\
\| *	DafnyExtension: fix up compilation (once again)	Rustan Leino	2011-11-22
\| \|
* \|	Dafny: Added "type" declaration (syntax: "type X;"), which introduces an ↵	Rustan Leino	2011-11-21
\|/ \| \| \|	arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
*	DafnyExtension: fixed build problems	Rustan Leino	2011-11-15
\|
*	Dafny: allow single-quote as a character in identifiers in the VS2010 mode	Rustan Leino	2011-11-09
\|
*	Dafny: added "multiset" keyword to syntax highlighting in emacs, vim, latex, VSX	Rustan Leino	2011-11-09
\|
*	Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" ↵	Rustan Leino	2011-10-26
\| \| \| \|	statement)
*	Dafny: changed triggers (which are never really used, anyhow) from having a ↵	Rustan Leino	2011-10-21
\| \| \| \| \| \| \|	special syntactic form to being just an attribute Dafny: added "parallel" statement (so far, only parsing and resolving) Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them)
*	Dafny: for VS mode, let lexer allow "?"	Rustan Leino	2011-08-04
\|
*	Added new multiset keyword to VS2010 syntax highlighter.	Jason Koenig	2011-07-11
\|
*	Dafny: removed deprecated "call" and "use" keywords from syntax highlighters	Rustan Leino	2011-06-20
\|
*	Dafny: added constructors	Rustan Leino	2011-05-28
\|
*	Better VisualStudio plugin feedback.	Jason Koenig	2011-05-27
\|
*	VisualStudio plugin now informs the user of a timeout.	Jason Koenig	2011-05-26
\|
*	Dafny: Alternative (and candidate replacement) syntax for declaring datatypes	Rustan Leino	2011-04-20
\| \| \| \|	Dafny: Additional induction test cases
*	Dafny: added type "nat"	Rustan Leino	2011-04-19
\|
*	Dafny: added "choose" operator on sets	rustanleino	2011-03-26
\|
*	Dafny:	rustanleino	2011-02-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case). * Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.) * Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type. * More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal") * Add axioms about idempotence of set union and intersection * The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one * In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase * Fixed error in translation of while(*)
*	Dafny: implemented a more precise scheme for allowing use of a function's ↵	rustanleino	2011-02-03
\| \| \| \|	rep axiom
*	VSIP integration into VS: Changed idle delay to 300ms (from 1s). ↵	rustanleino	2010-11-17
\| \| \| \|	Distinguish warnings/errors in Chalice.