diff options
| -rw-r--r-- | Source/Core/Scanner.ssc | 4 | ||||
| -rw-r--r-- | Source/Core/scanner.frame | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 21 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.ssc | 3 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 168 | ||||
| -rw-r--r-- | Source/Dafny/Printer.ssc | 44 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 4 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.ssc | 20 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 132 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 7 | ||||
| -rw-r--r-- | Test/dafny0/BinaryTree.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny0/TerminationDemos.dfy | 80 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
13 files changed, 305 insertions, 196 deletions
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc index 2d977e79..a6f2c0a4 100644 --- a/Source/Core/Scanner.ssc +++ b/Source/Core/Scanner.ssc @@ -83,7 +83,7 @@ public class Buffer { static int pos;
public const int eof = '\uffff';
- public static void Fill(StreamReader! reader) {
+ public static void Fill(TextReader! reader) {
List<string!> defines = new List<string!>();
Fill(reader, defines);
}
@@ -97,7 +97,7 @@ public class Buffer { }
}
- public static void Fill(StreamReader! reader, List<string!>! defines) {
+ public static void Fill(TextReader! reader, List<string!>! defines) {
StringBuilder sb = new StringBuilder();
List<ReadState>! readState = new List<ReadState>(); // readState.Count is the current nesting level of #if's
int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n
diff --git a/Source/Core/scanner.frame b/Source/Core/scanner.frame index 3753c6e9..b9a2ce02 100644 --- a/Source/Core/scanner.frame +++ b/Source/Core/scanner.frame @@ -83,7 +83,7 @@ public class Buffer { static int pos;
public const int eof = '\uffff';
- public static void Fill(StreamReader! reader) {
+ public static void Fill(TextReader! reader) {
List<string!> defines = new List<string!>();
Fill(reader, defines);
}
@@ -97,7 +97,7 @@ public class Buffer { }
}
- public static void Fill(StreamReader! reader, List<string!>! defines) {
+ public static void Fill(TextReader! reader, List<string!>! defines) {
StringBuilder sb = new StringBuilder();
List<ReadState>! readState = new List<ReadState>(); // readState.Count is the current nesting level of #if's
int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index fe2e6a8c..d6f3aeae 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -61,10 +61,16 @@ private static Expression! ConvertToLocal(Expression! e) /// Note: first initialize the Scanner.
///</summary>
public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
- using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
- BoogiePL.Buffer.Fill(reader);
+ if (filename == "stdin.dfy") {
+ BoogiePL.Buffer.Fill(System.Console.In);
Scanner.Init(filename);
return Parse(classes);
+ } else {
+ using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
+ BoogiePL.Buffer.Fill(reader);
+ Scanner.Init(filename);
+ return Parse(classes);
+ }
}
}
@@ -260,6 +266,7 @@ MethodDecl<MemberModifiers mmod, out Method! m> List<MaybeFreeExpression!> req = new List<MaybeFreeExpression!>();
List<Expression!> mod = new List<Expression!>();
List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
+ List<Expression!> dec = new List<Expression!>();
Statement! bb; Statement body = null;
.)
"method"
@@ -274,16 +281,17 @@ MethodDecl<MemberModifiers mmod, out Method! m> Formals<false, outs>
]
- ( ";" { MethodSpec<req, mod, ens> }
- | { MethodSpec<req, mod, ens> } BlockStmt<out bb> (. body = bb; .)
+ ( ";" { MethodSpec<req, mod, ens, dec> }
+ | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb> (. body = bb; .)
)
(. parseVarScope.PopMarker();
- m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, body, attrs);
+ m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
.)
.
-MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<MaybeFreeExpression!\>! ens>
+MethodSpec<List<MaybeFreeExpression!\>! req, List<Expression!\>! mod, List<MaybeFreeExpression!\>! ens,
+ List<Expression!\>! decreases>
= (. Expression! e; bool isFree = false;
.)
( "modifies" [ Expression<out e> (. mod.Add(e); .)
@@ -295,6 +303,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> ";"
)
.
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index 549a32e0..b22e9cf6 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -494,6 +494,7 @@ namespace Microsoft.Dafny public readonly List<MaybeFreeExpression!>! Req;
public readonly List<Expression!>! Mod;
public readonly List<MaybeFreeExpression!>! Ens;
+ public readonly List<Expression!>! Decreases;
public readonly Statement Body;
public Method(Token! tok, string! name,
@@ -501,6 +502,7 @@ namespace Microsoft.Dafny [Captured] List<TypeParameter!>! typeArgs,
[Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,
[Captured] List<MaybeFreeExpression!>! req, [Captured] List<Expression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,
+ [Captured] List<Expression!>! decreases,
[Captured] Statement body,
Attributes attributes) {
this.IsClass = isClass;
@@ -511,6 +513,7 @@ namespace Microsoft.Dafny this.Req = req;
this.Mod = mod;
this.Ens = ens;
+ this.Decreases = decreases;
this.Body = body;
base(tok, name, attributes);
}
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index ec3e44f4..0560a45b 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -59,10 +59,16 @@ private static Expression! ConvertToLocal(Expression! e) /// Note: first initialize the Scanner.
///</summary>
public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
- using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
- BoogiePL.Buffer.Fill(reader);
+ if (filename == "stdin.dfy") {
+ BoogiePL.Buffer.Fill(System.Console.In);
Scanner.Init(filename);
return Parse(classes);
+ } else {
+ using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
+ BoogiePL.Buffer.Fill(reader);
+ Scanner.Init(filename);
+ return Parse(classes);
+ }
}
}
@@ -238,7 +244,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
if (t.kind == 11) {
FieldDecl(mmod, mm);
- } else if (t.kind == 29) {
+ } else if (t.kind == 30) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (t.kind == 16) {
@@ -279,7 +285,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { List<Expression!> decreases = new List<Expression!>();
Expression! bb; Expression body = null;
- Expect(29);
+ Expect(30);
if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost'"); }
while (t.kind == 5) {
@@ -295,11 +301,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { Type(out returnType);
if (t.kind == 10) {
Get();
- while (t.kind == 20 || t.kind == 30 || t.kind == 31) {
+ while (t.kind == 20 || t.kind == 22 || t.kind == 31) {
FunctionSpec(reqs, reads, decreases);
}
} else if (StartOf(2)) {
- while (t.kind == 20 || t.kind == 30 || t.kind == 31) {
+ while (t.kind == 20 || t.kind == 22 || t.kind == 31) {
FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
@@ -319,6 +325,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { List<MaybeFreeExpression!> req = new List<MaybeFreeExpression!>();
List<Expression!> mod = new List<Expression!>();
List<MaybeFreeExpression!> ens = new List<MaybeFreeExpression!>();
+ List<Expression!> dec = new List<Expression!>();
Statement! bb; Statement body = null;
Expect(16);
@@ -340,17 +347,17 @@ public static int Parse (List<TopLevelDecl!>! classes) { if (t.kind == 10) {
Get();
while (StartOf(3)) {
- MethodSpec(req, mod, ens);
+ MethodSpec(req, mod, ens, dec);
}
} else if (StartOf(4)) {
while (StartOf(3)) {
- MethodSpec(req, mod, ens);
+ MethodSpec(req, mod, ens, dec);
}
BlockStmt(out bb);
body = bb;
} else Error(96);
parseVarScope.PopMarker();
- m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, body, attrs);
+ m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
}
@@ -368,7 +375,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
- if (t.kind == 22) {
+ if (t.kind == 23) {
FormalsOptionalIds(formals);
}
parseVarScope.PopMarker();
@@ -379,7 +386,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void FormalsOptionalIds(List<Formal!>! formals) {
Token! id; Type! ty; string! name;
- Expect(22);
+ Expect(23);
if (StartOf(5)) {
TypeIdentOptional(out id, out name, out ty);
formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name);
@@ -389,7 +396,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name);
}
}
- Expect(23);
+ Expect(24);
}
static void IdentType(out Token! id, out Type! ty) {
@@ -441,13 +448,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
- if (t.kind == 24) {
+ if (t.kind == 25) {
Get();
tok = token;
- } else if (t.kind == 25) {
+ } else if (t.kind == 26) {
Get();
tok = token; ty = new IntType();
- } else if (t.kind == 26) {
+ } else if (t.kind == 27) {
Get();
tok = token; gt = new List<Type!>();
GenericInstantiation(gt);
@@ -456,7 +463,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
ty = new SetType(gt[0]);
- } else if (t.kind == 27) {
+ } else if (t.kind == 28) {
Get();
tok = token; gt = new List<Type!>();
GenericInstantiation(gt);
@@ -465,14 +472,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
ty = new SeqType(gt[0]);
- } else if (t.kind == 1 || t.kind == 28) {
+ } else if (t.kind == 1 || t.kind == 29) {
ReferenceType(out tok, out ty);
} else Error(97);
}
static void Formals(bool incoming, List<Formal!>! formals) {
Token! id; Type! ty;
- Expect(22);
+ Expect(23);
if (t.kind == 1) {
IdentType(out id, out ty);
formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val);
@@ -482,10 +489,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { formals.Add(new Formal(id, id.val, ty, incoming)); parseVarScope.Push(id.val, id.val);
}
}
- Expect(23);
+ Expect(24);
}
- static void MethodSpec(List<MaybeFreeExpression!>! req, List<Expression!>! mod, List<MaybeFreeExpression!>! ens) {
+ static void MethodSpec(List<MaybeFreeExpression!>! req, List<Expression!>! mod, List<MaybeFreeExpression!>! ens,
+List<Expression!>! decreases) {
Expression! e; bool isFree = false;
if (t.kind == 18) {
@@ -516,6 +524,10 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(10);
ens.Add(new MaybeFreeExpression(e, isFree));
} else Error(98);
+ } else if (t.kind == 22) {
+ Get();
+ PossiblyWildExpressions(decreases);
+ Expect(10);
} else Error(99);
}
@@ -553,6 +565,17 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else Error(100);
}
+ static void PossiblyWildExpressions(List<Expression!>! args) {
+ Expression! e;
+ PossiblyWildExpression(out e);
+ args.Add(e);
+ while (t.kind == 12) {
+ Get();
+ PossiblyWildExpression(out e);
+ args.Add(e);
+ }
+ }
+
static void GenericInstantiation(List<Type!>! gt) {
Type! ty;
Expect(14);
@@ -570,7 +593,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
- if (t.kind == 28) {
+ if (t.kind == 29) {
Get();
tok = token; ty = new ObjectType();
} else if (t.kind == 1) {
@@ -590,13 +613,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expression(out e);
Expect(10);
reqs.Add(e);
- } else if (t.kind == 30) {
+ } else if (t.kind == 31) {
Get();
if (StartOf(9)) {
PossiblyWildExpressions(reads);
}
Expect(10);
- } else if (t.kind == 31) {
+ } else if (t.kind == 22) {
Get();
Expressions(decreases);
Expect(10);
@@ -614,17 +637,6 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(6);
}
- static void PossiblyWildExpressions(List<Expression!>! args) {
- Expression! e;
- PossiblyWildExpression(out e);
- args.Add(e);
- while (t.kind == 12) {
- Get();
- PossiblyWildExpression(out e);
- args.Add(e);
- }
- }
-
static void Expressions(List<Expression!>! args) {
Expression! e;
Expression(out e);
@@ -679,7 +691,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(34);
x = token; parseVarScope.PushMarker();
Ident(out id);
- if (t.kind == 22) {
+ if (t.kind == 23) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
@@ -690,7 +702,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
}
- Expect(23);
+ Expect(24);
}
Expect(35);
Expression(out body);
@@ -729,7 +741,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { UseStmt(out s);
break;
}
- case 1: case 22: case 85: case 86: {
+ case 1: case 23: case 85: case 86: {
AssignStmt(out s);
break;
}
@@ -947,7 +959,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { x = token;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 19 || t.kind == 31 || t.kind == 45) {
+ while (t.kind == 19 || t.kind == 22 || t.kind == 45) {
if (t.kind == 19 || t.kind == 45) {
isFree = false;
if (t.kind == 19) {
@@ -982,7 +994,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
- Expect(22);
+ Expect(23);
Ident(out boundVar);
if (t.kind == 13) {
Get();
@@ -995,7 +1007,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
Expression(out range);
}
- Expect(23);
+ Expect(24);
Expect(5);
while (t.kind == 8 || t.kind == 50 || t.kind == 51) {
if (t.kind == 50) {
@@ -1044,7 +1056,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 22 || t.kind == 85 || t.kind == 86) {
+ } else if (t.kind == 23 || t.kind == 85 || t.kind == 86) {
ObjectExpression(out e);
} else Error(111);
while (t.kind == 80 || t.kind == 82) {
@@ -1081,7 +1093,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void Guard(out Expression e) {
Expression! ee; e = null;
- Expect(22);
+ Expect(23);
if (t.kind == 32) {
Get();
e = null;
@@ -1089,14 +1101,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expression(out ee);
e = ee;
} else Error(112);
- Expect(23);
+ Expect(24);
}
static void CallStmtSubExpr(out Expression! e) {
e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 22 || t.kind == 85 || t.kind == 86) {
+ } else if (t.kind == 23 || t.kind == 85 || t.kind == 86) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
} else Error(113);
@@ -1370,12 +1382,12 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(80);
Ident(out id);
elements = new List<Expression!>();
- if (t.kind == 22) {
+ if (t.kind == 23) {
Get();
if (StartOf(6)) {
Expressions(elements);
}
- Expect(23);
+ Expect(24);
}
e = new DatatypeValue(token, dtName.val, id.val, elements);
break;
@@ -1383,9 +1395,9 @@ public static int Parse (List<TopLevelDecl!>! classes) { case 81: {
Get();
x = token;
- Expect(22);
- Expression(out e);
Expect(23);
+ Expression(out e);
+ Expect(24);
e = new FreshExpr(x, e);
break;
}
@@ -1435,13 +1447,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void IdentOrFuncExpression(out Expression! e) {
Token! id; e = dummyExpr; List<Expression!>! args;
Ident(out id);
- if (t.kind == 22) {
+ if (t.kind == 23) {
Get();
args = new List<Expression!>();
if (StartOf(6)) {
Expressions(args);
}
- Expect(23);
+ Expect(24);
e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args);
}
if (e == dummyExpr) {
@@ -1462,18 +1474,18 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (t.kind == 86) {
Get();
x = token;
- Expect(22);
- Expression(out e);
Expect(23);
+ Expression(out e);
+ Expect(24);
e = new OldExpr(x, e);
- } else if (t.kind == 22) {
+ } else if (t.kind == 23) {
Get();
if (StartOf(15)) {
QuantifierGuts(out e);
} else if (StartOf(6)) {
Expression(out e);
} else Error(124);
- Expect(23);
+ Expect(24);
} else Error(125);
}
@@ -1485,13 +1497,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { if (t.kind == 80) {
Get();
Ident(out id);
- if (t.kind == 22) {
+ if (t.kind == 23) {
Get();
args = new List<Expression!>(); func = true;
if (StartOf(6)) {
Expressions(args);
}
- Expect(23);
+ Expect(24);
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
@@ -1682,16 +1694,16 @@ public static int Parse (List<TopLevelDecl!>! classes) { case 19: s = "free expected"; break;
case 20: s = "requires expected"; break;
case 21: s = "ensures expected"; break;
- case 22: s = "( expected"; break;
- case 23: s = ") expected"; break;
- case 24: s = "bool expected"; break;
- case 25: s = "int expected"; break;
- case 26: s = "set expected"; break;
- case 27: s = "seq expected"; break;
- case 28: s = "object expected"; break;
- case 29: s = "function expected"; break;
- case 30: s = "reads expected"; break;
- case 31: s = "decreases expected"; break;
+ case 22: s = "decreases expected"; break;
+ case 23: s = "( expected"; break;
+ case 24: s = ") expected"; break;
+ case 25: s = "bool expected"; break;
+ case 26: s = "int expected"; break;
+ case 27: s = "set expected"; break;
+ case 28: s = "seq expected"; break;
+ case 29: s = "object expected"; break;
+ case 30: s = "function expected"; break;
+ case 31: s = "reads expected"; break;
case 32: s = "* expected"; break;
case 33: s = "match expected"; break;
case 34: s = "case expected"; break;
@@ -1802,22 +1814,22 @@ public static int Parse (List<TopLevelDecl!>! classes) { static bool[,]! set = {
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, T,x,x,T, T,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,T,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,T,T,x, T,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,T,T,x, T,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,x,x,x, T,x,x,T, T,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,T,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,T,T,x, T,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,T,T,x, T,x,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
{x,x,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x},
- {x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x}
+ {x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index 89b9f62e..23e6dfce 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -137,24 +137,9 @@ namespace Microsoft.Dafny { } else {
wr.WriteLine();
}
- foreach (Expression r in f.Req) {
- Indent(2 * IndentAmount);
- wr.Write("requires ");
- PrintExpression(r);
- wr.WriteLine(";");
- }
- foreach (Expression r in f.Reads) {
- Indent(2 * IndentAmount);
- wr.Write("reads ");
- PrintExpression(r);
- wr.WriteLine(";");
- }
- foreach (Expression r in f.Decreases) {
- Indent(2 * IndentAmount);
- wr.Write("decreases ");
- PrintExpression(r);
- wr.WriteLine(";");
- }
+ PrintSpec("requires", f.Req, 2 * IndentAmount);
+ PrintSpecLine("reads", f.Reads, 2 * IndentAmount);
+ PrintSpecLine("decreases", f.Decreases, 2 * IndentAmount);
if (f.Body != null) {
Indent(IndentAmount);
wr.WriteLine("{");
@@ -205,8 +190,9 @@ namespace Microsoft.Dafny { wr.WriteLine(method.Body == null ? ";" : ":");
PrintSpec("requires", method.Req, 2 * IndentAmount);
- PrintSpec("modifies", method.Mod, 2 * IndentAmount);
+ PrintSpecLine("modifies", method.Mod, 2 * IndentAmount);
PrintSpec("ensures", method.Ens, 2 * IndentAmount);
+ PrintSpecLine("decreases", method.Decreases, 2 * IndentAmount);
if (method.Body != null) {
Indent(IndentAmount);
@@ -242,6 +228,15 @@ namespace Microsoft.Dafny { }
}
+ void PrintSpecLine(string! kind, List<Expression!>! ee, int indent) {
+ if (ee.Count != 0) {
+ Indent(indent);
+ wr.Write("{0} ", kind);
+ PrintExpressionList(ee);
+ wr.WriteLine(";");
+ }
+ }
+
void PrintSpec(string! kind, List<MaybeFreeExpression!>! ee, int indent) {
foreach (MaybeFreeExpression e in ee) {
Indent(indent);
@@ -377,16 +372,7 @@ namespace Microsoft.Dafny { int ind = indent + IndentAmount;
PrintSpec("invariant", s.Invariants, ind);
- if (s.Decreases.Count != 0) {
- Indent(indent);
- string sep = "decreases ";
- foreach (Expression e in s.Decreases) {
- wr.Write(sep);
- sep = ", ";
- PrintExpression(e);
- }
- wr.WriteLine(";");
- }
+ PrintSpecLine("decreases", s.Decreases, indent);
Indent(indent);
PrintStatement(s.Body, indent);
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 8bbc1d29..d53bf450 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -343,6 +343,10 @@ namespace Microsoft.Dafny { Error(e, "a modifies-clause expression must denote an object or a collection of objects (instead got {0})", e.Type);
}
}
+ foreach (Expression e in m.Decreases) {
+ ResolveExpression(e, false);
+ // any type is fine
+ }
// Add out-parameters to the scope, but don't care about any duplication errors, since they have already been reported
foreach (Formal p in m.Outs) {
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index 921ef4f6..a1895c0c 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -286,14 +286,14 @@ public class Scanner { case "free": t.kind = 19; break;
case "requires": t.kind = 20; break;
case "ensures": t.kind = 21; break;
- case "bool": t.kind = 24; break;
- case "int": t.kind = 25; break;
- case "set": t.kind = 26; break;
- case "seq": t.kind = 27; break;
- case "object": t.kind = 28; break;
- case "function": t.kind = 29; break;
- case "reads": t.kind = 30; break;
- case "decreases": t.kind = 31; break;
+ case "decreases": t.kind = 22; break;
+ case "bool": t.kind = 25; break;
+ case "int": t.kind = 26; break;
+ case "set": t.kind = 27; break;
+ case "seq": t.kind = 28; break;
+ case "object": t.kind = 29; break;
+ case "function": t.kind = 30; break;
+ case "reads": t.kind = 31; break;
case "match": t.kind = 33; break;
case "case": t.kind = 34; break;
case "label": t.kind = 36; break;
@@ -366,9 +366,9 @@ public class Scanner { if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}
else {t.kind = 15; goto done;}
case 12:
- {t.kind = 22; goto done;}
- case 13:
{t.kind = 23; goto done;}
+ case 13:
+ {t.kind = 24; goto done;}
case 14:
{t.kind = 32; goto done;}
case 15:
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index aef2ad9b..185a81ee 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -897,8 +897,9 @@ namespace Microsoft.Dafny { CheckWellformed(p, null, Position.Positive, locals, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
}
- // Note: the reads clauses are not checked for well-formedness (is that sound?), because the syntax is
- // not rich enough for programmers to specify reads clauses and always being absolutely well-defined.
+ // Note: the reads clauses are not checked for well-formedness (is that sound?), because it used to
+ // be that the syntax was not rich enough for programmers to specify reads clauses and always being
+ // absolutely well-defined.
// check well-formedness of the decreases clauses
foreach (Expression p in f.Decreases) {
CheckWellformed(p, f, Position.Positive, locals, builder, etran);
@@ -1153,58 +1154,15 @@ namespace Microsoft.Dafny { builder.Add(Assert(expr.tok, q, "insufficient reads clause to invoke function"));
// finally, check that the decreases measure goes down
- Bpl.Expr decrExpr;
- int N = min{e.Function.Decreases.Count, func.Decreases.Count};
- if (N != 0) {
- // both functions have explicit decreases clauses, so use them
- List<Type!> types = new List<Type!>();
- List<Bpl.Expr!> calleeTotal = new List<Bpl.Expr!>();
- List<Bpl.Expr!> callee = new List<Bpl.Expr!>();
- List<Bpl.Expr!> caller = new List<Bpl.Expr!>();
- for (int i = 0; i < N; i++) {
- Expression e0 = Substitute(e.Function.Decreases[i], e.Receiver, substMap);
- Expression e1 = func.Decreases[i];
- if (!CompatibleDecreasesTypes((!)e0.Type, (!)e1.Type)) {
- break;
- }
- types.Add(e0.Type);
- calleeTotal.Add(IsTotal(e0, etran));
- callee.Add(etran.TrExpr(e0));
- caller.Add(etran.TrExpr(e1));
- }
- decrExpr = DecreasesCheck(expr.tok, types, calleeTotal, callee, caller, builder, etran, "");
- } else {
- // todo: include totality checks for callee in this branch!
- List<Expression!> d0 = null, d1 = null;
- if (e.Function.Decreases.Count == 0) {
- d0 = e.Function.Reads; // use its reads clause instead
- } else if (e.Function.Decreases[0].Type is SetType) {
- d0 = new List<Expression!>(1);
- d0.Add(e.Function.Decreases[0]); // use the first component of the declared decreases clause
- } else {
- d0 = null; // there is a declared decreases clause, but its first component has a type that is incomparable with a reads clause
- }
- if (func.Decreases.Count == 0) {
- d1 = func.Reads; // use its reads clause instead
- } else if (func.Decreases[0].Type is SetType) {
- d1 = new List<Expression!>(1);
- d1.Add(func.Decreases[0]); // use the first component of the declared decreases clause
- } else {
- d1 = null; // there is a declared decreases clause, but its first component has a type that is incomparable with a reads clause
- }
- if (d0 == null || d1 == null) {
- decrExpr = Bpl.Expr.False;
- } else {
- oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$d", predef.RefType));
- o = new Bpl.IdentifierExpr(expr.tok, oVar);
- Bpl.Expr r0 = InRWClause(expr.tok, o, d0, etran, e.Receiver, substMap);
- Bpl.Expr r1 = InRWClause(expr.tok, o, d1, etran, null, null);
- Bpl.Expr qSubset = new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(r0, r1));
- Bpl.Expr qProper = new Bpl.ExistsExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.And(Bpl.Expr.Not(r0), r1));
- decrExpr = Bpl.Expr.And(qSubset, qProper);
- }
+ List<Expression!> contextDecreases = func.Decreases;
+ if (contextDecreases.Count == 0) {
+ contextDecreases = func.Reads; // use its reads clause instead
}
- builder.Add(Assert(expr.tok, decrExpr, "failure to decrease termination measure"));
+ List<Expression!> calleeDecreases = e.Function.Decreases;
+ if (calleeDecreases.Count == 0) {
+ calleeDecreases = e.Function.Reads; // use its reads clause instead
+ }
+ CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);
}
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
@@ -1775,7 +1733,28 @@ namespace Microsoft.Dafny { outs.Add(etran.TrExpr(e));
}
}
-
+
+ if (currentMethod.Decreases.Count == 0 || exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {
+ // omit termination checking for calls in this context
+ } else {
+ // Check termination. Ideally, this would be checked after the precondition check.
+ // Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
+ Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ VarDecl local = new VarDecl(p.tok, p.Name, p.Type, null);
+ local.type = local.OptionalType; // resolve local here
+ IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
+ ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here
+ substMap.Add(p, ie);
+ locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
+ Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.TrExpr(s.Args[i]));
+ builder.Add(cmd);
+ }
+ CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);
+ }
+
Bpl.CallCmd call = new Bpl.CallCmd(stmt.Tok, s.Method.FullName, ins, outs);
builder.Add(call);
for (int i = 0; i < s.Lhs.Count; i++) {
@@ -1918,6 +1897,7 @@ namespace Microsoft.Dafny { // time for the actual loop body
TrStmt(s.Body, loopBodyBuilder, locals, etran);
// check definedness of decreases expressions
+ List<Token!> toks = new List<Token!>();
List<Type!> types = new List<Type!>();
List<Bpl.Expr!> decrsTotal = new List<Bpl.Expr!>();
List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
@@ -1925,11 +1905,12 @@ namespace Microsoft.Dafny { // The following totality check implies that the loop invariant stating the same property will hold;
// thus, an alternative (perhaps preferable) design would be: add the totality check also just before
// the loop, and change the loop invariant to be free.
+ toks.Add(e.tok);
types.Add((!)e.Type);
decrsTotal.Add(IsTotal(e, etran));
decrs.Add(etran.TrExpr(e));
}
- Bpl.Expr decrCheck = DecreasesCheck(stmt.Tok, types, decrsTotal, decrs, oldBfs, loopBodyBuilder, etran, "at end of loop iteration");
+ Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrsTotal, decrs, oldBfs, loopBodyBuilder, etran, " at end of loop iteration");
loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, "decreases expression might not decrease"));
}
Bpl.StmtList body = loopBodyBuilder.Collect(stmt.Tok);
@@ -2032,11 +2013,41 @@ namespace Microsoft.Dafny { }
}
+ void CheckCallTermination(Token! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,
+ 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!>();
+ List<Bpl.Expr!> calleeTotal = new List<Bpl.Expr!>();
+ List<Bpl.Expr!> callee = new List<Bpl.Expr!>();
+ List<Bpl.Expr!> caller = new List<Bpl.Expr!>();
+ for (int i = 0; i < N; i++) {
+ Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap);
+ Expression e1 = contextDecreases[i];
+ if (!CompatibleDecreasesTypes((!)e0.Type, (!)e1.Type)) {
+ break;
+ }
+ toks.Add(tok);
+ types.Add(e0.Type);
+ calleeTotal.Add(IsTotal(e0, etran));
+ callee.Add(etran.TrExpr(e0));
+ caller.Add(etran.TrExpr(e1));
+ }
+ Bpl.Expr decrExpr = DecreasesCheck(toks, types, calleeTotal, callee, caller, builder, etran, "");
+ builder.Add(Assert(tok, decrExpr, "failure to decrease termination measure"));
+ }
+
/// <summary>
/// Returns the expression that says whether or not the decreases function has gone down. ee0 represents the new
/// values and ee1 represents old values.
/// </summary>
- Bpl.Expr! DecreasesCheck(Token! tok, List<Type!>! types, List<Bpl.Expr!>! total0, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,
+ Bpl.Expr! DecreasesCheck(List<Token!>! toks, List<Type!>! types, List<Bpl.Expr!>! total0, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,
Bpl.StmtListBuilder! builder, ExpressionTranslator! etran, string! suffixMsg)
requires predef != null;
requires types.Count == ee0.Count && ee0.Count == ee1.Count;
@@ -2048,7 +2059,7 @@ namespace Microsoft.Dafny { List<Bpl.Expr!> Less = new List<Bpl.Expr!>(N);
for (int i = 0; i < N; i++) {
Bpl.Expr! less, eq;
- ComputeLessEq(tok, types[i], ee0[i], ee1[i], out less, out eq, etran);
+ ComputeLessEq(toks[i], types[i], ee0[i], ee1[i], out less, out eq, etran);
Eq.Add(eq);
Less.Add(less);
}
@@ -2060,12 +2071,13 @@ namespace Microsoft.Dafny { // more precisely, for component k of the lexicographic decreases function, check:
// ee0[0] < ee1[0] || ee0[1] < ee1[1] || ... || ee0[k-1] < ee1[k-1] || ee0[k] == ee1[k] || 0 <= ee1[k]
for (int k = 0; k < N; k++) {
- // we only need to check lower bound for integers--sets, sequences, booleans, and references all have natural lower bounds
+ // we only need to check lower bound for integers--sets, sequences, booleans, references, and datatypes all have natural lower bounds
Bpl.Expr prefixIsLess = Bpl.Expr.False;
for (int i = 0; i < k; i++) {
prefixIsLess = Bpl.Expr.Or(prefixIsLess, Less[i]);
}
- Bpl.Cmd cmd = Assert(ee0[k].tok, Bpl.Expr.Or(prefixIsLess, total0[k]), "decreases expression (component " + k + ") must be well-defined" + suffixMsg);
+ string component = N == 1 ? "" : " (component " + k + ")";
+ Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(prefixIsLess, total0[k]), "decreases expression" + component + " must be well-defined" + suffixMsg);
builder.Add(cmd);
if (types[k] is IntType) {
@@ -2073,7 +2085,7 @@ namespace Microsoft.Dafny { for (int i = 0; i < k; i++) {
bounded = Bpl.Expr.Or(bounded, Less[i]);
}
- cmd = Assert(ee0[k].tok, Bpl.Expr.Or(bounded, Eq[k]), "decreases expression (component " + k + ") must be bounded below by 0" + suffixMsg);
+ cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), "decreases expression" + component + " must be bounded below by 0" + suffixMsg);
builder.Add(cmd);
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 540bcb4b..95302b05 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -8,8 +8,7 @@ class MyClass<T, U> { method M(s: bool, lotsaObjects: set<object>)
returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>):
requires s;
- modifies this;
- modifies lotsaObjects;
+ modifies this, lotsaObjects;
ensures t == t;
ensures old(null) != this;
{
@@ -195,3 +194,7 @@ Dafny program verifier finished with 7 verified, 0 errors -------------------- SumOfCubes.dfy --------------------
Dafny program verifier finished with 10 verified, 0 errors
+
+-------------------- TerminationDemos.dfy --------------------
+
+Dafny program verifier finished with 7 verified, 0 errors
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy index 54a98a56..5f56cf40 100644 --- a/Test/dafny0/BinaryTree.dfy +++ b/Test/dafny0/BinaryTree.dfy @@ -1,6 +1,6 @@ class IntSet {
- var contents: set<int>;
- var footprint: set<object>;
+ ghost var contents: set<int>;
+ ghost var footprint: set<object>;
var root: Node;
@@ -48,7 +48,7 @@ class IntSet { footprint := root.footprint + {this};
}
- method InsertHelper(x: int, n: Node) returns (m: Node)
+ class method InsertHelper(x: int, n: Node) returns (m: Node)
requires n == null || n.Valid();
modifies n.footprint;
ensures m != null && m.Valid();
@@ -97,9 +97,9 @@ class IntSet { }
class Node {
- var contents: set<int>;
- var footprint: set<object>;
-
+ ghost var contents: set<int>;
+ ghost var footprint: set<object>;
+
var data: int;
var left: Node;
var right: Node;
diff --git a/Test/dafny0/TerminationDemos.dfy b/Test/dafny0/TerminationDemos.dfy new file mode 100644 index 00000000..6b63bfec --- /dev/null +++ b/Test/dafny0/TerminationDemos.dfy @@ -0,0 +1,80 @@ +class Example {
+ method M(n: int)
+ {
+ var i := 0;
+ while (i < n)
+ decreases n - i;
+ {
+ i := i + 1;
+ }
+ }
+}
+
+// -----------------------------------
+
+class Fibonacci {
+ function Fib(n: int): int
+ decreases n;
+ {
+ if n < 2 then n else Fib(n-2) + Fib(n-1)
+ }
+}
+
+// -----------------------------------
+
+class Ackermann {
+ function F(m: int, n: int): int
+ decreases m, n;
+ {
+ if m <= 0 then
+ n + 1
+ else if n <= 0 then
+ F(m - 1, 1)
+ else
+ F(m - 1, F(m, n - 1))
+ }
+}
+
+// -----------------------------------
+
+class List {
+ var data: int;
+ var next: List;
+ ghost var ListNodes: set<List>;
+ function IsAcyclic(): bool
+ reads *;
+ decreases ListNodes;
+ {
+ this in ListNodes &&
+ (next != null ==>
+ next.ListNodes <= ListNodes && this !in next.ListNodes &&
+ next.IsAcyclic())
+ }
+
+ method Singleton(x: int) returns (list: List)
+ ensures list != null && list.IsAcyclic();
+ {
+ list := new List;
+ list.data := x;
+ list.next := null;
+ list.ListNodes := {list};
+ }
+
+ method Prepend(x: int, tail: List) returns (list: List)
+ requires tail == null || tail.IsAcyclic();
+ ensures list != null && list.IsAcyclic();
+ {
+ list := new List;
+ list.data := x;
+ list.next := tail;
+ list.ListNodes := if tail == null then {list} else {list} + tail.ListNodes;
+ }
+
+ function Sum(): int
+ requires IsAcyclic();
+ reads *;
+ decreases ListNodes;
+ {
+ if next == null then data else data + next.Sum()
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 64efe27b..c1837b43 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -21,7 +21,7 @@ for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy
- SumOfCubes.dfy) do (
+ SumOfCubes.dfy TerminationDemos.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% %* %%f
|