summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Dafny: datatype constructors can be accessed across module boundaries.Gravatar Jason Koenig2012-07-06
|
* Dafny: fixed a crash in datatype argument resolutionGravatar Jason Koenig2012-07-05
|
* Dafny: Fixed bug in autocontracts where the post resolver was run even if ↵Gravatar Jason Koenig2012-07-05
| | | | there were resolution errors.
* Dafny: disallow importing ghost modules into physical ones.Gravatar Jason Koenig2012-07-05
|
* Dafny: added static members of _default to the module level scope, at low ↵Gravatar Jason Koenig2012-07-03
| | | | priority.
* Dafny: added support for nested abstract modules, fixed some translation issuesGravatar Jason Koenig2012-07-03
|
* Dafny: re-added field non-uniqueness (was accidentally reverted by a bad merge)Gravatar Jason Koenig2012-07-02
|
* MergeGravatar Jason Koenig2012-07-02
|\
| * Dafny: reinstated autocontractsGravatar Jason Koenig2012-07-02
|/
* Dafny: updated contracts to allow null parent (of the default module)Gravatar Rustan Leino2012-06-29
|
* Dafny: fixed up test suite (temporarily removed autocontract tests)Gravatar Jason Koenig2012-06-28
|
* Dafny: fixed some test casesGravatar Jason Koenig2012-06-28
|
* Dafny: fixed bug with translation of class._System.object;Gravatar Jason Koenig2012-06-28
|
* Dafny: MergeGravatar Jason Koenig2012-06-27
|\
* | Dafny: fixed bug in which _module scope declarations were not verified.Gravatar Jason Koenig2012-06-27
| |
* | Dafny: Fixed module bugsGravatar Jason Koenig2012-06-27
| |
| * Undo bad merge.Gravatar afd2012-06-27
| |
* | Dafny: Implemented abstract modulesGravatar Jason Koenig2012-06-26
| |
| * MergeGravatar Unknown2012-06-25
| |\
| | * Dafny: now, equality-support determination and checking feels ripe; so, ↵Gravatar Rustan Leino2012-06-22
| | | | | | | | | | | | | | | | | | codatatypes would then be sound Dafny: added special case to allow equality comparison against parameter-less datatype values
| | * MergeGravatar Unknown2012-06-22
| | |\
| | * | Dafny: mark code for equality-support determination tentativeGravatar Unknown2012-06-22
| | | |
| | * | Dafny: equality-support test cases. This is just a snapshot--some things ↵Gravatar Unknown2012-06-22
| | | | | | | | | | | | | | | | still to be fixed up.
| | * | Dafny: added contracts to IRewriter methodsGravatar Unknown2012-06-22
| | | |
| | * | Dafny: allow "assume ..." as a refining statement (provided it replaces an ↵Gravatar Unknown2012-06-22
| | | | | | | | | | | | | | | | "assume E")
| | * | Dafny: deal with equality-support issues in refinementsGravatar Unknown2012-06-22
| | | | | | | | | | | | | | | | Dafny: a small amount of refactoring and bug fixes
| | | * Dafny: Fixed bug in CompilerizeName.Gravatar chmaria2012-06-22
| | | |
| | | * Dafny: fixed two contractsGravatar Rustan Leino2012-06-22
| | | |
| | * | Dafny: Since it's no longer true that all types support equality at run-time ↵Gravatar Unknown2012-06-21
| | |/ | | | | | | | | | (in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.
| * | MergeGravatar Unknown2012-06-21
| |\|
| | * MergeGravatar Unknown2012-06-19
| | |\
| | * | Dafny: improved refinement features; added staged version of the proof of ↵Gravatar Unknown2012-06-19
| | | | | | | | | | | | | | | | the Schorr-Waite algorithm (the staging features, as well as the newly added comments, make the verification much more digestible)
* | | | Dafny: disallow declare identifiers starting with underscore (_)Gravatar Jason Koenig2012-06-19
| | | | | | | | | | | | | | | | | | | | | | | | It is still possible to reference names containing an underscore, but it is not possible to make a variable, method, class, bound variable, type, or module name beginning with one.
* | | | Dafny: Added nested modulesGravatar Jason Koenig2012-06-19
| |_|/ |/| |
| * | Merge with dafny_runtime_checkingGravatar Unknown2012-06-18
| |\ \
| | * \ Merged with default.Gravatar chmaria2012-06-18
| | |\ \ | |_|/ / |/| | |
| | * | Dafny: Added CC translation of postconditions.Gravatar chmaria2012-06-18
| | | |
* | | | Dafny: fixed parsing bug.Gravatar Jason Koenig2012-06-15
| |_|/ |/| |
* | | Dafny: in compiler, respect C#'s different scoping rules and lack of support ↵Gravatar Unknown2012-06-14
| | | | | | | | | | | | for special characters in identifiers
* | | MergeGravatar Unknown2012-06-14
|\| |
* | | Dafny: fixed a couple of compiler bugsGravatar Unknown2012-06-14
| | |
* | | Dafny: cleaned up test scripts a littleGravatar Unknown2012-06-14
| | |
| * | MergeGravatar Jason Koenig2012-06-13
| |\ \ | |/ / |/| |
| * | Dafny: allow parallel assignments to assign to the same LHS if the RHS match.Gravatar Jason Koenig2012-06-13
| | |
* | | MergeGravatar Unknown2012-06-13
|\| |
* | | Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to ↵Gravatar Unknown2012-06-13
| | | | | | | | | | | | check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
| * | Dafny: liberalized equality to work when the types could possibly be the sameGravatar Jason Koenig2012-06-13
| | | | | | | | | | | | (i.e. a != b is allowed when a: array<int> and b: array<T>)
* | | Dafny: added another version of the majority finding algorithm to the test suiteGravatar Unknown2012-06-12
|/ /
* | Dafny: beefed up allocation axioms for boxes stored in fieldsGravatar Unknown2012-06-12
| |
| * Dafny: Added tests.Gravatar chmaria2012-06-12
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 10:20:01 +0000