Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | Dafny: added Snapshotable Trees example | 2011-09-11 | ||
| | | ||||
* | | Dafny: added Flatten example to test suite | 2011-09-11 | ||
|/ | ||||
* | Dafny: fixed parsing bug with "!in" | 2011-09-08 | ||
| | | | | | Dafny: fixed translation bug with missing match cases (where the constructor has some parameters) Dafny: fixed translation bug where the program had forward references to members of a datatype | |||
* | Dafny: updated Answer file from recent test additions | 2011-08-22 | ||
| | ||||
* | Dafny: updated test files (will soon update Answer files as well) | 2011-08-22 | ||
| | ||||
* | Merge | 2011-08-18 | ||
|\ | ||||
* | | Dafny: fixed bug in looking at the arguments of the :induction attribute | 2011-08-18 | ||
| | | ||||
| * | Dafny: Fixed a bug in the printer that led to a stack overflow. | 2011-08-11 | ||
| | | ||||
| * | Jennisys: started to work on synthesizing some methods. So far, only | 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 | 2011-08-04 | ||
| | ||||
* | Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative) | 2011-08-03 | ||
| | ||||
* | Dafny: re-ran parser generator to include semicolon-less body-less ↵ | 2011-07-26 | ||
| | | | | functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366) | |||
* | Merge | 2011-07-21 | ||
|\ | ||||
* | | Dafny: call previous lemma instead of restating it | 2011-07-21 | ||
| | | ||||
| * | Fixed regression test failures due to removal of bodiless methods and functions. | 2011-07-15 | ||
| | | ||||
| * | Fixed failing regression tests. | 2011-07-14 | ||
| | | ||||
| * | Merge | 2011-07-14 | ||
| |\ | |/ |/| | ||||
| * | Added multiset from sequence axioms, removed array range RHSs. Fixed issue ↵ | 2011-07-13 | ||
| | | | | | | | | with duplicate array.Length functions in generated Boogie file. | |||
* | | Merge | 2011-07-11 | ||
|\ \ | ||||
* | | | Dafny: allow constructors only inside classes, removed semi-colons at end of ↵ | 2011-07-11 | ||
| | | | | | | | | | | | | body-less functions/methods | |||
| | * | Added s[..] syntax in anticipation of sequence forming operation. (also ↵ | 2011-07-11 | ||
| |/ | | | | | | | updated regression tests.) | |||
| * | Dafny: Added Euclidean regression test (Verifier only). | 2011-07-08 | ||
|/ | ||||
* | Dafny: Fixed bug in call statements where mutability of out parameters was ↵ | 2011-07-06 | ||
| | | | | | | not checked. Added regression test. | |||
* | Dafny: Updated regression tests to include chaining disjoint operators. | 2011-07-05 | ||
| | ||||
* | Added additional test case to modifies on loops tests. | 2011-06-29 | ||
| | ||||
* | Removed tab characters. | 2011-06-29 | ||
| | ||||
* | Merge | 2011-06-29 | ||
|\ | ||||
* | | Added regression tests for new return statements with parameters. | 2011-06-29 | ||
| | | ||||
| * | Merge | 2011-06-29 | ||
| |\ | |/ |/| | ||||
| * | Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions | 2011-06-29 | ||
| | | ||||
* | | Added regression test file LoopModifies.dfy. | 2011-06-29 | ||
| | | ||||
* | | Added regression test for loop modifies clauses. | 2011-06-28 | ||
| | | ||||
* | | Changed regression test answer for dafny0 to reflect new error messages. | 2011-06-28 | ||
|/ | ||||
* | Dafny: added implicit datatype query fields and datatype destructor fields | 2011-06-05 | ||
| | ||||
* | Dafny: translate call statements with fancy LHSs | 2011-05-31 | ||
| | ||||
* | Dafny: Translate general LHSs for var and := (not yet for call, no ↵ | 2011-05-30 | ||
| | | | | compilation yet) | |||
* | Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;" | 2011-05-28 | ||
| | ||||
* | Dafny: added constructors | 2011-05-28 | ||
| | ||||
* | Merge | 2011-05-27 | ||
|\ | ||||
* | | Dafny: | 2011-05-27 | ||
| | | | | | | | | | | * fixed bug in allowing ghost out-parameters of ghost methods * added test case for verifying calls of the form MyClass.M(...) | |||
| * | Merge | 2011-05-27 | ||
| |\ | |/ |/| | ||||
* | | Dafny: permanently changed the syntax of "datatype" declarations to what ↵ | 2011-05-27 | ||
| | | | | | | | | previously was an alternative syntax | |||
* | | Dafny: retired "use" statements | 2011-05-27 | ||
| | | ||||
* | | Dafny: added chaining operators | 2011-05-27 | ||
| | | ||||
* | | Dafny: | 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 ↵ | 2011-05-26 | ||
| | | | | | | | | whose type is a type parameter) | |||
| * | Dafny: fixed bug (ill-formed Boogie) in translation of "foreach" for sequences | 2011-05-26 | ||
| | | ||||
* | | Dafny: retired the "call" keyword | 2011-05-26 | ||
| | | ||||
* | | Dafny: allow class names to be used when referring to static functions (and, ↵ | 2011-05-21 | ||
| | | | | | | | | soon, methods), and test cases for new name resolution rules | |||
* | | Dafny: | 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) |