debian-dafny - Debian packaging for Dafny

	Commit message (Expand)	Author	Age
*	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
\| *	Dafny: removed div/mod axioms, since Boogie now interprets div/mod	Unknown	2012-09-28
\| *	Boogie: new syntax for integer division and modulus: use div and mod instead ...	boehmes	2012-09-27
\|/
*	Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ...	Unknown	2012-09-12
*	Dafny: Implemented abstract modules	Jason Koenig	2012-06-26
*	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 finite maps	Unknown	2012-05-25
*	Dafny: fully qualify (with module names) names of types in the translation in...	Rustan Leino	2012-01-05
*	Dafny: moved definition of class.array into prelude, anticipating writing axi...	Rustan Leino	2011-11-09
*	Dafny: removed support for assigning to an array-range (that is, an assignmen...	Rustan Leino	2011-10-26
*	Fixed axiom for Take/Update commuting.	Jason Koenig	2011-07-19
*	Strengthened axioms for multisets and sequences.	Jason Koenig	2011-07-14
*	Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi...	Jason Koenig	2011-07-13
*	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 run...	Jason Koenig	2011-07-08
*	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: To help verifications involving sequences of (boxed) booleans along, a...	Rustan Leino	2011-05-16
*	Dafny: added "choose" operator on sets	rustanleino	2011-03-26
*	Dafny:	rustanleino	2011-02-17
*	Dafny: replaced the user-defined $ite function with Boogie's built-in if-then...	rustanleino	2011-02-03
*	Dafny: removed CEV instrumentation	rustanleino	2011-02-03
*	Dafny: a partial first crack at a Dafny model-viewer provider, including capt...	rustanleino	2010-11-01
*	Dafny:	rustanleino	2010-09-17
*	Dafny:	rustanleino	2010-09-14
*	Dafny: added inlined functions making reads and updates of the heap explicit	sboehme	2010-08-27
*	Dafny: Axiom about inverting a set union operation, similar to the recent on...	rustanleino	2010-07-09
*	Boogie:	rustanleino	2010-06-22
*	Dafny:	rustanleino	2010-06-18
*	Dafny:	rustanleino	2010-05-21
*	Dafny:	rustanleino	2010-05-06
*	Dafny:	rustanleino	2010-03-31
*	Dafny: Ensures that function axioms are not being used while their consisten...	rustanleino	2010-03-19
*	Dafny: Added if-then-else expressions (replacing and extending the previous b...	rustanleino	2010-02-04
*	Dafny: updated to reflect Boogie's new parsing of function arguments	rustanleino	2010-01-07
*	Added resolution and translation of algebraic datatypes and (in function bodi...	rustanleino	2009-11-20
*	Start (some parsing and resolution) of adding algebraic datatypes to Dafny.	rustanleino	2009-11-08
*	Added a sequence update expression in Dafny.	rustanleino	2009-11-06
*	Redesigned the encoding of Dafny generics, including the built-in types set a...	rustanleino	2009-11-06
*	Applied patch 4316, which fixes an unsoundness in the axiomatization of seque...	rustanleino	2009-11-05
*	Dafny: Added axioms for division and modulo.	rustanleino	2009-09-15
*	Dafny:	rustanleino	2009-09-14
*	Full (?) support in Dafny for Counterexample Visualizer predicates.	rustanleino	2009-08-19
*	Incorporated Counterexample Visualizer (CEV) information in the generated Boo...	rustanleino	2009-08-15
*	Initial set of files.	mikebarnett	2009-07-15