| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
* Added internal support for multi-dimensional arrays (but not all surface syntax is there yet)
* Removed unused variables from Dafny.atg
Boogie and Dafny:
* Improved error message for postcondition violations
|
| |
|
|
| |
as output variables of the extracted procedure.
|
| | |
|
| | |
|
| |
|
|
| |
TypeToString() instead. Add test for /typeEncoding:m.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
|
| | |
|
| |
|
|
| |
input).
|
| |
|
|
| |
locally
|
| |
|
|
| |
for better performance on VCs that are heavy on bitvector arithmetic
|
| |
|
|
| |
test for Boogie and a single test for Dafny, just to check for grievous runtime errors in the code. (In my porting, I work with code that, in some cases, is not tested until the 3rd or 4th regression test. These 2 test files should make use of that more obscure code and alert me to my errors quickly, rather than making me wait through a full regression cycle.)
|
| |
|
|
| |
assertions with "if"s to handle errors gently and add cycle detection check.
|
| |
|
|
| |
ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.
|
| |
|
|
| |
/stratifiedInline:1.
|
| |
|
|
|
| |
* changed rule about scoping of out-parameters
* added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
|
| | |
|
| |
|
|
| |
return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call.
|
| |
|
|
| |
regression test -- a sequence refined by a singly linked list.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
* 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).
|
| |
|
|
|
|
| |
having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories.
Lots of code changes to compensate for the new frame files.
|
| |
|
|
|
|
|
|
|
| |
* 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)
|
| |
|
|
|
|
| |
* 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
|
| |
|
|
|
| |
* 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)
|
| |
|
|
| |
function calls
|
| | |
|
| |
|
|
|
|
|
|
|
| |
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
|
| |
|
|
|
|
| |
* Fixed bug in translation of well-formedness conditions
* Added Test/dafny0/Celebrity.dfy
* Added a harness to Test/vacid0/Composite.dfy
|
| | |
|
| |
|
|
| |
their ranks)
|
| |
|
|
|
|
|
| |
* 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
|
| |
|
|
|
|
|
|
|
|
| |
* Added support for polymorphism in lambda expressions
* Little clean-up here and there
* Added 'then' keyword to emacs and latex modes
Dafny:
* Added support for fine-grained framing, using the back-tick syntax from Region Logic
* Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses
|
| |
|
|
|
| |
* Effectively make all in- and out-parameters of ghost methods ghosts.
* Added DafnyRuntime.cs back in, which is needed to run Dafny programs, but which, unfortunately, is currently not being used in the test suite (something we should address)
|
| |
|
|
|
| |
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
|
| |
|
|
| |
/lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.
|
| |
|
|
| |
parens instead, when needed!).
|
| |
|
|
|
|
|
| |
* Added match statements (in addition to the previous match expressions)
* Added missing axiom about boxes and datatypes
* Improved axioms for datatype rank comparisons
* Added test cases with mutual-recursion termination challenges
|
| |
|
|
| |
consistency is being checked.
|
| |
|
|
|
| |
* Allow "decreases *" only for loops.
* Cosmetic changes in SchorrWaite.dfy
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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
|
| |
|
|
|
| |
* Beginning of module implementation
* Changed "class" modifier (for functions and methods) to "static"
|
| |
|
|
|
|
| |
missing)
Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
|
rustanleino