| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
| |
generic datatypes instantiated with datatypes
|
| |
|
| |
|
|
|
|
|
|
|
| |
not be compiled)
Dafny: improved :autocontracts heuristic for detecting "simple query method"
Dafny: fixed some bugs
|
|
|
|
| |
be used
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
- removed the awkward restriction that method postconditions cannot use old/fresh if there's no modifies clause and no out-parameters; instead, implemented parallel statements to handle these cases
- also allow old/fresh in ensures clauses of parallel statements
- allow TypeRhs and choose expressions in Call/Proof parallel statements
- disallow calls to non-ghost methods in parallel statements (since those may do "print" statements and we don't want to allow those to take place in parallel; besides, the compiler wants to omit the parallel statement altogether and could not do so if there were print statements)
|
|
|
|
| |
even if they are contained inside a split expression. Superposition is thought to be sound.
|
|
|
|
| |
need to deal with unsplit expressions, like quantifiers)
|
|
|
|
| |
(outside is just an implication: the predicate implies the body known so far)
|
|
|
|
| |
to fail
|
| |
|
|
|
|
| |
parentheses
|
|
|
|
| |
feature is now functional, provided the refining module does not add or change anything
|
|
|
|
|
|
|
| |
into Boogie
Dafny: started cloning of refined classes
Dafny: added /rprint switch to print the (syntax of the) resolved Dafny program
|
| |
|
|
|
|
| |
that destructors are applied only to those values constructed by that one-and-only constructor
|
|
|
|
| |
(assert, ensures, modifies, decreases, invariant).
|
|
|
|
| |
(see bug report Issue 10214 on codeplex)
|
|\ |
|
| |
| |
| |
| | |
wellformedness checks).
|
|/
|
|
| |
arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
|
| |
|
|
|
|
| |
CommandLineOptions to separate the options that belong to these 3 tools.
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
only applied to values created by the corresponding constructor
Dafny: implement ghost destructors properly
|
| |
|
|
|
|
| |
axioms that use it
|
|
|
|
|
|
| |
operator on datatypes
Dafny: allow the well-formedness check of a function's specification to know that the function, on the current arguments, returns a value of the declared result type
|
| |
|
| |
|
|
|
|
| |
expressions
|
|
|
|
|
|
|
| |
* 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)
|
|
|
|
| |
statement)
|
|
|
|
| |
assignment statement where the LHS has the form a[lo..hi])
|
|
|
|
| |
elided some temporary variables
|
|
|
|
|
| |
Dafny: verify parallel Call statement
Dafny: fixed some bugs: handle all cases of comprehension expressions in resolver's UsesSpecFeatures, check target of method calls to be non-null (duh!)
|
|
|
|
|
|
|
| |
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)
|
|
|
|
|
|
|
| |
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)
|
|
|
|
| |
other features in SplitExpr (such as induction on existential quantifiers)
|
| |
|
|
|
|
| |
violations.
|
| |
|
| |
|
|
|
|
|
| |
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
|