debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	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
*	Stop pretty-print from emitting deprecated semi-colons.	qunyanm	2015-03-05
\|
*	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.
*	Set up the same test infrastructure as in Boogie.	wuestholz	2014-05-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.
*	Dafny: updated test suite to new syntax	Jason Koenig	2012-07-30
\|
*	Dafny: fixed some test cases	Jason Koenig	2012-06-28
\|
*	Dafny: make sure assume->assert transformation gives rise to a check	Rustan Leino	2012-02-19
\|
*	Dafny: added syntactic support for ...'s in statements, and started ↵	Unknown	2012-02-18
\| \| \| \|	implementation of refinement transformations thereof
*	Dafny: allow signatures to be omitted on refining functions/methods	Unknown	2012-02-16
\|
*	Dafny: improved error location for violations of function postconditions	Rustan Leino	2012-01-18
\|
*	Dafny: allow a refinement to provide a function/method body if the ↵	Rustan Leino	2012-01-18
\| \| \| \|	function/method being refined didn't have one
*	Dafny: added signature checking to refinement	Rustan Leino	2012-01-17
\|
*	Dafny: allow class-member declarations at top level of any module (not just ↵	Rustan Leino	2012-01-10
\| \| \| \|	the default module); these go into the (new) default class of each module
*	Dafny: added test case for refinement and predicates (and fixed a parsing bug)	Rustan Leino	2012-01-10
\|
*	Dafny: added support for simple superposition refinements	Rustan Leino	2012-01-09
\|
*	Dafny: added assertions in the refinement obligation necessitating that the ↵	kyessenov	2010-07-03
\| \| \| \|	return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call.
*	Dafny: Support class type parameters in refinements. Added another ↵	kyessenov	2010-07-02
\| \| \| \|	regression test -- a sequence refined by a singly linked list.
*	Dafny: added Carrol Morgan's calculator regression test.	kyessenov	2010-07-02