| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| |\ |
|
| | |
| |
| |
| | |
some trailing whitespace.
|
| | |
| |
| |
| | |
context.
|
| | |
| |
| |
| | |
with duplicate array.Length functions in generated Boogie file.
|
| | | |
|
| |\ \ |
|
| | |/
|/|
| |
| | |
updated regression tests.)
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
method
Dafny: fixed compilation bug with parallel assignment involving a ghost LHS
Dafny: added sequence-to-set conversion if a function's reads clause is used implicitly as the decreases clause
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
compilation yet)
|
| |
|
|
| |
match-case expressions
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
* 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)
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
to UpdateStmt, automatically infer ghosts when local variables are introduced with a call RHS
|
| | |
| |
| |
| |
| |
| | |
parsing as the old VarDecl's with RHS's
To-do: automatically make some variables introduce ghost variables, depending on RHS of initial assignment
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* fixed parsing problem with a block ending a block
* replaced AssignStmt and "call" statements with UpdateStmt's
* fixed some minor printing problems
* changed implementation to check for ghost expressions in a pass separate from ResolveExpr
To-dos:
* compile and translate multi-assignments
* handle non-identifier LHSs of call statements
* change "var" statements in a similar way
* tighten up parsing of LHSs to allow only things like SelectExpr
* code and grammar clean-up to remove unused parts (e.g., "call" grammar productions and the "allowGhostFeatures" parameters)
* include the commented-out precondition of TrAssignment
* check in changes to the test suite
|
| |/
|
|
|
|
|
|
|
|
| |
* 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)
|
| | |
|
| |
|
|
| |
expressions/statements
|
| | |
|
| |
|
|
| |
added function $IsCanonicalBoolBox
|
| |
|
|
| |
for addition other other comprehensions (like set comprehension)
|
| |
|
|
|
|
| |
* 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
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
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
|
| |
|
|
|
|
| |
dictionaries are non-null, which is enforced by the implementation of Dictionary.
Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
|
| |
|
|
|
|
| |
* 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)
|
Rustan Leino
Jason Koenig
Unknown
Unknown