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: compile iterators	Rustan Leino	2012-09-26
\| \|
* \|	Dafny: added test cases for resolving iterators	Rustan Leino	2012-09-25
\| \|
\| *	Bugfix in the translation of calc statements (oops), added more resolution ↵	Nadia Polikarpova	2012-09-21
\|/ \| \| \|	and verification tests
*	Dafny: improved checking of inherited postconditions (in refinements)	Unknown	2012-09-10
\|
*	Dafny: allow 'decreases *' (that is, non-terminating recursion) on ↵	Rustan Leino	2012-09-09
\| \| \| \|	tail-recursive methods
*	Dafny: support opening modules into the local scope	Jason Koenig	2012-07-30
\|
*	Dafny: fixed bug in which old locals were not properly forbidden from being ↵	Jason Koenig	2012-07-12
\| \| \| \|	modified during refinement
*	Dafny: More work on the coinduction principle	Rustan Leino	2012-07-09
\|
*	Dafny: equality-support test cases. This is just a snapshot--some things ↵	Unknown	2012-06-22
\| \| \| \|	still to be fixed up.
*	Dafny: cleaned up test scripts a little	Unknown	2012-06-14
\|
*	Dafny: liberalized equality to work when the types could possibly be the same	Jason Koenig	2012-06-13
\| \| \| \|	(i.e. a != b is allowed when a: array<int> and b: array<T>)
*	Dafny: Added maps to regression tests.	Unknown	2012-05-29
\|
*	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: allow more skeleton statements in refinements	Unknown	2012-03-02
\|
*	Dafny: allow various forms of leaving off type arguments in declarations	Rustan Leino	2012-02-16
\|
*	Dafny: Fixed a bug in the printing of let expressions.	wuestholz	2012-01-24
\|
*	Dafny: added predicates	Rustan Leino	2012-01-10
\|
*	Dafny: added support for simple superposition refinements	Rustan Leino	2012-01-09
\|
*	Dafny: firmed up the module system	Rustan Leino	2012-01-05
\|
*	Dafny: disengaged old refinement test files	Rustan Leino	2012-01-04
\|
*	Dafny: Fixed a bug in the pretty printer.	wuestholz	2011-12-26
\|
*	Dafny: Made sure that error locations refer to the Dafny program, even if ↵	wuestholz	2011-12-15
\| \| \| \|	the /print option is used.
*	Dafny: added let expressions (syntax: "var x := E0; E1")	Rustan Leino	2011-11-14
\| \| \| \| \|	Dafny: firmed up semantics of assert/assume expressions (the condition is now good for all program control paths that pass through the expression) Dafny: various implementation clean-ups
*	Dafny: added assert/assume expressions	Rustan Leino	2011-11-09
\|
*	Dafny: implemented compilation of parallel statements	Rustan Leino	2011-10-25
\| \| \| \|	Dafny: beefed up resolution of parallel statements
*	Dafny: continued translation of "parallel" statements (Assign and Proof ↵	Rustan Leino	2011-10-24
\| \| \| \| \| \| \|	forms are mostly there, Call is missing and so is compilation) Dafny: included some test cases for the "parallel" statement Dafny: starting changing old "foreach" statements to the new "parallel" statement
*	Dafny: Fixed a bug in the printer that led to a stack overflow.	wuestholz	2011-08-11
\|
*	Fixed regression test failures due to removal of bodiless methods and functions.	Jason Koenig	2011-07-15
\|
*	Dafny: Fixed bug in call statements where mutability of out parameters was ↵	Jason Koenig	2011-07-06
\| \| \| \| \| \|	not checked. Added regression test.
*	Dafny: Updated regression tests to include chaining disjoint operators.	Jason Koenig	2011-07-05
\|
*	Added regression tests for new return statements with parameters.	Jason Koenig	2011-06-29
\|
*	Added regression test for loop modifies clauses.	Jason Koenig	2011-06-28
\|
*	Dafny: retired "use" statements	Rustan Leino	2011-05-27
\|
*	Dafny: added chaining operators	Rustan Leino	2011-05-27
\|
*	Dafny: allow class names to be used when referring to static functions (and, ↵	Rustan Leino	2011-05-21
\| \| \| \|	soon, methods), and test cases for new name resolution rules
*	Dafny: let verifier, not the resolver, check for missing cases in match ↵	Rustan Leino	2011-05-19
\| \| \| \|	expressions/statements
*	Dafny: added set comprehension expressions	Rustan Leino	2011-05-18
\|
*	Dafny: forbid "decreases *" on ghost loops	Rustan Leino	2011-05-12
\|
*	Dafny: added type "nat"	Rustan Leino	2011-04-19
\|
*	Dafny: Allow field selections and array-element selection as LHSs of ↵	Unknown	2011-04-05
\| \| \| \|	assignments where RHS is not just an expression
*	Dafny: compile quantifiers	rustanleino	2011-03-26
\| \| \| \| \| \|	Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges
*	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: allow self-calls in function postconditions--these simply refer to ↵	rustanleino	2011-02-03
\| \| \| \|	the result value of the current call
*	Dafny:	rustanleino	2010-09-17
\| \| \| \| \| \|	* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation) * Changed syntax of array length from \|a\| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays. * Internally, this meant adding support for built-in classes and readonly fields
*	Dafny: better error reporting on resolution of refinements. Replace ↵	kyessenov	2010-07-14
\| \| \| \|	assertions with "if"s to handle errors gently and add cycle detection check.
*	Dafny: added Carrol Morgan's calculator regression test.	kyessenov	2010-07-02
\|
*	Dafny: added a regression test for the refinement extension.	kyessenov	2010-07-02
\|