| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Codeplex repositories.
|
| |
|
|
|
|
| |
codatatypes would then be sound
Dafny: added special case to allow equality comparison against parameter-less datatype values
|
| | |
|
| |
|
|
| |
body-less functions/methods
|
| |
|
|
| |
previously was an alternative syntax
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
* 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)
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case).
* Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.)
* Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type.
* More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal")
* Add axioms about idempotence of set union and intersection
* The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one
* In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase
* Fixed error in translation of while(*)
|
| |
|
|
| |
of TOP elements; this reduces the need for manually supplied decreases clauses (see the Outer/Inner example in Test/dafny0/Termination.dfy and the Substitute/SubstSeq example in Test/dafny1/Substitution.dfy).
|
| |
|
|
|
| |
* For every loop decreases clause N, generate a free loop invariant N <= N0, where N0 is the value of N just before the loop.
* Added Test/dafny1/KatzManna.dfy, which contains the 3 programs (and their termination annotations) from the Katz and Manna 1975 paper "A closer look at termination" (which benefits from the feature above).
|
| |
|
|
|
|
| |
* Improved design and implementation of SplitExpr
* Fixed some tests in dafny0/Use.dfy
* Added test case (in dafny0/Termination.dfy) to test the recent strengthening of set axioms
|
| |
|
|
| |
clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
|
| |
|
|
|
|
| |
bodies) match expressions.
Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
|
| |
|
|
| |
variables, if they were not already local variables.
|
| |
|
Rustan Leino
Rustan Leino