| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
(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.
|
| |\| |
|
| | | |
|
| | | |
|
| |/ |
|
| |
|
|
| |
.cs file with the new /spillTargetCode switch
|
| |
|
|
|
|
|
| |
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
|
| |
|
|
| |
functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)
|
| | |
|
| |
|
|
| |
body-less functions/methods
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
* 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)
|
| |
|
|
| |
avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
|
| |
|
|
| |
assignments where RHS is not just an expression
|
| |
|
|
|
|
|
|
|
|
|
| |
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);
|
| |
|
|
|
|
| |
* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields
|
| | |
|
| |
|
|
|
|
|
|
|
| |
* Set Z3's QI_COST as the sum of "weight" and "generation", not their product. This worked better when setting the :weight of a quantifier (see below).
Dafny:
* Improved axiomatization of sequences; in particular, use an axiom to generate terms that say what the two pieces of a concatenation are
* Two of the (previous) sequence axioms could cause a matching loop, in cases where Z3's arithmetic reasoning does not infer all rational arithmetic equalities during instantiation. The effect of this was apparently not noticed before, perhaps the concatenation/drop properties previously had to be supplied in manual assert statements. But now, with the improved sequence axiomatization (see previous bullet), this effect became remarkably noticeable. To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results.
* Removed several assert lemmas that are no longer needed in Test programs (the test programs now contain only about a handful of such lemmas)
|
| |
|
|
|
| |
* changed implementation of Test/VSI-Benchmarks/b4.dfy to be more interesting (and, in particular, different from the specification)
* reformatted Test/VSI-Benchmarks/b3.dfy
|
| |
|
|
| |
clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
|
| |
|
|
|
|
|
| |
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
|
| |
|
|
|
| |
Previously, a "use" function was one whose definition was applied only in limited ways, namely when the function was uttered in a program (possibly in a "use" statement). Now, recursive functions are always limited, unless declared with the new modifier "unlimited". Non-recursive functions are always unlimited. Also new is that only function calls within the same SCC of the call graph use the limited form of the callee.
The "use" modifier is no longer supported. The "use" statement is still supported, now for both limited and unlimited functions; but it's probably better and easier to just explicitly mention a function in an assertion, if needed.
|
| |
|
|
|
| |
* Recoded frame axioms to be more goal directed
* Added Main test driver to Test/VSI-Benchmarks/b2.dfy
|
| |
|
|
|
|
|
|
| |
* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies)
* Added "print" statement (to make running compiled programs more interesting)
* Changed name of default class from $default to _default
Boogie:
* Included "lambda" as a keyword in emacs and latex style files
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Added modules with imports. These can be used to deal with termination checks without going into method/function implementations. Imports must be acyclic.
* Added a default module. It contains all classes/datatypes defined outside the lexical scope of any other module.
* Added a default class. It contains all class members defined outside the lexical scope of any module and class. This means that one can write small Dafny programs without any mention of a "class"!
* Revised scheme for termination metrics. Inter-module calls are allowed iff they follow the import relation. Intra-module calls where the callee is in another strongly connected component of the call graph are always allowed. Intra-module calls in the same strongly connected component are verified to terminate via decreases clauses.
* Removed previous hack that allowed methods with no decreases clauses not to be subjected to termination checking.
* Removed or simplified decreases clauses in test suite, where possible.
* Fixed error in Test/VSI-Benchmarks/b1.dfy
|
| |
|
|
|
|
| |
missing)
Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
|
| | |
|
| |
|
|
|
| |
* Modifies clause checking is now done with each update, instead of at the end of the method. Not only does this improve error messages, but on some examples, it gives a dramatic speed-up (2x) in proving time.
* bugfix: range expressions of foreach statements were previously ignored during Translation
|
| |
|
|
|
|
| |
* Enforce ghost vs. non-ghost separation
* Allow ghost parameters and ghost locals
* Functions are ghost, but allow the non-ghost "function method"
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* If no decreases clause is given, the decreases clause defaults to the set of objects denoted by the reads clause, which was the previous Dafny behavior
* Made Dafny check loops for termination by default. Previously, this was done only if the loop had a decreases clause. To indicate that a loop is to be checked only for partial correctness, Dafny now allows "decreases *".
* Allow "reads *" to say that the function may read anything at all (sound, but not very useful)
* Adjusted frame axioms of functions to speak of allocated objects more liberally; and also added antecedents about the heaps being well-formed and the parameters being allocated
* Added some previously omitted well-definedness checks.
* Fixed some bugs in the resolver that caused some type errors not to be reported
* Added some messages to go with some (previously rather opaquely reported) errors
* Fixed some test cases that previously had ordered conjuncts incorrectly to prove termination and reads checks (such checks were previously omitted)
* Beefed up Test/dafny0/SchorrWaite.dfy to use datatypes to specify that no garbage gets marked. The full-functional total-correctness verification of this Schorr-Waite method now takes about 3.2 seconds.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
and seq.
Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).
Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.
Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.
Added a space in the pretty printing of Boogie coercion expressions.
|
| |
|
|
| |
variables, if they were not already local variables.
|
| |
|
|
|
|
|
| |
"!(x in S)".
Changed Dafny test files to use the new operator.
Included the file b8.dfy into the VSI-Benchmarks test harness.
|
| |
|
|
| |
uncomment a couple of the desired loop invariants.)
|
| |
|
wuestholz
Unknown
Unknown
Rustan Leino
Unknown