debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Additional test case for inductive predicates	leino	2015-05-07
\|
*	Added "inductive lemma" methods	leino	2015-05-07
\|
*	Added inductive predicates	leino	2015-05-06
\|
*	Fixed bug in tuples	leino	2015-04-24
\|
*	Include axioms about $Is and $IsAlloc for traits	leino	2015-04-07
\|
*	Support calls to static trait methods/functions via the class	leino	2015-04-07
\|
*	Revised look-up and compilation of inherited trait members (static ↵	leino	2015-04-07
\| \| \| \|	functions/methods don't work yet)
*	Fixed compilation of static members in traits	leino	2015-04-05
\|
*	Fixed some bugs in override axioms (but still missing support for classes ↵	leino	2015-04-05
\| \| \| \| \| \| \|	with type parameters). Resolve ClassDecl.TraitsTyp as types. Moved declaration of TraitParent and NoTraitAtAll to prelude.
*	Whitespace deltas in test files (in particular, removing tabs and adjusting ↵	leino	2015-04-03
\| \| \| \|	some indentation)
*	Added test cases and fixes for overrides termination checks	leino	2015-04-03
\| \| \| \|	Removed syntactic presence checks for specifications--these will be checked semantically by the verifier
*	Merge	leino	2015-03-13
\|\
* \|	Allow let-such-that expression to be compiled, provided that they provably ↵	leino	2015-03-13
\| \| \| \| \| \| \| \|	have a unique value
\| *	Beefed up collection axioms (in particular, for maps) to improve the chance ↵	Rustan Leino	2015-03-10
\|/ \| \| \|	of proving the existence check of let-such-that and assign-such-that
*	Fixed bug in resolution of illegal programs.	leino	2015-03-10
\| \| \| \|	Fixed comments in some test cases.
*	This changeset changes the default visibility of a function/predicate body ↵	leino	2015-03-09
\| \| \| \| \| \| \| \| \| \|	outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'. Semantics of 'protected': * The definition (i.e., body) of a 'protected' function is not visible outside the defining module * The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions. * In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected' * The 'protected' status of a function must be preserved in refinement modules
*	Added 'protected' keyword (syntax)	leino	2015-03-07
\|
*	Stop pretty-print from emitting deprecated semi-colons.	qunyanm	2015-03-05
\|
*	Add imap display/update expressions	chrishaw	2015-02-27
\|
*	Add imap type, which is like map but may have have infinite size	chrishaw	2015-02-26
\|
*	Generate unique IDs hierarchically, to reduce changes to IDs when the ↵	leino	2015-01-28
\| \| \| \|	program is modified (to help with fine-grained caching)
*	Did some refactoring to improve the name generation.	wuestholz	2015-01-27
\|
*	Did some refactoring to improve the name generation.	wuestholz	2015-01-27
\|
*	Assume type properties of values that are created by a havoc assignment. ↵	Rustan Leino	2015-01-27
\| \| \| \| \| \|	Such assignments are part of assign-such-that statements, and thus this also fixes Issue 52.
*	Fixed an encoding bug for newtypes (this fixes Issue #50)	Rustan Leino	2015-01-27
\|
*	Minor change to a test case	wuestholz	2015-01-27
\|
*	Updated test output after change in Boogie.	wuestholz	2015-01-24
\|
*	Make sure to check that subrange types are not used as type parameters	leino	2015-01-23
\|
*	Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, ↵	leino	2015-01-23
\| \| \| \| \| \| \|	so use the new name resolution machinery that handles modules and type parameters Included some inadvertently left-out test cases in dafny0/Modules0.dfy Fixed comparable-types tests
*	When ambiguous references all resolve to the same declaration, don't complain	leino	2015-01-09
\|
*	Fixed bug in opaque functions with type parameters	leino	2015-01-07
\|
*	Merge	leino	2015-01-03
\|\
* \|	Fixed resolution of method calls with explicit type parameters.	leino	2015-01-02
\| \| \| \| \| \| \| \|	Finished refactoring of the recent name segments changes.
\| *	Updated test output after change in Boogie.	wuestholz	2014-12-28
\| \|
* \|	Language change: All functions and methods declared lexically outside any ↵	leino	2014-12-12
\|/ \| \| \| \| \| \| \| \| \|	class are now automatically static, and fields are no longer allowed to be declared there. Stated differently, all heap state must now be declared inside an explicitly declared class, and functions and methods declared outside any class can be viewed as belonging to the module. The motivating benefit of this change is to no longer need the 'static' keyword when declaring a module of functions and methods.
*	Fixed two crashes in resolver	leino	2014-12-10
\| \| \| \|	Corrected merge
*	Merge	leino	2014-12-09
\|\
* \|	Allow user-specified type parameters	leino	2014-12-09
\| \|
\| *	minor change on a test.	Reza Ahmadi	2014-12-03
\| \|
\| *	added multiple trait inheritance.	Reza Ahmadi	2014-12-03
\| \| \| \| \| \| \| \|	- a class can now extend more than one traits
* \|	Fixed some issues with assignments in refinements, both soundness bugs in ↵	leino	2014-12-02
\| \| \| \| \| \| \| \|	previous version and changes necessitated by recent parsing refactoring
* \|	Snapshot, to be continued	leino	2014-12-02
\| \|
\| *	removing one unnessessary check in the cloner	Reza Ahmadi	2014-12-02
\| \|
\| *	- fixed a bug in merging fields that come from a parent trait	Reza Ahmadi	2014-12-02
\| \| \| \| \| \| \| \|	- added one more test
\| *	Updated test output after change in Boogie.	wuestholz	2014-11-25
\|/
*	Merge	leino	2014-11-19
\|\
* \|	Fixed bug where resolution was overly restrictive with ghost variables ↵	leino	2014-11-19
\| \| \| \| \| \| \| \| \| \| \| \|	appearing in reads clauses. Fixed bug in the checking of reads subset for field frame targets ("back ticks")
\| *	Updated test output after change in Boogie.	wuestholz	2014-11-16
\|/
*	Bug fixes in the compilation of forall statements.	leino	2014-11-13
\|
*	Merge	leino	2014-11-06
\|\