debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	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 heuristics for finding witnesses in assign-such-that checking	Unknown	2012-08-10
\|
*	DafnyExtension: improvements	Rustan Leino	2012-08-08
\|
*	Dafny: reverify if the refining method modifies the heap.	Jason Koenig	2012-08-01
\|
*	Dafny: support opening modules into the local scope	Jason Koenig	2012-07-30
\|
*	Dafny: removed allocated, changed semantics of fresh	Jason Koenig	2012-07-29
\| \| \| \| \|	-allocated(x) removed, as really only useful in old(...) -old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).
*	Dafny: added structural refinement check	Jason Koenig	2012-07-29
\|
*	Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ↵	Jason Koenig	2012-07-17
\| \| \| \|	parallel statements.
*	Dafny: compilation of abstract modules, including local definitions (as in ↵	Jason Koenig	2012-07-17
\| \| \| \| \| \| \|	module A as B = C) * * * Dafny: compilation of abstract modules, including local definitions (as in module A as B = C)
*	Merge	Rustan Leino	2012-07-09
\|\
* \|	Dafny: More work on the coinduction principle	Rustan Leino	2012-07-09
\| \|
\| *	Dafny: added verification that replaced expressions are the same as the original	Jason Koenig	2012-07-09
\| \|
\| *	Dafny: added named expressions and replacement	Jason Koenig	2012-07-09
\| \|
\| *	Dafny: types can now be qualified with full module paths	Jason Koenig	2012-07-06
\| \|
\| *	Dafny: disallow importing ghost modules into physical ones.	Jason Koenig	2012-07-05
\| \|
* \|	Merge	Rustan Leino	2012-07-04
\|\\|
\| *	Dafny: added static members of _default to the module level scope, at low ↵	Jason Koenig	2012-07-03
\| \| \| \| \| \| \| \|	priority.
\| *	Dafny: added support for nested abstract modules, fixed some translation issues	Jason Koenig	2012-07-03
\| \|
* \|	Dafny: added copredicates	Rustan Leino	2012-07-03
\|/
*	Dafny: updated contracts to allow null parent (of the default module)	Rustan Leino	2012-06-29
\|
*	Dafny: fixed bug with translation of class._System.object;	Jason Koenig	2012-06-28
\|
*	Dafny: Merge	Jason Koenig	2012-06-27
\|\
* \|	Dafny: Fixed module bugs	Jason Koenig	2012-06-27
\| \|
* \|	Dafny: Implemented abstract modules	Jason Koenig	2012-06-26
\| \|
\| *	Dafny: now, equality-support determination and checking feels ripe; so, ↵	Rustan Leino	2012-06-22
\| \| \| \| \| \| \| \| \| \| \| \|	codatatypes would then be sound Dafny: added special case to allow equality comparison against parameter-less datatype values
\| *	Merge	Unknown	2012-06-22
\| \|\
\| * \|	Dafny: mark code for equality-support determination tentative	Unknown	2012-06-22
\| \| \|
\| * \|	Dafny: equality-support test cases. This is just a snapshot--some things ↵	Unknown	2012-06-22
\| \| \| \| \| \| \| \| \| \| \| \|	still to be fixed up.
\| * \|	Dafny: allow "assume ..." as a refining statement (provided it replaces an ↵	Unknown	2012-06-22
\| \| \| \| \| \| \| \| \| \| \| \|	"assume E")
\| * \|	Dafny: deal with equality-support issues in refinements	Unknown	2012-06-22
\| \| \| \| \| \| \| \| \| \| \| \|	Dafny: a small amount of refactoring and bug fixes
\| \| *	Dafny: Fixed bug in CompilerizeName.	chmaria	2012-06-22
\| \| \|
\| \| *	Dafny: fixed two contracts	Rustan Leino	2012-06-22
\| \| \|
\| * \|	Dafny: Since it's no longer true that all types support equality at run-time ↵	Unknown	2012-06-21
\| \|/ \| \| \| \| \| \|	(in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.
\| *	Dafny: improved refinement features; added staged version of the proof of ↵	Unknown	2012-06-19
\| \| \| \| \| \| \| \|	the Schorr-Waite algorithm (the staging features, as well as the newly added comments, make the verification much more digestible)
* \|	Dafny: Added nested modules	Jason Koenig	2012-06-19
\|/
*	Dafny: in compiler, respect C#'s different scoping rules and lack of support ↵	Unknown	2012-06-14
\| \| \| \|	for special characters in identifiers
*	Dafny: Changed the semantics of the assign-such-that statement "x :\| P;" to ↵	Unknown	2012-06-13
\| \| \| \|	check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
*	Dafny: allow types to be qualified with the name of the module that declares ↵	Unknown	2012-06-11
\| \| \| \|	them (for now, this is supported only in type expressions and "new" allocations, not in places where the type name is used to qualify some other type member)
*	Dafny: removed support for the old keyword "unlimited" (all functions are ↵	Unknown	2012-06-11
\| \| \| \|	limited)
*	Dafny: change labels to use a generic singly linked list	Jason Koenig	2012-06-06
\|
*	Dafny: Added map comprehensions and updated display syntax	Unknown	2012-05-31
\|
*	Dafny: added finite maps	Unknown	2012-05-25
\|
*	Dafny: more correct checking of co-inductive productivity	Unknown	2012-05-18
\|
*	Dafny: improve printing of inductive datatypes	Unknown	2012-05-01
\| \| \| \|	Dafny: don't consider co-datatypes as candidates for default decreases components
*	Dafny: added support for co-recursive calls	Rustan Leino	2012-05-01
\|
*	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: added assign-such-that statements; syntax: x,y,a[i],o.f :\| Expr;	Unknown	2012-03-15
\|
*	Dafny: fixed compilation problem with names in _default module	Rustan Leino	2012-03-08
\|
*	Dafny: added ghost modules (the meaning is simply that such a module will ↵	Rustan Leino	2012-03-07
\| \| \| \| \| \| \|	not be compiled) Dafny: improved :autocontracts heuristic for detecting "simple query method" Dafny: fixed some bugs