| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
keyword is parsed but ignored.
|
| |
|
|
|
| |
-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).
|
| |
|
|
| |
parallel syntax, other minor fixes
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
| |
(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".
|
| |
|
|
| |
them (for now, this is supported only in type expressions and "new" allocations, not in places where the type name is used to qualify some other type member)
|
| |
|
|
| |
limited)
|
| | |
|
| |
|
|
|
|
|
| |
handle generic datatypes correctly)
Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code)
Dafny: added "codatatype" declaration (syntax only for now)
|
| | |
|
| |
|
|
|
|
|
| |
not be compiled)
Dafny: improved :autocontracts heuristic for detecting "simple query method"
Dafny: fixed some bugs
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
(assert, ensures, modifies, decreases, invariant).
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
| |
arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
|
| |
|
|
|
| |
Dafny: firmed up semantics of assert/assume expressions (the condition is now good for all program control paths that pass through the expression)
Dafny: various implementation clean-ups
|
| |
|
|
| |
statement)
|
| |
|
|
|
|
|
| |
special syntactic form to being just an attribute
Dafny: added "parallel" statement (so far, only parsing and resolving)
Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them)
|
| |
|
|
|
| |
Dafny: fixed translation bug with missing match cases (where the constructor has some parameters)
Dafny: fixed translation bug where the program had forward references to members of a datatype
|
| |
|
|
| |
functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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
|
| | |
|
| | |
|
| |
|
|
| |
match-case expressions
|
| |
|
|
| |
previously was an alternative syntax
|
| | |
|
| | |
|
| |
|
|
| |
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)
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
parentheses around forall/exists expressions
|
| |
|
|
| |
Dafny: Additional induction test cases
|
Jason Koenig
Rustan Leino
Unknown
Unknown