debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Bumped version to 1.7.0, to be released as a binary and on rise4fun.	wuestholz	2013-08-06
\|
*	Removed code for an unreachable case	Rustan Leino	2013-08-06
\|
*	Merge	Rustan Leino	2013-08-06
\|\
* \|	Allow calls to side-effect-free ghost methods from expressions	Rustan Leino	2013-08-06
\| \|
* \|	Merged PredicateExpr and CalcExpr into a single StmtExpr	Rustan Leino	2013-08-06
\| \| \| \| \| \| \| \|	In that process, added a SubstStmt method (and entourage) for substituting into statements
\| *	Updated 'PrepareDafnyZip.bat'.	wuestholz	2013-08-05
\| \|
\| *	DafnyExtension: Use the same version number as Dafny (unfortunately needs to ↵	wuestholz	2013-08-05
\| \| \| \| \| \| \| \|	be updated separately in the vsixmanifests).
* \|	Added hover text ("additional information") in places where co-predicates ↵	Rustan Leino	2013-08-04
\| \| \| \| \| \| \| \|	provide syntactic shorthands
* \|	Allow co-predicates to be wrapped inside bounded existential quantifiers	Rustan Leino	2013-08-04
\| \|
* \|	Added hover text ("additional information") in places where co-methods ↵	Rustan Leino	2013-08-04
\| \| \| \| \| \| \| \|	provide syntactic shorthands
* \|	Unified function/method context heights	Rustan Leino	2013-08-04
\| \|
* \|	Disallow call-graph clusters that mix co-methods / prefix methods with other ↵	Rustan Leino	2013-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	things. Disallow call-graph clusters that mix co-predicates / prefix predicates with other things.
* \|	Set up call-graph to keep track of edges between functions and methods. (To ↵	Rustan Leino	2013-08-04
\| \| \| \| \| \| \| \|	be done: replace InMethodContext with a Function/Method-Height in translator.)
\| *	DafnyExtension: Fixed issue with visual elements being accessed by ↵	wuestholz	2013-08-04
\| \| \| \| \| \| \| \|	non-owning thread.
\| *	DafnyExtension: Did some refactoring and added a description to error states.	wuestholz	2013-08-03
\|/
*	Introduced keywords "lemma" (like a "ghost method", but not allowed to have ↵	Rustan Leino	2013-08-02
\| \| \| \|	a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
*	More and improved CaptureState info	Rustan Leino	2013-08-02
\|
*	Merge adjustments	Rustan Leino	2013-08-02
\|\
* \|	Added activation antecedents for co-predicate / prefix predicate axioms.	Rustan Leino	2013-08-02
\| \|
* \|	Changed the encoding of recursive functions. Previous, three hardcoded ↵	Rustan Leino	2013-08-02
\| \| \| \| \| \| \| \| \| \| \| \|	layers were used: F#2, F, and F#limited. Now, recursive functions take a layer argument, which is specified by Peano numbers. Also, cleaned up and made more consistent the emission of axioms regarding functions.
\| *	DafnyExtension: Fixed a minor issue in the error selection.	wuestholz	2013-08-01
\| \|
\| *	Fixed contract build errors	Rustan Leino	2013-08-01
\| \|
\| *	DafnyExtension: Fixed a minor issue in the error selection.	wuestholz	2013-08-01
\| \|
\| *	DafnyExtension: Made it select the last error state by default when an error ↵	wuestholz	2013-08-01
\| \| \| \| \| \| \| \|	is selected.
\| *	DafnyExtension: Made it display if a variable was updated in a given model ↵	wuestholz	2013-08-01
\| \| \| \| \| \| \| \|	state.
\| *	DafnyExtension: Made it display all variable values from the model.	wuestholz	2013-08-01
\| \|
\| *	DafnyExtension: Increased the font size for the BVD tool window.	wuestholz	2013-07-31
\| \|
\| *	Added support for more fine-grained generation of unique names.	wuestholz	2013-07-31
\| \| \| \| \| \| \| \| \| \|	Creation of unique names is now deferred until translation to Boogie or C#. For Boogie names are unique within a Dafny class member.
\| *	Regenerated Parser after a merge.	Nadia Polikarpova	2013-07-31
\| \|
\| *	Merge	Nadia Polikarpova	2013-07-31
\| \|\
\| * \|	Allowing dangling hints in calculations.	Nadia Polikarpova	2013-07-31
\|/ /
\| *	DafnyExtension: Added support for displaying values from the model as hover ↵	wuestholz	2013-07-30
\| \| \| \| \| \| \| \|	text.
\| *	Add support for hexidecimal numbers.	parno	2013-07-30
\| \|
\| *	Minor change	wuestholz	2013-07-30
\|/
*	Added "co-recursive call" to drop box	Rustan Leino	2013-07-30
\|
*	Simplified the guardedness checking algorithm	Rustan Leino	2013-07-30
\|
*	Co-recursion, now sounder than ever!	Rustan Leino	2013-07-30
\| \| \| \| \| \|	- prefix equality is destructive - co-methods are not allowed to have out-parameters - in an SCC with both co-recursive and recursive calls, the latter are allowed only in non-destructive contexts
*	Fixed issue in the computation of checksums.	wuestholz	2013-07-29
\|
*	Fixed distinction between intra/inter-module calls and refined calls.	Rustan Leino	2013-07-29
\|
*	Added an assert to help the theorem prover out in the RingBuffer.Enqueue method.	Rustan Leino	2013-07-29
\|
*	Merge	Rustan Leino	2013-07-29
\|\
* \|	Make functions and predicates be opaque outside the defining module -- only ↵	Rustan Leino	2013-07-29
\| \| \| \| \| \| \| \|	their specifications (e.g., ensures clauses) are exported.
\| *	DafnyExtension: Make it possible to enable and disable BVD.	wuestholz	2013-07-28
\| \|
\| *	DafnyExtension: Hide the state list and the menu strip in BVD.	wuestholz	2013-07-28
\| \|
\| *	DafnyExtension: Avoid allocating too much space for the error model adornments.	wuestholz	2013-07-28
\| \|
\| *	DafnyExtension: Update the error model when a new error state is selected.	wuestholz	2013-07-28
\| \|
\| *	DafnyExtension: Did some refactoring to integrate the Dafny menu more tightly.	wuestholz	2013-07-28
\| \|
* \|	Added some test cases: theorem about infinite and finite trees.	Rustan Leino	2013-07-27
\| \|
\| *	DafnyExtension: minor change	wuestholz	2013-07-26
\| \|
\| *	DafnyExtension: Did some refactoring and worked towards integrating the ↵	wuestholz	2013-07-26
\| \| \| \| \| \| \| \|	Dafny menu more tightly.