debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	minor changes	Checkmate50	2016-06-06
\|
*	Merging complete. Everything looks good crosses fingers	Checkmate50	2016-06-06
\|
*	Added initial support for float addition	Checkmate50	2015-09-17
\|
*	Added the fp32 class, copied from the previously existing BigDec class. No ↵	Dietrich	2015-04-17
\| \| \| \|	significant changes from BigDec have been made
*	The back pred files have been eliminated. The small backpred string is now ↵	qadeer	2013-12-08
\| \| \| \|	directly included in ProverInterface.cs.
*	Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵	Rustan Leino	2013-03-05
\| \| \| \|	Codeplex repositories.
*	Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵	Rustan Leino	2013-03-05
\| \| \| \|	Codeplex repositories.
*	Updated PrepareBoogieZip.bat file for the binary release that just went out ↵	Rustan Leino	2012-10-22
\| \| \| \|	on Codeplex
*	deleted unnecessary files	Unknown	2012-10-04
\|
*	Dafny: fixed merge	Rustan Leino	2012-10-04
\|
*	Merge	Rustan Leino	2012-10-04
\|\
* \|	Dafny: complete implementation of iterators	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: more part of verifying iterators	Rustan Leino	2012-10-03
\| \|
* \|	Dafny: incomplete snapshot of verification of iterators	Rustan Leino	2012-10-02
\| \|
\| *	Updated the 'PrepareBoogieZip.bat' script.	wuestholz	2012-10-01
\| \|
\| *	Dafny: removed div/mod axioms, since Boogie now interprets div/mod	Unknown	2012-09-28
\| \| \| \| \| \| \| \| \| \|	Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support
\| *	Boogie: added type 'real' with overloaded arithmetic operations plus real ↵	boehmes	2012-09-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
\| *	Boogie: new syntax for integer division and modulus: use div and mod instead ↵	boehmes	2012-09-27
\|/ \| \| \|	of / and %
*	Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ↵	Unknown	2012-09-12
\| \| \| \|	and axiomatize [][..0] == [] == [][0..]
*	Implement support for alternative SMT solvers -- CVC3 and CVC4	Peter Collingbourne	2012-09-06
\|
*	Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ↵	Jason Koenig	2012-07-17
\| \| \| \|	parallel statements.
*	Dafny: Implemented abstract modules	Jason Koenig	2012-06-26
\|
*	Dafny: fixed a couple of compiler bugs	Unknown	2012-06-14
\|
*	Dafny: beefed up allocation axioms for boxes stored in fields	Unknown	2012-06-12
\|
*	Dafny: Added map comprehensions and updated display syntax	Unknown	2012-05-31
\|
*	Dafny: Added compilation of finite maps	Unknown	2012-05-25
\|
*	Dafny: added finite maps	Unknown	2012-05-25
\|
*	Dafny: fully qualify (with module names) names of types in the translation ↵	Rustan Leino	2012-01-05
\| \| \| \| \| \| \|	into Boogie Dafny: started cloning of refined classes Dafny: added /rprint switch to print the (syntax of the) resolved Dafny program
*	Dafny: added comment about how to mark the run-time expression-sequencing ↵	Rustan Leino	2012-01-04
\| \| \| \|	method as a good candidate for inlining (supported in .NET 4.5)
*	Dafny: compile let expressions efficiently (i.e., with an extra variable, ↵	Rustan Leino	2012-01-04
\| \| \| \|	not with a substitution)
*	Dafny: moved definition of class.array into prelude, anticipating writing ↵	Rustan Leino	2011-11-09
\| \| \| \|	axioms that use it
*	Dafny: removed support for assigning to an array-range (that is, an ↵	Rustan Leino	2011-10-26
\| \| \| \|	assignment statement where the LHS has the form a[lo..hi])
*	Dafny: implemented compilation of parallel statements	Rustan Leino	2011-10-25
\| \| \| \|	Dafny: beefed up resolution of parallel statements
*	Updated 'PrepareBoogieZip.bat' to include Houdini.	wuestholz	2011-08-23
\|
*	Fixed axiom for Take/Update commuting.	Jason Koenig	2011-07-19
\|
*	Added compilation support for multisets and sequences from arrays.	Jason Koenig	2011-07-15
\|
*	Strengthened axioms for multisets and sequences.	Jason Koenig	2011-07-14
\|
*	Added multiset from sequence axioms, removed array range RHSs. Fixed issue ↵	Jason Koenig	2011-07-13
\| \| \| \|	with duplicate array.Length functions in generated Boogie file.
*	Multiset forming operators added.	Jason Koenig	2011-07-11
\|
*	Partial implementation of multisets.	Jason Koenig	2011-07-11
\|
*	Dafny: Dafny now uses the Euclidean definition of division. (Verifier and ↵	Jason Koenig	2011-07-08
\| \| \| \|	runtime.)
*	Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions	Rustan Leino	2011-06-29
\|
*	Dafny: fixed soundness problem with HeapSucc axiom	Rustan Leino	2011-06-01
\|
*	Dafny: added set comprehension expressions	Rustan Leino	2011-05-18
\|
*	Dafny: To help verifications involving sequences of (boxed) booleans along, ↵	Rustan Leino	2011-05-16
\| \| \| \|	added function $IsCanonicalBoolBox
*	Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵	Rustan Leino	2011-05-11
\| \| \| \|	avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
*	Don't set logic to UFNIA when /useArrayTheory	Michal Moskal	2011-05-09
\|
*	Dafny: added "choose" operator on sets	rustanleino	2011-03-26
\|
*	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
*	Updated PrepareBoogieZip.bat to include BVD and smt2	rustanleino	2011-03-10
\| \| \| \|	Ignore duplicated else functions in models