diff options
author | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-22 17:19:36 -0700 |
---|---|---|
committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-22 17:19:36 -0700 |
commit | 964be96ce093e85355091ba447f2e71d035b0556 (patch) | |
tree | da9df955aaf6a9230d51dd739b3ce7c34afcf0b7 /Source/Dafny/Dafny.atg | |
parent | 61831b969894e7bac6c8c1212835a5aade18de4d (diff) |
Dafny: allow "assume ..." as a refining statement (provided it replaces an "assume E")
Diffstat (limited to 'Source/Dafny/Dafny.atg')
-rw-r--r-- | Source/Dafny/Dafny.atg | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 3000d348..4b9e0c27 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1036,11 +1036,11 @@ CaseStatement<out MatchCaseStmt/*!*/ c> /*------------------------------------------------------------------------*/
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
- Expression/*!*/ e = null; Attributes attrs = null;
+ Expression e = null; Attributes attrs = null;
.)
- "assert" (. x = t; s = null;.)
+ "assert" (. x = t; .)
{ IF(IsAttribute()) Attribute<ref attrs> }
- ( Expression<out e>
+ ( Expression<out e>
| "..."
)
";"
@@ -1052,9 +1052,21 @@ AssertStmt<out Statement/*!*/ s> .)
.
AssumeStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
+ Expression e = null; Attributes attrs = null;
+ .)
"assume" (. x = t; .)
- Expression<out e> ";" (. s = new AssumeStmt(x, e); .)
+ { IF(IsAttribute()) Attribute<ref attrs> }
+ ( Expression<out e>
+ | "..."
+ )
+ (. if (e == null) {
+ s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ } else {
+ s = new AssumeStmt(x, e, attrs);
+ }
+ .)
+ ";"
.
PrintStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
|