| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | 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 |
| | | |||
| * | Added further assistance in coming up with decreases clauses in SCCs with ↵ | Rustan Leino | 2014-02-24 |
| | | | | | co-recursive calls. | ||
| * | Refactored code for dealing with SCCs in the call graph. | Rustan Leino | 2014-02-24 |
| | | | | | Fixed bug. | ||
| * | 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) | ||
| * | 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 soundness bug with co-recursive calls: co-recursive calls may now no ↵ |  Rustan Leino | 2013-06-29 |
| | | | | | longer to to functions with ensures clauses | ||
| * | Fixed unsoundness (and also allowed other, sound cases) in the admissability ↵ | Rustan Leino | 2013-06-28 |
| | | | | | checks for co-recursive calls | ||
| * | changed default decreases clause for functions with a reads clause: use the ↵ | Rustan Leino | 2012-10-04 |
| | | | | | reads clause followed by the list of parameters | ||
| * | Dafny: more correct checking of co-inductive productivity |  Unknown | 2012-05-18 |
| | | |||
| * | Dafny: added support for co-recursive calls | Rustan Leino | 2012-05-01 |
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |