debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵	Rustan Leino	2013-03-05
\| \| \| \|	Codeplex repositories.
*	Merge	Rustan Leino	2012-10-04
\|\
* \|	Dafny: complete implementation of iterators	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: automatically update iterator _new field upon allocations	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: good error locations for yield statements; other iterator ↵	Rustan Leino	2012-10-03
\| \| \| \| \| \| \| \|	improvements / bug fixes
* \|	Dafny: more part of verifying iterators	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: changed iterator body to resolve to implicit fields rather than to ↵	Rustan Leino	2012-10-02
\| \| \| \| \| \| \| \|	the formal in- and yield-parameters
* \|	Dafny: handle decreases clause for iterators	Rustan Leino	2012-10-02
\| \|
* \|	Dafny: incomplete snapshot of verification of iterators	Rustan Leino	2012-10-02
\| \|
* \|	Dafny: compile iterators	Rustan Leino	2012-09-26
\| \|
* \|	Dafny: added iterators; for now, only parsing and resolving (and printing ↵	Rustan Leino	2012-09-25
\| \| \| \| \| \| \| \|	and refining), no compilation or verification
\| *	Use expression splitting for checking calculation steps	Nadia Polikarpova	2012-09-23
\| \|
\| *	Bugfix in the translation of calc statements (oops), added more resolution ↵	Nadia Polikarpova	2012-09-21
\| \| \| \| \| \| \| \|	and verification tests
\| *	Well-formedness check for calc lines	Nadia Polikarpova	2012-09-19
\| \|
\| *	Allow multiple calc/block statements in a hint. Removed the empty calc test ↵	Nadia Polikarpova	2012-09-19
\| \| \| \| \| \| \| \|	from dafny2/Calculations, as it actually belongs in dafny0.
\| *	Made verification error message more explicit	Nadia Polikarpova	2012-09-19
\| \|
\| *	Allow empty calc statements	Nadia Polikarpova	2012-09-19
\| \|
\| *	Allow custom operators on a line	Nadia Polikarpova	2012-09-17
\| \|
\| *	Renamed terms into lines (according to the proposal), fixed some contracts	Nadia Polikarpova	2012-09-16
\| \|
\| *	Error reporting for calculation steps	Nadia Polikarpova	2012-09-14
\| \|
\| *	Calc statements: Renamed Steps into Terms; introduced Steps (expressions ↵	Nadia Polikarpova	2012-09-14
\|/ \| \| \|	t<i> op t<i + 1>), generated during resolution; first version of the translation
*	Dafny: improved checking of inherited postconditions (in refinements)	Unknown	2012-09-10
\|
*	Merge	Rustan Leino	2012-09-10
\|\
* \|	Dafny: allow 'decreases *' (that is, non-terminating recursion) on ↵	Rustan Leino	2012-09-09
\| \| \| \| \| \| \| \|	tail-recursive methods
* \|	Dafny: for refinements, don't consider a newly provided predicate body to be ↵	Unknown	2012-08-30
\| \| \| \| \| \| \| \|	an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be
\| *	Dafny: allow more corecursive calls for copredicates	Rustan Leino	2012-08-30
\|/
*	Dafny: fixed bug in checking postconditions of functions that mention the ↵	Unknown	2012-08-29
\| \| \| \|	result the function itself
*	Dafny: added heuristics for finding witnesses in assign-such-that checking	Unknown	2012-08-10
\|
*	DafnyExtension: hide execution-trace output, show split-expr related error ↵	Rustan Leino	2012-08-10
\| \| \| \|	locations, set a 10-second timeout
*	Dafny: reverify if the refining method modifies the heap.	Jason Koenig	2012-08-01
\|
*	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: restored soundness for refinement by disallowing certain updates and ↵	Jason Koenig	2012-07-11
\| \| \| \|	method calls
*	Dafny: fixed translation bug in maps with objects in the domain, added test case	Jason Koenig	2012-07-11
\|
*	Dafny: fixed bad merge	Rustan Leino	2012-07-09
\|
*	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
\| \|
* \|	Merge	Rustan Leino	2012-07-04
\|\\|
\| *	Dafny: added support for nested abstract modules, fixed some translation issues	Jason Koenig	2012-07-03
\| \|
* \|	Dafny: removed old Substitute method (which has been replaced by a ↵	Rustan Leino	2012-07-03
\| \| \| \| \| \| \| \|	Substituter class)
* \|	Dafny: added copredicates	Rustan Leino	2012-07-03
\| \|
\| *	Dafny: re-added field non-uniqueness (was accidentally reverted by a bad merge)	Jason Koenig	2012-07-02
\|/
*	Dafny: fixed bug with translation of class._System.object;	Jason Koenig	2012-06-28
\|
*	Dafny: Merge	Jason Koenig	2012-06-27
\|\
* \|	Dafny: Implemented abstract modules	Jason Koenig	2012-06-26
\| \|
\| *	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
\|/
*	Merge	Jason Koenig	2012-06-13
\|\