debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
*	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)
*	Jennisys: added "ensures" to emacs mode	Rustan Leino	2011-10-19
\|
*	Jennisys: change of keywords, now: interface/datamodel/code	Rustan Leino	2011-09-28
\| \| \| \|	Jennisys: allow assignment statements in interfaces (for now, these are syntactic sugar for ensures clauses)
*	Merge	Rustan Leino	2011-08-04
\|\
* \|	Dafny: for VS mode, let lexer allow "?"	Rustan Leino	2011-08-04
\| \|
\| *	Chalie: Fix Visual Studio integration and add note about JVM stack size ↵	stefanheule	2011-08-04
\|/ \| \| \|	problems.
*	Chalice VS integration: recognize string literals	Rustan Leino	2011-08-03
\|
*	Chalice: added string type and string literals (but no other string operations)	Rustan Leino	2011-07-26
\|
*	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
\|
*	Jennisys: Parse and print	Rustan Leino	2011-04-07
\|
*	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
*	Dafny: Improved default decreases clauses for methods and functions	rustanleino	2010-11-25
\| \| \| \| \|	Dafny: Don't display "alloc" field in BVD Chalice: Fixed error-message parsing error in VS mode
*	VSIP integration into VS: Changed idle delay to 300ms (from 1s). ↵	rustanleino	2010-11-17
\| \| \| \|	Distinguish warnings/errors in Chalice.
*	Dafny: Record source positions of start/end curly braces for declaration ↵	rustanleino	2010-10-27
\| \| \| \| \| \|	constructs. Dafny VS2010 extension: link with Dafny and use it to parse and type check
*	Added AssemblyInfo.cs, missing from previous DafnyExtension check-in	rustanleino	2010-10-22
\|
*	New Dafny mode for Visual Studio 2010, using the VS2010 extensions.	rustanleino	2010-10-22
\|
*	Miscellaneous changes:	rustanleino	2010-10-22
\| \| \| \| \| \| \|	* Also copy CodeContractExtender in PrepareBoogieZip.bat * Added some comments and a new program in Test/textbook * Included refinement keywords in Chalice emacs mode * Used assignment instead of spec statement in DuplicatesVideo.chalice
*	Chalice:	rustanleino	2010-10-09
\| \| \| \| \|	* extended the cheap type inference to also consider "in" expressions and quantifiers * added some refinement keywords to the Emacs mode for Chalice
*	Util: Minor changes to the LaTeX listings packages for Boogie and Dafny.	wuestholz	2010-09-30
\|
*	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
*	Vim: add keywords to Chalice	kyessenov	2010-09-02
\|
*	VS 2010: add "spec" as keyword in Chalice	kyessenov	2010-09-02
\|
*	VS2010 mode for Dafny and Boogie: updated, for example to properly deal ↵	rustanleino	2010-09-01
\| \| \| \|	with string literals