| Commit message (Expand) | Author | Age |
* | Dafny: added support for co-recursive calls | Rustan Leino | 2012-05-01 |
* | Dafny: rudimentary translation into Boogie of co-inductive datatypes | Unknown | 2012-04-25 |
* | Dafny: fixed bug (missing Boogie cast) in translation of induction over gener... | Unknown | 2012-04-20 |
* | Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr; | Unknown | 2012-03-15 |
* | Dafny: fixed build error | Rustan Leino | 2012-03-09 |
* | Dafny: added ghost modules (the meaning is simply that such a module will not... | Rustan Leino | 2012-03-07 |
* | Dafny: fixed well-formedness checking of LET expressions to allow the RHS to ... | Rustan Leino | 2012-02-29 |
* | Dafny: make sure assume->assert transformation gives rise to a check | Rustan Leino | 2012-02-19 |
* | Dafny: improved error location for violations of function postconditions | Rustan Leino | 2012-01-18 |
* | Dafny: allow parallel statements with an empty list of bound variables | Rustan Leino | 2012-01-17 |
* | Dafny: parallel statements: | Rustan Leino | 2012-01-17 |
* | Dafny: Recheck specifications that contain refined (extended) predicates, eve... | Rustan Leino | 2012-01-16 |
* | Dafny: handle refinement of nested tokens that come from SpliExpr (still need... | Rustan Leino | 2012-01-12 |
* | Dafny: make full predicate definitions available only inside a module (outsid... | Rustan Leino | 2012-01-11 |
* | Dafny: fixed bugs in contract types, and a code bug that caused a contract to... | Rustan Leino | 2012-01-10 |
* | Dafny: some bug fixes | Rustan Leino | 2012-01-10 |
* | Dafny: allow definitions and uses of parameter-less predicates to go without ... | Rustan Leino | 2012-01-10 |
* | Dafny: changed translation to be sensitive to refinement inheritance; this fe... | Rustan Leino | 2012-01-09 |
* | Dafny: fully qualify (with module names) names of types in the translation in... | Rustan Leino | 2012-01-05 |
* | Dafny: Start of new refinement features -- clean out old ones | Rustan Leino | 2012-01-04 |
* | Dafny: for a datatype with just one constructor, don't check (but do assume) ... | Rustan Leino | 2011-12-19 |
* | Dafny: Added support for attributes on various specification constructs (asse... | wuestholz | 2011-12-07 |
* | Dafny: fix bug in translation of (the splitting of) if-then-else expressions ... | Rustan Leino | 2011-12-10 |
* | Merge | Rustan Leino | 2011-12-07 |
|\ |
|
* | | Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable well... | wuestholz | 2011-12-07 |
| * | Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbi... | Rustan Leino | 2011-11-21 |
|/ |
|
* | Dafny: fixed bad Code Contracts | Rustan Leino | 2011-11-16 |
* | Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine... | Rustan Leino | 2011-11-15 |
* | Dafny: added let expressions (syntax: "var x := E0; E1") | Rustan Leino | 2011-11-14 |
* | Dafny: implemented the wellformedness check that datatype destructors are onl... | Rustan Leino | 2011-11-11 |
* | Dafny: added assert/assume expressions | Rustan Leino | 2011-11-09 |
* | Dafny: moved definition of class.array into prelude, anticipating writing axi... | Rustan Leino | 2011-11-09 |
* | Dafny: fixed part of a type-inference issue with datatypes and the < operator... | Rustan Leino | 2011-11-09 |
* | Dafny: fixed bug in reads checking of array-to-sequence conversions | Rustan Leino | 2011-11-08 |
* | Dafny: added a new /inductionHeuristic option | Rustan Leino | 2011-11-04 |
* | Dafny: added options to make Induction Heuristic apply to array index express... | Rustan Leino | 2011-11-04 |
* | Dafny induction: | Rustan Leino | 2011-10-29 |
* | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s... | Rustan Leino | 2011-10-26 |
* | Dafny: removed support for assigning to an array-range (that is, an assignmen... | Rustan Leino | 2011-10-26 |
* | BVD: fixed two basic but damning problems with the Dafny provider, and elided... | Rustan Leino | 2011-10-26 |
* | Dafny: check subrange restriction in parallel Assign statement | Rustan Leino | 2011-10-24 |
* | Dafny: continued translation of "parallel" statements (Assign and Proof forms... | Rustan Leino | 2011-10-24 |
* | Dafny: added translation of Assign case of the parallel statement | Rustan Leino | 2011-10-22 |
* | Dafny: changed triggers (which are never really used, anyhow) from having a s... | Rustan Leino | 2011-10-21 |
* | Dafny: fixed performance-buggy translation of exists, and also added some oth... | Rustan Leino | 2011-10-19 |
* | Dafny: fixed bug in translator when LHS of a call was an array element or a nat | Rustan Leino | 2011-09-30 |
* | Dafny: Added a 'Checked' configuration and fixed some runtime assertion viola... | wuestholz | 2011-09-23 |
* | Dafny: Fixed an assertion violation in the "Checked" configuration. | wuestholz | 2011-09-20 |
* | Dafny: Added support for attributes on methods and constructors. | wuestholz | 2011-09-16 |
* | Dafny: fixed parsing bug with "!in" | Rustan Leino | 2011-09-08 |