debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Renamed identifiers for increased geopolitical appeal	Rustan Leino	2016-02-08
\|
*	In method and iterator specifications, inline top-level predicates (except	leino	2015-10-24
\| \| \| \|	protected predicated in cross-module calls) like in other places.
*	Implement {:nowarn}, clarify some messages, and add a few tests	Clément Pit--Claudel	2015-08-28
\|
*	Add a small test from the IronClad notebook	Clément Pit--Claudel	2015-08-27
\|
*	Further relax the loop detection conditions	Clément Pit--Claudel	2015-08-27
\| \| \| \| \|	Mismatches are now allowed up to expressions not involving any of the bound variables of the quantifier under inspection.
*	Small fix: there is no loop in (forall x :: Q(x) && Q(0))	Clément Pit--Claudel	2015-08-27
\| \| \| \|	Again, spotted by Chris :)
*	Improve the redundancy detection algorithm used while constructing sets of terms	Clément Pit--Claudel	2015-08-26
\| \| \| \| \| \| \| \|	Based on an issue noted by Chris with redundancy removal resuls being dependent on the order of the terms. Interestingly, one of our tests already had an instance of that problem. Also fix the issue with nested quantifiers getting redundant triggers.
*	s/loops with/may loop with/	Clément Pit--Claudel	2015-08-23
\|
*	Make quantifier splitting a two step process	Clément Pit--Claudel	2015-08-23
\| \| \| \|	This fixes a bug that affected Monad.dfy
*	Improve error reporting for split quantifiers	Clément Pit--Claudel	2015-08-23
\|
*	Allow MultiSelectExpr as quantifier heads	Clément Pit--Claudel	2015-08-23
\|
*	Look at the full quantifier to find loops, not just the term.	Clément Pit--Claudel	2015-08-22
\|
*	Make `old` a special case for trigger generation.	Clément Pit--Claudel	2015-08-21
\| \| \| \| \| \|	Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and old(f(x)). This has a number of implications; see the new tests files for more information.
*	Rephrase the message about triggers being rejected because they are too strong	Clément Pit--Claudel	2015-08-21
\|
*	Adjust WF checks to use unsplit quantifiers.	Clément Pit--Claudel	2015-08-21
\| \| \| \| \| \| \| \| \| \| \| \| \|	The logic about split quantifiers is that Boogie (and z3) should never realize that there was an unsplit quantifier. The WF check code does not produce a quantifier, at least in it's checking part; thus, it should use original quantifier. This fixes a problem in VerifyThis2015/Problem2.dfy with a null check, and a problem spotted by Chris, made into a test case saved in triggers/wf-checks-use-the-original-quantifier.dfy. The issue boiled down to being able to verify (forall x :: x != null && x.a == 0). Of course, the assumption that WF checks produce for a quantifier is a quantifier, so it uses the split expression.
*	Add tests for display expressions used as triggers	Clément Pit--Claudel	2015-08-21
\|
*	Add /printTooltips to trigger tests	Clément Pit--Claudel	2015-08-21
\|
*	Fix a typo	Clément Pit--Claudel	2015-08-20
\|
*	Implement the SelectTrigger method, removing redundant triggers.	Clément Pit--Claudel	2015-08-20
\| \| \| \| \| \| \| \| \|	The idea is that we define an partial order on triggers (which may contain multiple terms), and find all the maximal elements. The algorithm as implemented is rather inefficient; in particular, is does not look at the structure of the graph of the relation (thus is does many redundant comparisons). See triggers/useless-triggers-are-removed.dfy for an example where such a filter is useful.
*	Add unit tests for trigger-related error messages	Clément Pit--Claudel	2015-08-20
\|
*	Simplify error reporting in the trigger generator to get cleaner messages	Clément Pit--Claudel	2015-08-20
\|
*	Add a test to show how trigger splitting balances the downsides of loop ↵	Clément Pit--Claudel	2015-08-20
\| \| \| \|	detection
*	Add tests for quantifier splitting and trigger generation	Clément Pit--Claudel	2015-08-19