| Commit message (Expand) | Author | Age |
* | Dafny: Added support for attributes on various specification constructs (asse... | wuestholz | 2011-12-07 |
* | Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbi... | Rustan Leino | 2011-11-21 |
* | DafnyExtension: fixed build problems | 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: allow assert/assume expressions in more places | Rustan Leino | 2011-11-09 |
* | Dafny: added assert/assume expressions | Rustan Leino | 2011-11-09 |
* | Dafny: fixed part of a type-inference issue with datatypes and the < operator... | Rustan Leino | 2011-11-09 |
* | Dafny induction: | Rustan Leino | 2011-10-29 |
* | Dafny: allow attributes on function/method declarations to refer to the (in- ... | Rustan Leino | 2011-10-26 |
* | 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 |
* | Dafny: implemented compilation of parallel statements | Rustan Leino | 2011-10-25 |
* | Dafny: check subrange restriction in parallel Assign statement | 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: improved a resolution error message, and fixed a crash in the resolver | Rustan Leino | 2011-09-29 |
* | Dafny: Added a 'Checked' configuration and fixed some runtime assertion viola... | wuestholz | 2011-09-23 |
* | Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative) | Rustan Leino | 2011-08-03 |
* | Merge | Jason Koenig | 2011-07-15 |
|\ |
|
| * | Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed so... | wuestholz | 2011-07-15 |
* | | Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi... | Jason Koenig | 2011-07-13 |
* | | Multiset forming operators added. | Jason Koenig | 2011-07-11 |
* | | Partial implementation of multisets. | Jason Koenig | 2011-07-11 |
|/ |
|
* | Dafny: Fixed bug in call statements where mutability of out parameters was no... | Jason Koenig | 2011-07-06 |
* | Refactored update statement resolution to its own method. | Jason Koenig | 2011-06-30 |
* | Refactor. Renamed update statement field and removed unused field in AST. | Jason Koenig | 2011-06-30 |
* | Stable implementation of return statements with parameters. | Jason Koenig | 2011-06-29 |
* | Initial implementation of return statments with parameters. | Jason Koenig | 2011-06-29 |
* | Initial modifies on loops implementation. Still some errors remaining. | Jason Koenig | 2011-06-28 |
* | Dafny: added implicit datatype query fields and datatype destructor fields | Rustan Leino | 2011-06-05 |
* | Dafny: translate call statements with fancy LHSs | Rustan Leino | 2011-05-31 |
* | Dafny: Translate general LHSs for var and := (not yet for call, no compilatio... | Rustan Leino | 2011-05-30 |
* | Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;" | Rustan Leino | 2011-05-28 |
* | Dafny: added constructors | Rustan Leino | 2011-05-28 |
* | Dafny: fixed parsing bug that prevented all expressions from occurring in mat... | Rustan Leino | 2011-05-27 |
* | Dafny: retired "use" statements | Rustan Leino | 2011-05-27 |
* | Dafny: added chaining operators | Rustan Leino | 2011-05-27 |
* | Dafny: | Rustan Leino | 2011-05-26 |
* | Dafny implementation: removed always-true "allowGhostFeatures" parameter | Rustan Leino | 2011-05-26 |
* | Dafny: retired the "call" keyword | Rustan Leino | 2011-05-26 |
* | Dafny: cleaned up parser, moved foreach statement from AssignStmt<> parsing t... | Rustan Leino | 2011-05-25 |
* | Dafny: changed local "var" introductions to use new VarDeclStmt instead of pa... | Rustan Leino | 2011-05-24 |
* | Dafny: | Rustan Leino | 2011-05-24 |
* | Dafny: refactored code into separate method ResolveIdentifierSequence and all... | Rustan Leino | 2011-05-22 |
* | Dafny: allow class names to be used when referring to static functions (and, ... | Rustan Leino | 2011-05-21 |
* | Dafny: | Rustan Leino | 2011-05-21 |
* | Dafny: added alternative statement and alternative-loop statement | Rustan Leino | 2011-05-19 |
* | Dafny: let verifier, not the resolver, check for missing cases in match expre... | Rustan Leino | 2011-05-19 |
* | Dafny: added set comprehension expressions | Rustan Leino | 2011-05-18 |