debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
...
*	Fixed bug in co axioms.	Unknown	2013-01-18
\| \| \| \|	Automatic induction on copredicate's _k argument.
*	Added axiom that relates larger and smaller prefix equalities.	Unknown	2013-01-18
\|
*	Proper support for inlining codatatype equalities	Rustan Leino	2013-01-18
\|
*	Removed the syntactic form copredicate #-form with the implicit argument.	Rustan Leino	2013-01-16
\| \| \| \|	Added syntactic support for codatatype #-form equalities.
*	Encode codatatype equalities by predefined copredicates, including their ↵	Rustan Leino	2013-01-15
\| \| \| \|	prefix versions
*	Support for copredicates and prefix predicates in comethods.	Rustan Leino	2012-12-04
\| \| \| \| \| \|	(Missing from the co support are (prefix) equalities of codatatypes, various restrictions on the use of co/prefix-predicates, and tactic support for applying the (prefix-)induction automatically.)
*	Added canCall as alternative antecedents to frame axioms.	Unknown	2012-11-12
\|
*	Merge	Rustan Leino	2012-10-30
\|\
* \|	Rename _reverifyPost to $_reverifyPost, so that it doesn't show up in BVD	Rustan Leino	2012-10-30
\| \| \| \| \| \| \| \| \| \|	Remove some duplicated hover text in DafnyExtension Enable Code Contracts in the build
\| *	Removed the encoding that was used to distinguish datatype values by their type	Unknown	2012-10-30
\|/ \| \| \| \| \| \| \|	parameters. Previously, this encoding was used in places like the antecedents of function frame axioms. However, not all datatype constructors had this information available, so it seems better (for now) to drop this information altogether. When a full Boogie-term encoding of Dafny types is done, then it would be appropriate revisit this issue.
*	renamed "abstract module" to "module facade"	Rustan Leino	2012-10-22
\| \| \| \|	renamed "ghost module" to "abstract module", adding a keyword "abstract"
*	allow a refinement to introduce "return" statements, at the price of ↵	Rustan Leino	2012-10-22
\| \| \| \| \| \|	re-verifying the postcondition at that time let refined classes inherit attributes
*	Included "all cases of a datatype" property for method in-parameters (see ↵	Unknown	2012-10-17
\| \| \| \|	http://boogie.codeplex.com/discussions/397616).
*	Added some axioms to try to recover boxed data. In particular, any element ↵	Unknown	2012-10-17
\| \| \| \|	'x' of a set in the encoding satisfies Box(Unbox(x))==x. The soundness and performance of the axiomatization are dicey, so the axioms are made available only to method in-parameters.
*	Added/fixed decreases clauses that use multisets or maps.	Unknown	2012-10-16
\|
*	Change the encoding of proof certificates to make the two levels explicit	Unknown	2012-10-12
\| \| \| \|	Restrict what conclusions comethods are allowed to have
*	Removed the old (though automatic) coinduction principle	Rustan Leino	2012-10-11
\|
*	New feature:	Rustan Leino	2012-10-11
\| \| \| \| \| \| \|	* Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with) Code restructuring: * New set of Boogie procedure stubs generated for each other * Start of improvements around TrSplitExpr
*	More free antecedents when proving well-formedness of iterator specs	Rustan Leino	2012-10-04
\|
*	changed default decreases clause for functions with a reads clause: use the ↵	Rustan Leino	2012-10-04
\| \| \| \|	reads clause followed by the list of parameters
*	Put all sources under \Source directory	Rustan Leino	2012-10-04