Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Merged with default. | chmaria | 2012-06-18 | |
| |\ | |/ |/| | ||||
* | | Dafny: cleaned up test scripts a little | Unknown | 2012-06-14 | |
| | | ||||
| * | Dafny: Added tests. | chmaria | 2012-06-12 | |
|/ | ||||
* | Dafny: fixed regression tests | Unknown | 2012-05-29 | |
| | ||||
* | Dafny: Added maps to regression tests. | Unknown | 2012-05-29 | |
| | ||||
* | Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic ↵ | Unknown | 2012-03-05 | |
| | | | | specifications | |||
* | Dafny: fixed bug in compilation of let expressions. | Rustan Leino | 2012-01-26 | |
| | ||||
* | Dafny: allow definitions and uses of parameter-less predicates to go without ↵ | Rustan Leino | 2012-01-10 | |
| | | | | parentheses | |||
* | Merge | Rustan Leino | 2011-11-22 | |
|\ | ||||
| * | Dafny: call C# compiler directly from inside Dafny, and optionally produce a ↵ | Rustan Leino | 2011-11-22 | |
| | | | | | | | | .cs file with the new /spillTargetCode switch | |||
* | | Dafny: Added "type" declaration (syntax: "type X;"), which introduces an ↵ | Rustan Leino | 2011-11-21 | |
|/ | | | | arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated. | |||
* | Dafny: Cleaned up proof of RevConcat in test case | Rustan Leino | 2011-11-08 | |
| | ||||
* | Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to ↵ | Rustan Leino | 2011-11-04 | |
| | | | | a previous lemma | |||
* | Added some Dafny and Boogie test cases, including Turing's factorial ↵ | Rustan Leino | 2011-11-03 | |
| | | | | program, Hoare's classic FIND, and some induction tests for negative integers | |||
* | Dafny induction: | Rustan Leino | 2011-10-29 | |
| | | | | | | | * implemented induction tactic for result-less, non-mutating ghost methods * refine heuristics for determining if a variables is usefully passed to a recursive function * disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy) * added command-line flags /induction and /inductionHeuristic (everything is on by default) | |||
* | Dafny: continued translation of "parallel" statements (Assign and Proof ↵ | Rustan Leino | 2011-10-24 | |
| | | | | | | | forms are mostly there, Call is missing and so is compilation) Dafny: included some test cases for the "parallel" statement Dafny: starting changing old "foreach" statements to the new "parallel" statement | |||
* | Dafny: added translation of Assign case of the parallel statement | Rustan Leino | 2011-10-22 | |
| | | | | Dafny: discovered and fixed bug in no-overlap check of multi-dimensional array update, and changed previously incorrect MatrixFun.dfy test case (the new version is also a more efficient program) | |||
* | Dafny: beautification in one test case, and fixed an Answer file | Rustan Leino | 2011-09-29 | |
| | ||||
* | Dafny: added Flatten example to test suite | Rustan Leino | 2011-09-11 | |
| | ||||
* | Dafny: updated Answer file from recent test additions | Rustan Leino | 2011-08-22 | |
| | ||||
* | Dafny: updated test files (will soon update Answer files as well) | Rustan Leino | 2011-08-22 | |
| | ||||
* | Dafny: Fixed a bug in the printer that led to a stack overflow. | wuestholz | 2011-08-11 | |
| | ||||
* | Jennisys: started to work on synthesizing some methods. So far, only | Aleksandar Milicevic | 2011-08-10 | |
| | | | | | | infrastructural things have been implemented, like handling return parameters, generating different "fresh" spec for methods than for constructors, adding "Valid()" to method preconditions. | |||
* | Dafny: added reverse*reverse=id example to test suite | Rustan Leino | 2011-08-04 | |
| | ||||
* | Dafny: re-ran parser generator to include semicolon-less body-less ↵ | Rustan Leino | 2011-07-26 | |
| | | | | functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366) | |||
* | Merge | Rustan Leino | 2011-07-21 | |
|\ | ||||
* | | Dafny: call previous lemma instead of restating it | Rustan Leino | 2011-07-21 | |
| | | ||||
| * | Fixed regression test failures due to removal of bodiless methods and functions. | Jason Koenig | 2011-07-15 | |
|/ | ||||
* | Dafny: allow constructors only inside classes, removed semi-colons at end of ↵ | Rustan Leino | 2011-07-11 | |
| | | | | body-less functions/methods | |||
* | Dafny: Translate general LHSs for var and := (not yet for call, no ↵ | Rustan Leino | 2011-05-30 | |
| | | | | compilation yet) | |||
* | Merge | Rustan Leino | 2011-05-27 | |
|\ | ||||
| * | Dafny: permanently changed the syntax of "datatype" declarations to what ↵ | Rustan Leino | 2011-05-27 | |
| | | | | | | | | previously was an alternative syntax | |||
| * | Dafny: | Rustan Leino | 2011-05-26 | |
| | | | | | | | | | | | | * fixed ghost/non-ghost story for breaks and returns * changed compilation/translation to always use goto's to implement Dafny's breaks * introduced "break break" statements | |||
* | | Dafny: fixed bug in induction-tactic heuristic (should never pick values ↵ | Rustan Leino | 2011-05-26 | |
| | | | | | | | | whose type is a type parameter) | |||
| * | Dafny: retired the "call" keyword | Rustan Leino | 2011-05-26 | |
| | | ||||
| * | Dafny: | Rustan Leino | 2011-05-21 | |
|/ | | | | | | | | | | * started rewriting parsing of qualified identifiers in expressions * annoyingly, had to introduce AST nodes for concrete syntax * previous syntax for invoking datatype constructors: #List.Cons(h, t) new syntax: List.Cons(h, t) or, if only one datatype has a constructor named Cons: Cons(h, t) * Removed type parameters for datatype constructors from the grammar * Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied) | |||
* | Dafny: added some test cases that use nat | Rustan Leino | 2011-05-16 | |
| | ||||
* | Merge | Rustan Leino | 2011-05-13 | |
|\ | ||||
| * | Dafny: | Rustan Leino | 2011-05-11 | |
| | | | | | | | | | | | | * added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword) * check that arrays are not null when accessed * added dafny1/FindZero.dfy test case | |||
* | | Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵ | Rustan Leino | 2011-05-11 | |
|/ | | | | avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation | |||
* | Dafny: Fix parsing of if-then-else expressions, and don't require ↵ | Rustan Leino | 2011-04-21 | |
| | | | | parentheses around forall/exists expressions | |||
* | Dafny: Alternative (and candidate replacement) syntax for declaring datatypes | Rustan Leino | 2011-04-20 | |
| | | | | Dafny: Additional induction test cases | |||
* | Dafny: added manual proofs for 5 theorems in Rippling.dfy | Rustan Leino | 2011-04-12 | |
| | ||||
* | 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 ↵ | Unknown | 2011-04-05 | |
| | | | | | | | | assignments where RHS is not just an expression | |||
| * | Dafny: fixed bug in induction over integers | Unknown | 2011-04-04 | |
|/ | | | | Dafny: added pow2 example | |||
* | Dafny: | rustanleino | 2011-03-30 | |
| | | | | | * Fixed handling of type parameters in automatic decreases clauses * Added ACL2s Rotate example | |||
* | Dafny: Added support for an initializing call as part of the new-allocation ↵ | rustanleino | 2011-03-27 | |
| | | | | | | | | | | | syntax. What you previously would have written like: c := new C; call c.Init(x, y); you can now write as: c := new C.Init(x, y); | |||
* | Dafny: added "choose" operator on sets | rustanleino | 2011-03-26 | |
| |