summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Dafny/Dafny.atg2
-rw-r--r--Dafny/Parser.ssc14
-rw-r--r--Dafny/Translator.ssc16
-rw-r--r--Test/dafny0/SchorrWaite.dfy36
4 files changed, 30 insertions, 38 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index bd1e7d0f..6fe25fb5 100644
--- a/Dafny/Dafny.atg
+++ b/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/Dafny/Parser.ssc b/Dafny/Parser.ssc
index b2ec727f..2ca6769c 100644
--- a/Dafny/Parser.ssc
+++ b/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/Dafny/Translator.ssc b/Dafny/Translator.ssc
index e6bed1b1..9bf4fd62 100644
--- a/Dafny/Translator.ssc
+++ b/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!>();
diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index 97317792..5a47cdad 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -4,10 +4,10 @@
// Copyright (c) 2008, Microsoft.
class Node {
+ var children: seq<Node>;
var marked: bool;
var childrenVisited: int;
- var children: seq<Node>;
- var pathFromRoot: Path; // used only as ghost variable
+ ghost var pathFromRoot: Path;
}
class Main {
@@ -21,7 +21,7 @@ class Main {
ensures root.marked;
// nodes reachable from 'root' are marked:
ensures (forall n :: n in S && n.marked ==>
- (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ (forall ch :: ch in n.children && ch != null ==> ch.marked));
ensures (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
@@ -35,14 +35,14 @@ class Main {
(forall ch :: ch in n.children ==> ch == null || ch in S));
requires (forall n :: n in S && n.marked ==>
n in stackNodes ||
- (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ (forall ch :: ch in n.children && ch != null ==> ch.marked));
requires (forall n :: n in stackNodes ==> n != null && n.marked);
modifies S;
ensures root.marked;
// nodes reachable from 'root' are marked:
ensures (forall n :: n in S && n.marked ==>
n in stackNodes ||
- (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ (forall ch :: ch in n.children && ch != null ==> ch.marked));
ensures (forall n: Node :: n in S && old(n.marked) ==> n.marked);
ensures (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
@@ -57,7 +57,7 @@ class Main {
invariant (forall n :: n in S && n.marked ==>
n == root ||
n in stackNodes ||
- (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ (forall ch :: ch in n.children && ch != null ==> ch.marked));
invariant (forall j :: 0 <= j && j < i ==>
root.children[j] == null || root.children[j].marked);
invariant (forall n: Node :: n in S && old(n.marked) ==> n.marked);
@@ -88,7 +88,7 @@ class Main {
ensures root.marked;
// nodes reachable from 'root' are marked:
ensures (forall n :: n in S && n.marked ==>
- (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ (forall ch :: ch in n.children && ch != null ==> ch.marked));
ensures (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
@@ -96,7 +96,7 @@ class Main {
var t := root;
t.marked := true;
var stackNodes := [];
- var unmarkedNodes := S - {t}; // used as ghost variable
+ ghost var unmarkedNodes := S - {t};
while (true)
invariant root.marked && t in S && t !in stackNodes;
// stackNodes has no duplicates:
@@ -115,7 +115,7 @@ class Main {
invariant 0 < |stackNodes| ==>
stackNodes[|stackNodes|-1].children[stackNodes[|stackNodes|-1].childrenVisited] == t;
invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
- (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ (forall ch :: ch in n.children && ch != null ==> ch.marked));
invariant (forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited));
invariant (forall n: Node :: n in S ==> n.children == old(n.children));
@@ -168,27 +168,27 @@ class Main {
// S is closed under 'children':
requires (forall n :: n in S ==> n != null &&
(forall ch :: ch in n.children ==> ch == null || ch in S));
- // the graph starts off with nothing marked and nothing being indicated as currently being visited
+ // the graph starts off with nothing marked and nothing being indicated as currently being visited:
requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);
modifies S;
// nodes reachable from 'root' are marked:
ensures root.marked;
ensures (forall n :: n in S && n.marked ==>
- (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
- // every marked node was reachable from 'root' in the pre-state
+ (forall ch :: ch in n.children && ch != null ==> ch.marked));
+ // every marked node was reachable from 'root' in the pre-state:
ensures (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));
- // the graph has not changed
+ // the structure of the graph has not changed:
ensures (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
{
var t := root;
var p: Node := null; // parent of t in original graph
- var path := #Path.Empty;
+ ghost var path := #Path.Empty;
t.marked := true;
t.pathFromRoot := path;
- var stackNodes := []; // used as ghost variable
- var unmarkedNodes := S - {t}; // used as ghost variable
+ ghost var stackNodes := [];
+ ghost var unmarkedNodes := S - {t};
while (true)
invariant root.marked && t != null && t in S && t !in stackNodes;
invariant |stackNodes| == 0 <==> p == null;
@@ -204,7 +204,7 @@ class Main {
n.children[j] == null || n.children[j].marked));
invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|);
invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
- (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
+ (forall ch :: ch in n.children && ch != null ==> ch.marked));
invariant (forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited));
invariant (forall n :: n in S ==> n in stackNodes || n.children == old(n.children));
@@ -212,7 +212,7 @@ class Main {
|n.children| == old(|n.children|) &&
(forall j :: 0 <= j && j < |n.children| ==>
j == n.childrenVisited || n.children[j] == old(n.children[j])));
- // every marked node is reachable
+ // every marked node is reachable:
invariant old(ReachableVia(root, path, t, S));
invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>
old(ReachableVia(root, pth, n, S)));
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 21:54:31 +0000