| Commit message (Expand) | Author | Age |
* | Dafny: bug fix in generating IsCanonicalBoolBox predicates | Rustan Leino | 2011-06-21 |
* | Dafny: better error message when "decreases *" is attempted on a function or ... | Rustan Leino | 2011-06-20 |
* | Dafny: fixed accidental omission of CaptureState after some assignments | Rustan Leino | 2011-06-16 |
* | Dafny: added implicit datatype query fields and datatype destructor fields | Rustan Leino | 2011-06-05 |
* | Dafny: compiler fixes | Rustan Leino | 2011-05-31 |
* | Dafny: compile multi-assignments, compile calls with more general LHSs | Rustan Leino | 2011-05-31 |
* | 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 |
* | Merge | Rustan Leino | 2011-05-27 |
|\ |
|
* | | Dafny: fixed parsing bug that prevented all expressions from occurring in mat... | Rustan Leino | 2011-05-27 |
| * | Merge | Rustan Leino | 2011-05-27 |
| |\ |
|
| * | | Dafny: | Rustan Leino | 2011-05-27 |
* | | | Dafny: fixed compilation bug that produced an extraneous comma in the target ... | Rustan Leino | 2011-05-27 |
| |/
|/| |
|
* | | Merge | Rustan Leino | 2011-05-27 |
|\| |
|
| * | 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: fixed bug in induction-tactic heuristic (should never pick values whos... | Rustan Leino | 2011-05-26 |
* | | Dafny: fixed bug (ill-formed Boogie) in translation of "foreach" for sequences | 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 |
* | Dafny: To help verifications involving sequences of (boxed) booleans along, a... | Rustan Leino | 2011-05-16 |
* | Dafny: added optional range expressions to logical quantifiers, preparing for... | Rustan Leino | 2011-05-15 |
* | Dafny: fixed bug in quantifier bounds discovery | Rustan Leino | 2011-05-14 |
* | Dafny: fixed typo in parser code | Rustan Leino | 2011-05-13 |
* | Merge | Rustan Leino | 2011-05-13 |
|\ |
|
* | | Dafny: fixed bugs in resolution of multi-dimensional arrays | Rustan Leino | 2011-05-12 |
* | | Dafny: forbid "decreases *" on ghost loops | Rustan Leino | 2011-05-12 |
| * | Dafny: | Rustan Leino | 2011-05-11 |
* | | Dafny: fixed compilation bugs, added @-signs in front of identifiers to avoid... | Rustan Leino | 2011-05-11 |
| * | 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: Alternative (and candidate replacement) syntax for declaring datatypes | Rustan Leino | 2011-04-20 |
* | Dafny: added type "nat" | Rustan Leino | 2011-04-19 |
* | Dafny: don't require parentheses in syntax of "choose" statements | Rustan Leino | 2011-04-05 |
* | branch merge | Rustan Leino | 2011-04-05 |
|\ |
|
* | | Dafny: Allow field selections and array-element selection as LHSs of assignme... | Unknown | 2011-04-05 |
| * | Dafny: fixed bug in induction over integers | Unknown | 2011-04-04 |
|/ |
|