diff options
| author |  rustanleino <unknown> | 2010-03-18 01:18:47 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-18 01:18:47 +0000 |
| commit | 946c1329d9cda4ec68abc9b326c6ac7163c63cd8 (patch) | |
| tree | 157042b897a326b5193386a04cb368e7535bedbe /Source/Dafny | |
| parent | 08a4a9054ea4651f409ca7275a70dca67b4254cf (diff) | |
Dafny:
* Allow "decreases *" only for loops.
* Cosmetic changes in SchorrWaite.dfy
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 14 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 16 |
3 files changed, 12 insertions, 20 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index bd1e7d0f..6fe25fb5 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -333,7 +333,7 @@ MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<Maybe ( "requires" Expression<out e> ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
| "ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
)
- | "decreases" PossiblyWildExpressions<decreases> ";"
+ | "decreases" Expressions<decreases> ";"
)
.
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index b2ec727f..2ca6769c 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -588,7 +588,7 @@ List<Expression!>! decreases) { } else Error(101);
} else if (t.kind == 25) {
Get();
- PossiblyWildExpressions(decreases);
+ Expressions(decreases);
Expect(13);
} else Error(102);
}
@@ -627,13 +627,13 @@ List<Expression!>! decreases) { } else Error(103);
}
- static void PossiblyWildExpressions(List<Expression!>! args) {
+ static void Expressions(List<Expression!>! args) {
Expression! e;
- PossiblyWildExpression(out e);
+ Expression(out e);
args.Add(e);
while (t.kind == 15) {
Get();
- PossiblyWildExpression(out e);
+ Expression(out e);
args.Add(e);
}
}
@@ -699,13 +699,13 @@ List<Expression!>! decreases) { Expect(7);
}
- static void Expressions(List<Expression!>! args) {
+ static void PossiblyWildExpressions(List<Expression!>! args) {
Expression! e;
- Expression(out e);
+ PossiblyWildExpression(out e);
args.Add(e);
while (t.kind == 15) {
Get();
- Expression(out e);
+ PossiblyWildExpression(out e);
args.Add(e);
}
}
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index e6bed1b1..9bf4fd62 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -1850,14 +1850,10 @@ namespace Microsoft.Dafny { }
// Check termination
- if (exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {
- // omit termination checking for calls in this context
- } else {
- ModuleDecl module = ((!)s.Method.EnclosingClass).Module;
- if (module == ((!)currentMethod.EnclosingClass).Module) {
- if (module.CallGraph.GetSCCRepresentative(s.Method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {
- CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);
- }
+ ModuleDecl module = ((!)s.Method.EnclosingClass).Module;
+ if (module == ((!)currentMethod.EnclosingClass).Module) {
+ if (module.CallGraph.GetSCCRepresentative(s.Method) == module.CallGraph.GetSCCRepresentative(currentMethod)) {
+ CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);
}
}
@@ -2192,10 +2188,6 @@ namespace Microsoft.Dafny { Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap,
ExpressionTranslator! etran, Bpl.StmtListBuilder! builder)
{
- if (exists{Expression e in contextDecreases; e is WildcardExpr}) {
- // omit termination checking for calls in this context
- return;
- }
int N = min{contextDecreases.Count, calleeDecreases.Count};
List<Token!> toks = new List<Token!>();
List<Type!> types = new List<Type!>();
|