| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.
|
| |
|
|
| |
Found by enabling auto-generated triggers and looking for failing tests
|
| |
|
|
|
| |
Window's batch doesn't recognize ";" as a command separator; lit has a
workaround for that, bu it's just as simple to do the right thing on our side.
|
| |
|
|
| |
of proving the existence check of let-such-that and assign-such-that
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
|
| |
|
|
|
|
|
| |
been added to the scope.
Resolve the attributes of local variables.
Don't resolve attributes of PredicateStmt's more than once.
|
| | |
|
| |
|
|
|
|
| |
Renamed "default constructor" to "anonymous constructor" (since there's really nothing "default" about it).
If the type of literal "null" is unresolved, make the type "object".
The need to translate unresolved proxies is now assumed to be gone.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* The reads clause now needs to be self framing.
* The requires clause now needs to be framed by the reads clause.
* There are one-shot lambdas, with a single arrow, but they will probably be
removed.
* There is a {:heapQuantifier} attribute to quantifiers, but they will
probably be removed.
* Add smart handling of type variables
* Add < and > for datatype & type parameter
|
| |
|
|
| |
Also add a test case for the different display expressions.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
in compiling assign-such-that statements
Added run-time support for printing sets, multisets, maps, and sequences
|
| |
|
|
|
|
|
| |
set/multiset/sequence/map display expressions
Run SmallTests.dfy and LetExpr.dfy only once in the test suite
Fixed some translation bugs (and a pretty-printing bug) for map display expressions
|
| | |
|
| |
|
|
| |
around the bound variables optional.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
-allocated(x) removed, as really only useful in old(...)
-old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).
|
| |
|
|
| |
(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.
|
| |
|
|
| |
check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
(assert, ensures, modifies, decreases, invariant).
|
| |
|
|
| |
(see bug report Issue 10214 on codeplex)
|
| |
|
|
| |
wellformedness checks).
|
| |
|
|
| |
statement)
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
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)
|
| | |
|
| |
|
|
| |
for addition other other comprehensions (like set comprehension)
|
| |
|
|
|
|
|
|
|
|
|
| |
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);
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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(*)
|
| |
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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
|
Clément Pit--Claudel
Rustan Leino
Dan Rosén
Rustan Leino
Unknown