debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
...
* \|	Allow let-such-that expression to be compiled, provided that they provably ↵	leino	2015-03-13
\| \| \| \| \| \| \| \|	have a unique value
\| *	Allow trigger annotations in more statements and expressions	chrishaw	2015-03-11
\| \|
\| *	Remove unneeded reference from DafnyExtension.csproj (accidentally added by ↵	chrishaw	2015-03-11
\| \| \| \| \| \| \| \|	my previous checkin)
\| *	Add DafnyOptions.txt, and have the Dafny Visual Studio extension read ↵	chrishaw	2015-03-11
\| \| \| \| \| \| \| \|	command-line options from DafnyOptions.txt during initialization. DafnyOptions.txt gets built into the VSIX file and is installed as part of the Dafny Visual Studio extension.
\| *	Merge	qunyanm	2015-03-11
\| \|\
\| * \|	Fix issue #54 and #57. Resolve a formal's type before creating a substitute.	qunyanm	2015-03-11
\| \| \|
\| \| *	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.
* \|	Removed some old and unused functions	leino	2015-03-09
\| \|
* \|	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
\|/
*	Fix issue #60	qunyanm	2015-03-06
\|
*	Stop pretty-print from emitting deprecated semi-colons.	qunyanm	2015-03-05
\|
*	Fixed issue #59.	wuestholz	2015-03-03
\|
*	Add imap display/update expressions	chrishaw	2015-02-27
\|
*	Removed Util/VS2010 folder, which has been superseded by DafnyExtension ↵	Rustan Leino	2015-02-27
\| \| \| \|	years ago
*	Add imap keyword to VS/emacs/vim/latex files	chrishaw	2015-02-26
\|
*	Add imap type, which is like map but may have have infinite size	chrishaw	2015-02-26
\|
*	Add an explicit trigger so that Z3 doesn't choose an overly generous trigger ↵	Bryan Parno	2015-02-09
\| \| \| \|	on SeqIndex
*	Make allowGlobals a bit more generous	Bryan Parno	2015-02-09
\|
*	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-28
\|
*	Did some refactoring to improve the name generation.	wuestholz	2015-01-28
\|
*	Did some refactoring to improve the name generation.	wuestholz	2015-01-27
\|
*	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
\|
*	DafnyExtension: Made it use the more advanced on-demand re-verification by ↵	wuestholz	2015-01-26
\| \| \| \|	default.
*	Updated test output after change in Boogie.	wuestholz	2015-01-24
\|
*	Minor change to grammar to avoid missing token	wuestholz	2015-01-24
\|
*	Make sure to check that subrange types are not used as type parameters	leino	2015-01-23
\|
*	Merge	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
\| *	Merge	Bryan Parno	2015-01-13
\| \|\
\| \| *	Minor change due to a change in Boogie	wuestholz	2015-01-13
\| \|/ \|/\|
* \|	When ambiguous references all resolve to the same declaration, don't complain	leino	2015-01-09
\| \|
\| *	Check the AllowGlobals flag in one additional location to avoid a contract ↵	Bryan Parno	2015-01-08
\|/ \| \| \|	failure
*	Added command-line switch /allowGlobals to simplify transition from language ↵	leino	2015-01-07
\| \| \| \|	changes introduced in changeset c56031307ac1
*	Bumped the version number to 1.9.3.20107	leino	2015-01-07
\|
*	Fixed bug in opaque functions with type parameters	leino	2015-01-07
\|
*	Added lemmas that make verification go through faster and more reliably	leino	2015-01-05
\|
*	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
\| \|
\| *	Minor change	wuestholz	2014-12-26
\| \|
\| *	When in DafnyCC mode, ignore termination checking	Bryan Parno	2014-12-16
\| \|
* \|	Fixed bug in /compile:3, when Main is explicitly given as a static method	leino	2014-12-12
\| \|
* \|	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.