diff options
author | 2012-01-17 15:58:11 -0800 | |
---|---|---|
committer | 2012-01-17 15:58:11 -0800 | |
commit | 560941a5db825d549b52462ecf0c81be19689aa2 (patch) | |
tree | b006b2cfaae9201606c33f85a7bea0b8cc0b9a0d /Source/Dafny/Compiler.cs | |
parent | b623a942161bd66b3a0fbef90c92ad4350fdebda (diff) |
Dafny: parallel statements:
- 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)
Diffstat (limited to 'Source/Dafny/Compiler.cs')
0 files changed, 0 insertions, 0 deletions