| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
into Boogie
Dafny: started cloning of refined classes
Dafny: added /rprint switch to print the (syntax of the) resolved Dafny program
|
|
|
|
| |
method as a good candidate for inlining (supported in .NET 4.5)
|
|
|
|
| |
not with a substitution)
|
|
|
|
| |
axioms that use it
|
|
|
|
| |
assignment statement where the LHS has the form a[lo..hi])
|
|
|
|
| |
Dafny: beefed up resolution of parallel statements
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
with duplicate array.Length functions in generated Boogie file.
|
| |
|
| |
|
|
|
|
| |
runtime.)
|
| |
|
| |
|
| |
|
|
|
|
| |
added function $IsCanonicalBoolBox
|
|
|
|
| |
avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
|
| |
|
| |
|
|
|
|
|
|
| |
Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction
Dafny: split expressions when proving function postconditions
Boogie and BVD: updated copyright year ranges
|
|
|
|
| |
Ignore duplicated else functions in models
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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(*)
|
|
|
|
|
| |
Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT.
Add default Z3 options when using Z3.
|
| |
|
| |
|
| |
|
|
|
|
| |
if-then-else expression
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
files generated by Coco/R.
This was done to support sharing of the Coco/R .frame files with Spec#.
|
|
|
|
| |
captureState mark-ups in the Boogie code generated from Dafny
|
|
|
|
|
|
|
| |
* Also copy CodeContractExtender in PrepareBoogieZip.bat
* Added some comments and a new program in Test/textbook
* Included refinement keywords in Chalice emacs mode
* Used assignment instead of spec statement in DuplicatesVideo.chalice
|
| |
|
|
|
|
|
|
| |
* 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
|
|
|
|
|
|
|
|
| |
* 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
|
| |
|
|
|
|
| |
input).
|
| |
|
|
|
|
| |
svn-ignoring some build artifacts
|
|
|
|
| |
added in manually.
|
| |
|
|
|
|
| |
ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.
|
|
|
|
|
|
|
|
|
| |
* 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)
|
|
|
|
|
|
| |
* Added some more set axioms that go "inside out" for union and set differences (UnionOne already had such an axiom)
* Fixed bug to, once again, allow multiple .dfy files on the command line (with the effect of them being merged into one program)
* Fixed bug in translation of reads/modifies clauses that mention sequences
|