| Commit message (Expand) | Author | Age |
|---|
| * | 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 induction: | Rustan Leino | 2011-10-29 |
| * | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s... | Rustan Leino | 2011-10-26 |
| * | Dafny: changed triggers (which are never really used, anyhow) from having a s... | Rustan Leino | 2011-10-21 |
| * | Dafny: Added some assertions. |  wuestholz | 2011-09-23 |
| * | Dafny: Added a 'Checked' configuration and fixed some runtime assertion viola... | wuestholz | 2011-09-23 |
| * | 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 |
| * | | Multiset forming operators added. | Jason Koenig | 2011-07-11 |
| * | | Merge | Jason Koenig | 2011-07-11 |
| |\ \ |
|
| * | | | Added s[..] syntax in anticipation of sequence forming operation. (also updat... | Jason Koenig | 2011-07-11 |
| | |/
|/| |
|
| | * | Partial implementation of multisets. | Jason Koenig | 2011-07-11 |
| |/ |
|
| * | Refactor. Renamed update statement field and removed unused field in AST. | Jason Koenig | 2011-06-30 |
| * | Made Receiver mutable, as this cannot be linked properly by the parser. | 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 |
| * | Added loop modifies clause syntax. | Jason Koenig | 2011-06-23 |
| * | Dafny: added implicit datatype query fields and datatype destructor fields | Rustan Leino | 2011-06-05 |
| * | 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: permanently changed the syntax of "datatype" declarations to what prev... | 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: 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 |
| * | Dafny: added optional range expressions to logical quantifiers, preparing for... | Rustan Leino | 2011-05-15 |
| * | Dafny: include source location for array types supplied in input | Rustan Leino | 2011-04-22 |
| * | Dafny: Fix parsing of if-then-else expressions, and don't require parentheses... | Rustan Leino | 2011-04-21 |
| * | Dafny: added type "nat" | Rustan Leino | 2011-04-19 |
| * | Dafny: Allow field selections and array-element selection as LHSs of assignme... |  Unknown | 2011-04-05 |
| * | Dafny: refactoring to soon support more general assignment statements | rustanleino | 2011-03-29 |
| * | Dafny: Added support for an initializing call as part of the new-allocation s... | rustanleino | 2011-03-27 |
| * | Dafny: added "choose" operator on sets | rustanleino | 2011-03-26 |
| * | Dafny: improved and corrected physical/ghost distinction | rustanleino | 2011-03-26 |
| * | Dafny: compile quantifiers | rustanleino | 2011-03-26 |
| * | Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic... | mikebarnett | 2011-03-10 |
| * | Dafny: Improved scheme for splitting expressions. Also, report each split i... | rustanleino | 2011-02-19 |
| * | Dafny: | rustanleino | 2011-02-17 |
| * | Dafny: added ensures clauses to functions | rustanleino | 2011-02-02 |
Rustan Leino
wuestholz
Unknown