| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
|
|
| |
* implemented induction tactic for result-less, non-mutating ghost methods
* refine heuristics for determining if a variables is usefully passed to a recursive function
* disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy)
* added command-line flags /induction and /inductionHeuristic (everything is on by default)
|
| |
|
|
|
|
|
| |
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
|
| |
|
|
| |
Dafny: discovered and fixed bug in no-overlap check of multi-dimensional array update, and changed previously incorrect MatrixFun.dfy test case (the new version is also a more efficient program)
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
infrastructural things have been implemented, like handling return parameters,
generating different "fresh" spec for methods than for constructors,
adding "Valid()" to method preconditions.
|
| | |
|
| |
|
|
| |
functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
|
| |
body-less functions/methods
|
| |
|
|
| |
compilation yet)
|
| |\ |
|
| | |
| |
| |
| | |
previously was an alternative syntax
|
| | |
| |
| |
| |
| |
| | |
* fixed ghost/non-ghost story for breaks and returns
* changed compilation/translation to always use goto's to implement Dafny's breaks
* introduced "break break" statements
|
| | |
| |
| |
| | |
whose type is a type parameter)
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
| |
* 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)
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
* added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword)
* check that arrays are not null when accessed
* added dafny1/FindZero.dfy test case
|
| |/
|
|
| |
avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
|
| |
|
|
| |
parentheses around forall/exists expressions
|
| |
|
|
| |
Dafny: Additional induction test cases
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
assignments where RHS is not just an expression
|
| |/
|
|
| |
Dafny: added pow2 example
|
| |
|
|
|
| |
* Fixed handling of type parameters in automatic decreases clauses
* Added ACL2s Rotate example
|
| |
|
|
|
|
|
|
|
|
|
| |
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);
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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
|
| |
|
|
| |
and) verifiable
|
| |
|
|
|
|
| |
* Support for induction over more than 1 variable
* Added many of the Rippling induction benchmarks
* Fixed bug in case handling
|
| | |
|
| |
|
|
|
|
| |
* Add support for an {:induction} attribute on universal quantifiers over one bound variable. It causes the universally quantified formulas to be proved by induction.
* For a user-defined function F, introduce not just F and F#limited, but also F#2 (which sits "above" F, just as F sits "above" F#limited)
* In base case of SplitExpr, make use of F#2 functions (unless already inside an inlined predicate)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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).
|
| |
|
|
| |
rep axiom
|
| | |
|
| | |
|
Rustan Leino
wuestholz
Unknown
Unknown