debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ↵	Jason Koenig	2012-07-17
\| \| \| \|	parallel statements.
*	Dafny: fixed a couple of compiler bugs	Unknown	2012-06-14
\|
*	Dafny: Added map comprehensions and updated display syntax	Unknown	2012-05-31
\|
*	Dafny: Added compilation of finite maps	Unknown	2012-05-25
\|
*	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: implemented compilation of parallel statements	Rustan Leino	2011-10-25
\| \| \| \|	Dafny: beefed up resolution of parallel statements
*	Added compilation support for multisets and sequences from arrays.	Jason Koenig	2011-07-15
\|
*	Dafny: Dafny now uses the Euclidean definition of division. (Verifier and ↵	Jason Koenig	2011-07-08
\| \| \| \|	runtime.)
*	Dafny: added set comprehension expressions	Rustan Leino	2011-05-18
\|
*	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
*	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
*	Dafny: Compilation of multi-dimensional arrays	rustanleino	2010-09-21
\|
*	Dafny:	rustanleino	2010-05-21
\| \| \| \| \| \| \|	* Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks
*	Dafny:	rustanleino	2010-05-13
\| \| \| \| \|	* Effectively make all in- and out-parameters of ghost methods ghosts. * Added DafnyRuntime.cs back in, which is needed to run Dafny programs, but which, unfortunately, is currently not being used in the test suite (something we should address)
*	Changed the 'svn:ignore' property of /Binaries such that ALL currently not ↵	mschwerhoff	2010-05-12
\| \| \| \|	svn-added files are ignored. Currently added are only the files that are not generated during the build process (e.g. Makefile, FSharp.Core.dll), hence all files generated during the build process won't be committed.
*	Dafny:	rustanleino	2010-05-06
	* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies) * Added "print" statement (to make running compiled programs more interesting) * Changed name of default class from $default to _default Boogie: * Included "lambda" as a keyword in emacs and latex style files