| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
the assign-such-that statement instead. For example: x :| x in S;
|
| | |
|
| |
|
|
| |
around the bound variables optional.
|
| |
|
|
| |
check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
|
| | |
|
| |
|
|
|
|
|
| |
- 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)
|
| |
|
|
|
|
|
| |
* 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)
|
|
|
Dafny: beefed up resolution of parallel statements
|
wuestholz
Unknown
Rustan Leino