diff options
| author |  Rustan Leino <unknown> | 2014-04-04 10:11:10 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-04 10:11:10 -0700 |
| commit | 0abbaee631e42479bba3cf98cb9a41fdf0f9358d (patch) | |
| tree | f9886c2f1ecd889739954b78e54f5ef977180818 /Source/Dafny/DafnyAst.cs | |
| parent | d6efe85276f21ab3ea2b04d7e6b3c2bfb1acd22e (diff) | |
Support the transition from "modify Frame;" to "modify Frame { Body }" by refinement.
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 51449440..1fc2d787 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3860,6 +3860,10 @@ namespace Microsoft.Dafny { /// ConditionOmitted == true && BodyOmitted == true
/// * while ... invariant J; { Stmt }
/// ConditionOmitted == true && BodyOmitted == false
+ /// * modify ...;
+ /// ConditionOmitted == true && BodyOmitted == false
+ /// * modify ... { Stmt }
+ /// ConditionOmitted == true && BodyOmitted == false
/// </summary>
public class SkeletonStatement : Statement
{
|