| Commit message (Expand) | Author | Age |
* | 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: Test case for sequence of boxed booleans | Rustan Leino | 2011-05-16 |
* | Dafny: added some test cases that use nat | Rustan Leino | 2011-05-16 |
* | Dafny: added optional range expressions to logical quantifiers, preparing for... | Rustan Leino | 2011-05-15 |
* | Merge | Rustan Leino | 2011-05-13 |
|\ |
|
* | | Boogie: added features to help with modular verification. In particular, defi... | Rustan Leino | 2011-05-13 |
* | | Cleaner version of ghost loop termination example. | Unknown | 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 |
|/ |
|
* | Merge with 1038 | Rustan Leino | 2011-04-22 |
|\ |
|
| * | Changed label checking for goto targets in StmtList so that they can be any l... | qadeer | 2011-04-21 |
* | | 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 |
* | Automated merge with https://hg01.codeplex.com/boogie | Rustan Leino | 2011-04-16 |
|\ |
|
* \ | merge | Unknown | 2011-04-14 |
|\ \ |
|
* | | | added reachability information to the VC and used that to support arbitrary a... | Unknown | 2011-04-14 |
| * | | Dafny: added manual proofs for 5 theorems in Rippling.dfy | Rustan Leino | 2011-04-12 |
|/ / |
|
| * | Jennisys: First cut of injectivity analysis | Rustan Leino | 2011-04-11 |
|/ |
|
* | Jennisys: Allow model members to occur in any order | Rustan Leino | 2011-04-07 |
* | Jennisys: Refined parsing of expressions, frames, and routine bodies | Rustan Leino | 2011-04-07 |
* | Jennisys: Improved parsing by using operator binding powers | Rustan Leino | 2011-04-07 |
* | Jennisys: Parse and print | Rustan Leino | 2011-04-07 |
* | 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 |
|/ |
|
* | Dafny: | rustanleino | 2011-03-30 |
* | Dafny: Added support for an initializing call as part of the new-allocation s... | rustanleino | 2011-03-27 |
* | Reflect effect of Celebrity.dfy change in previous check-in | 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 |
* | Dafny: Fixed typo in P16 of Rippling benchmarks, which now makes it (true and... | rustanleino | 2011-03-07 |
* | Dafny: | rustanleino | 2011-03-06 |
* | Dafny: Added heuristic for when to turn on the induction tactic | rustanleino | 2011-03-05 |
* | Dafny: | rustanleino | 2011-03-04 |
* | Dafny: support for nested match expressions | rustanleino | 2011-03-01 |
* | Updates to Answer files from recent changes | rustanleino | 2011-03-01 |
* | Add tests for -z3multipleErrors from Shuvendu. | MichalMoskal | 2011-02-23 |
* | Add workaround for cmd race | MichalMoskal | 2011-02-23 |
* | Dafny: Improved scheme for splitting expressions. Also, report each split i... | rustanleino | 2011-02-19 |
* | Don't run test21 with the untyped Z3, as this is no longer going to be available | MichalMoskal | 2011-02-18 |
* | Run dafny and boogie tests by default | MichalMoskal | 2011-02-18 |