diff options
| author |  rustanleino <unknown> | 2009-11-24 06:05:35 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-24 06:05:35 +0000 |
| commit | 666463d9fa29f14ea8aaec4d5bc8bd602e0033ba (patch) | |
| tree | c1cef0b220b1cf52472eeac82ad0bf75bf8c54e7 | |
| parent | 8c5fb20c77e73481e0ef9f5d9a5fb4b01d77aacd (diff) | |
* Added decreases clauses to functions
* If no decreases clause is given, the decreases clause defaults to the set of objects denoted by the reads clause, which was the previous Dafny behavior
* Made Dafny check loops for termination by default. Previously, this was done only if the loop had a decreases clause. To indicate that a loop is to be checked only for partial correctness, Dafny now allows "decreases *".
* Allow "reads *" to say that the function may read anything at all (sound, but not very useful)
* Adjusted frame axioms of functions to speak of allocated objects more liberally; and also added antecedents about the heaps being well-formed and the parameters being allocated
* Added some previously omitted well-definedness checks.
* Fixed some bugs in the resolver that caused some type errors not to be reported
* Added some messages to go with some (previously rather opaquely reported) errors
* Fixed some test cases that previously had ordered conjuncts incorrectly to prove termination and reads checks (such checks were previously omitted)
* Beefed up Test/dafny0/SchorrWaite.dfy to use datatypes to specify that no garbage gets marked. The full-functional total-correctness verification of this Schorr-Waite method now takes about 3.2 seconds.
| -rw-r--r-- | Dafny/Dafny.atg | 60 | ||||
| -rw-r--r-- | Dafny/DafnyAst.ssc | 36 | ||||
| -rw-r--r-- | Dafny/Parser.ssc | 339 | ||||
| -rw-r--r-- | Dafny/Printer.ssc | 9 | ||||
| -rw-r--r-- | Dafny/Resolver.ssc | 22 | ||||
| -rw-r--r-- | Dafny/Scanner.ssc | 40 | ||||
| -rw-r--r-- | Dafny/Translator.ssc | 426 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/Answer | 4 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b5.dfy | 4 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b8.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 32 | ||||
| -rw-r--r-- | Test/dafny0/BinaryTree.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny0/DTypes.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny0/ListContents.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny0/ListCopy.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny0/ListReverse.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny0/Queue.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/SchorrWaite.dfy | 43 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 5 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 18 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
22 files changed, 699 insertions, 378 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 2bf7c1e3..265ae01b 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -375,6 +375,7 @@ FunctionDecl<out Function! f> Type! returnType;
List<Expression!> reqs = new List<Expression!>();
List<Expression!> reads = new List<Expression!>();
+ List<Expression!> decreases = new List<Expression!>();
Expression! bb; Expression body = null;
bool use = false;
.)
@@ -388,26 +389,44 @@ FunctionDecl<out Function! f> ":"
Type<out returnType>
( ";"
- { FunctionSpec<reqs, reads> }
- | { FunctionSpec<reqs, reads> }
+ { FunctionSpec<reqs, reads, decreases> }
+ | { FunctionSpec<reqs, reads, decreases> }
FunctionBody<out bb> (. body = bb; .)
)
(. parseVarScope.PopMarker();
- f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, body, attrs);
+ f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
.)
.
-FunctionSpec<List<Expression!\>! reqs, List<Expression!\>! reads>
+FunctionSpec<List<Expression!\>! reqs, List<Expression!\>! reads, List<Expression!\>! decreases>
= (. Expression! e; .)
( "requires" Expression<out e> ";" (. reqs.Add(e); .)
- | ReadsClause<reads>
+ | "reads" [ PossiblyWildExpressions<reads> ] ";"
+ | "decreases" Expressions<decreases> ";"
)
.
-ReadsClause<List<Expression!\>! reads>
-= "reads"
- [ Expressions<reads> ]
- ";"
+PossiblyWildExpressions<List<Expression!\>! args>
+= (. Expression! e; .)
+ PossiblyWildExpression<out e> (. args.Add(e); .)
+ { "," PossiblyWildExpression<out e> (. args.Add(e); .)
+ }
+ .
+
+PossiblyWildExpression<out Expression! e>
+= (. e = dummyExpr; .)
+ /* A reads clause can list a wildcard, which allows the enclosing function to
+ * read anything. In many cases, and in particular in all cases where
+ * the function is defined recursively, this makes it next to impossible to make
+ * any use of the function. Nevertheless, as an experimental feature, the
+ * language allows it (and it is sound).
+ */
+ /* A decreases clause on a loop asks that no termination check be performed.
+ * Use of this feature is sound only with respect to partial correctness.
+ */
+ ( "*" (. e = new WildcardExpr(token); .)
+ | Expression<out e>
+ )
.
FunctionBody<out Expression! e>
@@ -447,6 +466,7 @@ MatchExpression<out Expression! e> "match" (. x = token; .)
Expression<out e>
( "{" CaseExpressions<cases> "}" /* curly braces are optional; in the future, when match expressions can be nested, this will be handy */
+ /* Note, because the curly braces are optional, Coco generates a "CaseExpressions deletable" warning, but that's okay. */
| CaseExpressions<cases>
)
(. e = new MatchExpr(x, e, cases); .)
@@ -627,21 +647,13 @@ WhileStmt<out Statement! stmt> .)
"while" (. x = token; .)
Guard<out guard> (. assume guard == null || Owner.None(guard); .)
- {( (. isFree = false; .)
- [ "free" (. isFree = true; .)
- ]
- "invariant"
- Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
- ";"
- )
- |
- (
- "decreases"
- Expression<out e> (. decreases.Add(e); .)
- { "," Expression<out e> (. decreases.Add(e); .)
- }
- ";"
- )
+ { (. isFree = false; .)
+ [ "free" (. isFree = true; .)
+ ]
+ "invariant"
+ Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
+ ";"
+ | "decreases" PossiblyWildExpressions<decreases> ";"
}
BlockStmt<out body> (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
.
diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc index 831cc424..9a121b01 100644 --- a/Dafny/DafnyAst.ssc +++ b/Dafny/DafnyAst.ssc @@ -463,16 +463,18 @@ namespace Microsoft.Dafny public readonly Type! ResultType;
public readonly List<Expression!>! Req;
public readonly List<Expression!>! Reads;
+ public readonly List<Expression!>! Decreases;
public readonly Expression Body; // an extended expression
public Function(Token! tok, string! name, bool use, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
- List<Expression!>! req, List<Expression!>! reads, Expression body, Attributes attributes) {
+ List<Expression!>! req, List<Expression!>! reads, List<Expression!>! decreases, Expression body, Attributes attributes) {
this.Use = use;
this.TypeArgs = typeArgs;
this.Formals = formals;
this.ResultType = resultType;
this.Req = req;
this.Reads = reads;
+ this.Decreases = decreases;
this.Body = body;
base(tok, name, attributes);
}
@@ -1100,6 +1102,25 @@ namespace Microsoft.Dafny }
}
+ public class WildcardExpr : Expression { // a WildcardExpr can occur only in reads clauses and a loop's decreases clauses (with different meanings)
+ public WildcardExpr(Token! tok) {
+ base(tok);
+ }
+ }
+
+ public class ITEExpr : Expression { // an ITEExpr is an "extended expression" and is only allowed in certain places
+ public readonly Expression! Test;
+ public readonly Expression! Thn;
+ public readonly Expression! Els;
+
+ public ITEExpr(Token! tok, Expression! test, Expression! thn, Expression! els) {
+ this.Test = test;
+ this.Thn = thn;
+ this.Els = els;
+ base(tok);
+ }
+ }
+
public class MatchExpr : Expression { // a MatchExpr is an "extended expression" and is only allowed in certain places
public readonly Expression! Source;
public readonly List<MatchCase!>! Cases;
@@ -1126,19 +1147,6 @@ namespace Microsoft.Dafny }
}
- public class ITEExpr : Expression { // an ITEExpr is an "extended expression" and is only allowed in certain places
- public readonly Expression! Test;
- public readonly Expression! Thn;
- public readonly Expression! Els;
-
- public ITEExpr(Token! tok, Expression! test, Expression! thn, Expression! els) {
- this.Test = test;
- this.Thn = thn;
- this.Els = els;
- base(tok);
- }
- }
-
public class MaybeFreeExpression {
public readonly Expression! E;
public readonly bool IsFree;
diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc index 7a5f78ef..5180d413 100644 --- a/Dafny/Parser.ssc +++ b/Dafny/Parser.ssc @@ -255,6 +255,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Type! returnType;
List<Expression!> reqs = new List<Expression!>();
List<Expression!> reads = new List<Expression!>();
+ List<Expression!> decreases = new List<Expression!>();
Expression! bb; Expression body = null;
bool use = false;
@@ -276,18 +277,18 @@ public static int Parse (List<TopLevelDecl!>! classes) { Type(out returnType);
if (t.kind == 8) {
Get();
- while (t.kind == 19 || t.kind == 30) {
- FunctionSpec(reqs, reads);
+ while (t.kind == 19 || t.kind == 30 || t.kind == 31) {
+ FunctionSpec(reqs, reads, decreases);
}
- } else if (t.kind == 5 || t.kind == 19 || t.kind == 30) {
- while (t.kind == 19 || t.kind == 30) {
- FunctionSpec(reqs, reads);
+ } else if (StartOf(2)) {
+ while (t.kind == 19 || t.kind == 30 || t.kind == 31) {
+ FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
body = bb;
} else Error(94);
parseVarScope.PopMarker();
- f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, body, attrs);
+ f = new Function(id, id.val, use, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
}
@@ -318,11 +319,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
if (t.kind == 8) {
Get();
- while (StartOf(2)) {
+ while (StartOf(3)) {
MethodSpec(req, mod, ens);
}
- } else if (StartOf(3)) {
- while (StartOf(2)) {
+ } else if (StartOf(4)) {
+ while (StartOf(3)) {
MethodSpec(req, mod, ens);
}
BlockStmt(out bb);
@@ -372,7 +373,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void FormalsOptionalIds(List<Formal!>! formals) {
Token! id; Type! ty; string! name;
Expect(21);
- if (StartOf(4)) {
+ if (StartOf(5)) {
TypeIdentOptional(out id, out name, out ty);
formals.Add(new Formal(id, name, ty, true)); parseVarScope.Push(name, name);
while (t.kind == 10) {
@@ -482,7 +483,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { if (t.kind == 17) {
Get();
- if (StartOf(5)) {
+ if (StartOf(6)) {
Expression(out e);
mod.Add(e);
while (t.kind == 10) {
@@ -519,7 +520,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { parseVarScope.PushMarker();
Expect(5);
x = token;
- while (StartOf(6)) {
+ while (StartOf(7)) {
Stmt(body);
}
Expect(6);
@@ -568,7 +569,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else Error(99);
}
- static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads) {
+ static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads, List<Expression!>! decreases) {
Expression! e;
if (t.kind == 19) {
Get();
@@ -576,29 +577,40 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(8);
reqs.Add(e);
} else if (t.kind == 30) {
- ReadsClause(reads);
+ Get();
+ if (StartOf(8)) {
+ PossiblyWildExpressions(reads);
+ }
+ Expect(8);
+ } else if (t.kind == 31) {
+ Get();
+ Expressions(decreases);
+ Expect(8);
} else Error(100);
}
static void FunctionBody(out Expression! e) {
e = dummyExpr;
Expect(5);
- if (t.kind == 31) {
+ if (t.kind == 33) {
IfThenElseExpr(out e);
- } else if (t.kind == 33) {
+ } else if (t.kind == 35) {
MatchExpression(out e);
- } else if (StartOf(5)) {
+ } else if (StartOf(6)) {
Expression(out e);
} else Error(101);
Expect(6);
}
- static void ReadsClause(List<Expression!>! reads) {
- Expect(30);
- if (StartOf(5)) {
- Expressions(reads);
+ static void PossiblyWildExpressions(List<Expression!>! args) {
+ Expression! e;
+ PossiblyWildExpression(out e);
+ args.Add(e);
+ while (t.kind == 10) {
+ Get();
+ PossiblyWildExpression(out e);
+ args.Add(e);
}
- Expect(8);
}
static void Expressions(List<Expression!>! args) {
@@ -612,20 +624,30 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
}
+ static void PossiblyWildExpression(out Expression! e) {
+ e = dummyExpr;
+ if (t.kind == 32) {
+ Get();
+ e = new WildcardExpr(token);
+ } else if (StartOf(6)) {
+ Expression(out e);
+ } else Error(102);
+ }
+
static void IfThenElseExpr(out Expression! e) {
Token! x; Expression! e0; Expression! e1 = dummyExpr;
- Expect(31);
+ Expect(33);
x = token;
Expect(21);
Expression(out e);
Expect(22);
ExtendedExpr(out e0);
- Expect(32);
- if (t.kind == 31) {
+ Expect(34);
+ if (t.kind == 33) {
IfThenElseExpr(out e1);
} else if (t.kind == 5) {
ExtendedExpr(out e1);
- } else Error(102);
+ } else Error(103);
e = new ITEExpr(x, e, e0, e1);
}
@@ -633,33 +655,33 @@ public static int Parse (List<TopLevelDecl!>! classes) { Token! x;
List<MatchCase!> cases = new List<MatchCase!>();
- Expect(33);
+ Expect(35);
x = token;
Expression(out e);
if (t.kind == 5) {
Get();
CaseExpressions(cases);
Expect(6);
- } else if (t.kind == 6 || t.kind == 34) {
+ } else if (t.kind == 6 || t.kind == 36) {
CaseExpressions(cases);
- } else Error(103);
+ } else Error(104);
e = new MatchExpr(x, e, cases);
}
static void ExtendedExpr(out Expression! e) {
e = dummyExpr;
Expect(5);
- if (t.kind == 31) {
+ if (t.kind == 33) {
IfThenElseExpr(out e);
- } else if (StartOf(5)) {
+ } else if (StartOf(6)) {
Expression(out e);
- } else Error(104);
+ } else Error(105);
Expect(6);
}
static void CaseExpressions(List<MatchCase!>! cases) {
MatchCase! c;
- while (t.kind == 34) {
+ while (t.kind == 36) {
CaseExpression(out c);
cases.Add(c);
}
@@ -670,7 +692,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { List<BoundVar!> arguments = new List<BoundVar!>();
Expression! body;
- Expect(34);
+ Expect(36);
x = token; parseVarScope.PushMarker();
Ident(out id);
if (t.kind == 21) {
@@ -686,7 +708,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
Expect(22);
}
- Expect(35);
+ Expect(37);
Expression(out body);
c = new MatchCase(x, id.val, arguments, body);
parseVarScope.PopMarker();
@@ -698,12 +720,12 @@ public static int Parse (List<TopLevelDecl!>! classes) { BlockStmt(out s);
ss.Add(s);
}
- if (StartOf(7)) {
+ if (StartOf(9)) {
OneStmt(out s);
ss.Add(s);
} else if (t.kind == 9) {
VarDeclStmts(ss);
- } else Error(105);
+ } else Error(106);
}
static void OneStmt(out Statement! s) {
@@ -727,7 +749,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { AssignStmt(out s);
break;
}
- case 41: {
+ case 43: {
HavocStmt(out s);
break;
}
@@ -735,11 +757,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { CallStmt(out s);
break;
}
- case 31: {
+ case 33: {
IfStmt(out s);
break;
}
- case 42: {
+ case 44: {
WhileStmt(out s);
break;
}
@@ -747,7 +769,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { ForeachStmt(out s);
break;
}
- case 36: {
+ case 38: {
Get();
x = token;
Ident(out id);
@@ -755,7 +777,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { s = new LabelStmt(x, id.val);
break;
}
- case 37: {
+ case 39: {
Get();
x = token;
if (t.kind == 1) {
@@ -766,14 +788,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { s = new BreakStmt(x, label);
break;
}
- case 38: {
+ case 40: {
Get();
x = token;
Expect(8);
s = new ReturnStmt(x);
break;
}
- default: Error(106); break;
+ default: Error(107); break;
}
}
@@ -825,7 +847,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { s = dummyStmt;
LhsExpr(out lhs);
- Expect(39);
+ Expect(41);
x = token;
AssignRhs(out rhs, out ty);
if (rhs != null) {
@@ -840,7 +862,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void HavocStmt(out Statement! s) {
Token! x; Expression! lhs;
- Expect(41);
+ Expect(43);
x = token;
LhsExpr(out lhs);
Expect(8);
@@ -856,7 +878,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(46);
x = token;
CallStmtSubExpr(out e);
- if (t.kind == 10 || t.kind == 39) {
+ if (t.kind == 10 || t.kind == 41) {
if (t.kind == 10) {
Get();
e = ConvertToLocal(e);
@@ -875,7 +897,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(39);
+ Expect(41);
CallStmtSubExpr(out e);
} else {
Get();
@@ -909,19 +931,19 @@ public static int Parse (List<TopLevelDecl!>! classes) { Statement! s;
Statement els = null;
- Expect(31);
+ Expect(33);
x = token;
Guard(out guard);
BlockStmt(out thn);
- if (t.kind == 32) {
+ if (t.kind == 34) {
Get();
- if (t.kind == 31) {
+ if (t.kind == 33) {
IfStmt(out s);
els = s;
} else if (t.kind == 5) {
BlockStmt(out s);
els = s;
- } else Error(107);
+ } else Error(108);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -934,30 +956,24 @@ public static int Parse (List<TopLevelDecl!>! classes) { List<Expression!> decreases = new List<Expression!>();
Statement! body;
- Expect(42);
+ Expect(44);
x = token;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 18 || t.kind == 43 || t.kind == 44) {
- if (t.kind == 18 || t.kind == 43) {
+ while (t.kind == 18 || t.kind == 31 || t.kind == 45) {
+ if (t.kind == 18 || t.kind == 45) {
isFree = false;
if (t.kind == 18) {
Get();
isFree = true;
}
- Expect(43);
+ Expect(45);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(8);
} else {
Get();
- Expression(out e);
- decreases.Add(e);
- while (t.kind == 10) {
- Get();
- Expression(out e);
- decreases.Add(e);
- }
+ PossiblyWildExpressions(decreases);
Expect(8);
}
}
@@ -1006,13 +1022,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
}
}
- if (StartOf(5)) {
+ if (StartOf(6)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (t.kind == 41) {
+ } else if (t.kind == 43) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(108);
+ } else Error(109);
Expect(6);
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
parseVarScope.PopMarker();
@@ -1026,14 +1042,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { Token! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (t.kind == 40) {
+ if (t.kind == 42) {
Get();
ReferenceType(out x, out tt);
ty = tt;
- } else if (StartOf(5)) {
+ } else if (StartOf(6)) {
Expression(out ee);
e = ee;
- } else Error(109);
+ } else Error(110);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1048,7 +1064,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Type(out ty);
optionalType = ty;
}
- if (t.kind == 39) {
+ if (t.kind == 41) {
Get();
AssignRhs(out rhs, out newType);
}
@@ -1067,13 +1083,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void Guard(out Expression e) {
Expression! ee; e = null;
Expect(21);
- if (t.kind == 45) {
+ if (t.kind == 32) {
Get();
e = null;
- } else if (StartOf(5)) {
+ } else if (StartOf(6)) {
Expression(out ee);
e = ee;
- } else Error(110);
+ } else Error(111);
Expect(22);
}
@@ -1084,7 +1100,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (t.kind == 21 || t.kind == 84 || t.kind == 85) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(111);
+ } else Error(112);
while (t.kind == 79 || t.kind == 81) {
SelectOrCallSuffix(ref e);
}
@@ -1106,13 +1122,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
} else if (t.kind == 53) {
Get();
- } else Error(112);
+ } else Error(113);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
- if (StartOf(8)) {
+ if (StartOf(10)) {
if (t.kind == 56 || t.kind == 57) {
AndOp();
x = token;
@@ -1144,13 +1160,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
} else if (t.kind == 55) {
Get();
- } else Error(113);
+ } else Error(114);
}
static void RelationalExpression(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Term(out e0);
- if (StartOf(9)) {
+ if (StartOf(11)) {
RelOp(out x, out op);
Term(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1162,7 +1178,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
} else if (t.kind == 57) {
Get();
- } else Error(114);
+ } else Error(115);
}
static void OrOp() {
@@ -1170,7 +1186,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
} else if (t.kind == 59) {
Get();
- } else Error(115);
+ } else Error(116);
}
static void Term(out Expression! e0) {
@@ -1246,14 +1262,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(116); break;
+ default: Error(117); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 45 || t.kind == 71 || t.kind == 72) {
+ while (t.kind == 32 || t.kind == 71 || t.kind == 72) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1268,7 +1284,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (t.kind == 70) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(117);
+ } else Error(118);
}
static void UnaryExpression(out Expression! e) {
@@ -1283,16 +1299,16 @@ public static int Parse (List<TopLevelDecl!>! classes) { x = token;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
- } else if (StartOf(10)) {
+ } else if (StartOf(12)) {
SelectExpression(out e);
- } else if (StartOf(11)) {
+ } else if (StartOf(13)) {
ConstAtomExpression(out e);
- } else Error(118);
+ } else Error(119);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 45) {
+ if (t.kind == 32) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
} else if (t.kind == 71) {
@@ -1301,7 +1317,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (t.kind == 72) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(119);
+ } else Error(120);
}
static void NegOp() {
@@ -1309,7 +1325,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
} else if (t.kind == 74) {
Get();
- } else Error(120);
+ } else Error(121);
}
static void SelectExpression(out Expression! e) {
@@ -1318,7 +1334,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { IdentOrFuncExpression(out e);
} else if (t.kind == 21 || t.kind == 84 || t.kind == 85) {
ObjectExpression(out e);
- } else Error(121);
+ } else Error(122);
while (t.kind == 79 || t.kind == 81) {
SelectOrCallSuffix(ref e);
}
@@ -1358,7 +1374,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { elements = new List<Expression!>();
if (t.kind == 21) {
Get();
- if (StartOf(5)) {
+ if (StartOf(6)) {
Expressions(elements);
}
Expect(22);
@@ -1386,7 +1402,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { case 5: {
Get();
x = token; elements = new List<Expression!>();
- if (StartOf(5)) {
+ if (StartOf(6)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
@@ -1396,14 +1412,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { case 81: {
Get();
x = token; elements = new List<Expression!>();
- if (StartOf(5)) {
+ if (StartOf(6)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
Expect(82);
break;
}
- default: Error(122); break;
+ default: Error(123); break;
}
}
@@ -1424,7 +1440,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { if (t.kind == 21) {
Get();
args = new List<Expression!>();
- if (StartOf(5)) {
+ if (StartOf(6)) {
Expressions(args);
}
Expect(22);
@@ -1454,13 +1470,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { e = new OldExpr(x, e);
} else if (t.kind == 21) {
Get();
- if (StartOf(12)) {
+ if (StartOf(14)) {
QuantifierGuts(out e);
- } else if (StartOf(5)) {
+ } else if (StartOf(6)) {
Expression(out e);
- } else Error(123);
+ } else Error(124);
Expect(22);
- } else Error(124);
+ } else Error(125);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1474,7 +1490,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { if (t.kind == 21) {
Get();
args = new List<Expression!>(); func = true;
- if (StartOf(5)) {
+ if (StartOf(6)) {
Expressions(args);
}
Expect(22);
@@ -1484,14 +1500,14 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (t.kind == 81) {
Get();
x = token;
- if (StartOf(5)) {
+ if (StartOf(6)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 39 || t.kind == 83) {
+ if (t.kind == 41 || t.kind == 83) {
if (t.kind == 83) {
Get();
anyDots = true;
- if (StartOf(5)) {
+ if (StartOf(6)) {
Expression(out ee);
e1 = ee;
}
@@ -1505,7 +1521,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(125);
+ } else Error(126);
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
@@ -1519,7 +1535,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
Expect(82);
- } else Error(126);
+ } else Error(127);
}
static void QuantifierGuts(out Expression! q) {
@@ -1538,7 +1554,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { } else if (t.kind == 88 || t.kind == 89) {
Exists();
x = token;
- } else Error(127);
+ } else Error(128);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1566,7 +1582,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
} else if (t.kind == 87) {
Get();
- } else Error(128);
+ } else Error(129);
}
static void Exists() {
@@ -1574,7 +1590,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
} else if (t.kind == 89) {
Get();
- } else Error(129);
+ } else Error(130);
}
static void QSep() {
@@ -1582,7 +1598,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Get();
} else if (t.kind == 91) {
Get();
- } else Error(130);
+ } else Error(131);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1591,11 +1607,11 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(5);
if (t.kind == 11) {
AttributeBody(ref attrs);
- } else if (StartOf(5)) {
+ } else if (StartOf(6)) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(131);
+ } else Error(132);
Expect(6);
}
@@ -1607,7 +1623,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expect(11);
Expect(1);
aName = token.val;
- if (StartOf(13)) {
+ if (StartOf(15)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (t.kind == 10) {
@@ -1624,10 +1640,10 @@ public static int Parse (List<TopLevelDecl!>! classes) { if (t.kind == 3) {
Get();
arg = new Attributes.Argument(token.val.Substring(1, token.val.Length-2));
- } else if (StartOf(5)) {
+ } else if (StartOf(6)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(132);
+ } else Error(133);
}
@@ -1677,21 +1693,21 @@ public static int Parse (List<TopLevelDecl!>! classes) { case 28: s = "function expected"; break;
case 29: s = "use expected"; break;
case 30: s = "reads expected"; break;
- case 31: s = "if expected"; break;
- case 32: s = "else expected"; break;
- case 33: s = "match expected"; break;
- case 34: s = "case expected"; break;
- case 35: s = "=> expected"; break;
- case 36: s = "label expected"; break;
- case 37: s = "break expected"; break;
- case 38: s = "return expected"; break;
- case 39: s = ":= expected"; break;
- case 40: s = "new expected"; break;
- case 41: s = "havoc expected"; break;
- case 42: s = "while expected"; break;
- case 43: s = "invariant expected"; break;
- case 44: s = "decreases expected"; break;
- case 45: s = "* expected"; break;
+ case 31: s = "decreases expected"; break;
+ case 32: s = "* expected"; break;
+ case 33: s = "if expected"; break;
+ case 34: s = "else expected"; break;
+ case 35: s = "match expected"; break;
+ case 36: s = "case expected"; break;
+ case 37: s = "=> expected"; break;
+ case 38: s = "label expected"; break;
+ case 39: s = "break expected"; break;
+ case 40: s = "return expected"; break;
+ case 41: s = ":= expected"; break;
+ case 42: s = "new expected"; break;
+ case 43: s = "havoc expected"; break;
+ case 44: s = "while expected"; break;
+ case 45: s = "invariant expected"; break;
case 46: s = "call expected"; break;
case 47: s = "foreach expected"; break;
case 48: s = "in expected"; break;
@@ -1748,37 +1764,38 @@ public static int Parse (List<TopLevelDecl!>! classes) { case 99: s = "invalid ReferenceType"; break;
case 100: s = "invalid FunctionSpec"; break;
case 101: s = "invalid FunctionBody"; break;
- case 102: s = "invalid IfThenElseExpr"; break;
- case 103: s = "invalid MatchExpression"; break;
- case 104: s = "invalid ExtendedExpr"; break;
- case 105: s = "invalid Stmt"; break;
- case 106: s = "invalid OneStmt"; break;
- case 107: s = "invalid IfStmt"; break;
- case 108: s = "invalid ForeachStmt"; break;
- case 109: s = "invalid AssignRhs"; break;
- case 110: s = "invalid Guard"; break;
- case 111: s = "invalid CallStmtSubExpr"; break;
- case 112: s = "invalid EquivOp"; break;
- case 113: s = "invalid ImpliesOp"; break;
- case 114: s = "invalid AndOp"; break;
- case 115: s = "invalid OrOp"; break;
- case 116: s = "invalid RelOp"; break;
- case 117: s = "invalid AddOp"; break;
- case 118: s = "invalid UnaryExpression"; break;
- case 119: s = "invalid MulOp"; break;
- case 120: s = "invalid NegOp"; break;
- case 121: s = "invalid SelectExpression"; break;
- case 122: s = "invalid ConstAtomExpression"; break;
- case 123: s = "invalid ObjectExpression"; break;
+ case 102: s = "invalid PossiblyWildExpression"; break;
+ case 103: s = "invalid IfThenElseExpr"; break;
+ case 104: s = "invalid MatchExpression"; break;
+ case 105: s = "invalid ExtendedExpr"; break;
+ case 106: s = "invalid Stmt"; break;
+ case 107: s = "invalid OneStmt"; break;
+ case 108: s = "invalid IfStmt"; break;
+ case 109: s = "invalid ForeachStmt"; break;
+ case 110: s = "invalid AssignRhs"; break;
+ case 111: s = "invalid Guard"; break;
+ case 112: s = "invalid CallStmtSubExpr"; break;
+ case 113: s = "invalid EquivOp"; break;
+ case 114: s = "invalid ImpliesOp"; break;
+ case 115: s = "invalid AndOp"; break;
+ case 116: s = "invalid OrOp"; break;
+ case 117: s = "invalid RelOp"; break;
+ case 118: s = "invalid AddOp"; break;
+ case 119: s = "invalid UnaryExpression"; break;
+ case 120: s = "invalid MulOp"; break;
+ case 121: s = "invalid NegOp"; break;
+ case 122: s = "invalid SelectExpression"; break;
+ case 123: s = "invalid ConstAtomExpression"; break;
case 124: s = "invalid ObjectExpression"; break;
- case 125: s = "invalid SelectOrCallSuffix"; break;
+ case 125: s = "invalid ObjectExpression"; break;
case 126: s = "invalid SelectOrCallSuffix"; break;
- case 127: s = "invalid QuantifierGuts"; break;
- case 128: s = "invalid Forall"; break;
- case 129: s = "invalid Exists"; break;
- case 130: s = "invalid QSep"; break;
- case 131: s = "invalid AttributeOrTrigger"; break;
- case 132: s = "invalid AttributeArg"; break;
+ case 127: s = "invalid SelectOrCallSuffix"; break;
+ case 128: s = "invalid QuantifierGuts"; break;
+ case 129: s = "invalid Forall"; break;
+ case 130: s = "invalid Exists"; break;
+ case 131: s = "invalid QSep"; break;
+ case 132: s = "invalid AttributeOrTrigger"; break;
+ case 133: s = "invalid AttributeArg"; break;
default: s = "error " + n; break;
}
@@ -1788,12 +1805,14 @@ 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,x,x,x, x,T,x,x, x,x,T,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,T, 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,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,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,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,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, 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,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,T, x,x,x,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, 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,T,x,x, x,x,x,x, x,T,x,T, x,x,x,x, T,T,T,x, x,T,T,x, x,x,T,T, x,T,T,T, 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,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,T,T, T,x,x,T, T,x,T,T, x,T,T,T, 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,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,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,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,T,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,x,T,T, T,x,x,T, T,x,T,T, x,T,T,T, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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, 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, T,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,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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},
diff --git a/Dafny/Printer.ssc b/Dafny/Printer.ssc index 26a7b965..d676c942 100644 --- a/Dafny/Printer.ssc +++ b/Dafny/Printer.ssc @@ -143,6 +143,12 @@ namespace Microsoft.Dafny { PrintExpression(r);
wr.WriteLine(";");
}
+ foreach (Expression r in f.Decreases) {
+ Indent(2 * IndentAmount);
+ wr.Write("decreases ");
+ PrintExpression(r);
+ wr.WriteLine(";");
+ }
if (f.Body != null) {
Indent(IndentAmount);
PrintExtendedExpr(f.Body, IndentAmount);
@@ -718,6 +724,9 @@ namespace Microsoft.Dafny { }
wr.Write(")");
+ } else if (expr is WildcardExpr) {
+ wr.Write("*");
+
} else if (expr is ITEExpr) {
assert false; // ITE is an extended expression and should be printed only using PrintExtendedExpr
} else if (expr is MatchExpr) {
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc index c89e925a..5eca038e 100644 --- a/Dafny/Resolver.ssc +++ b/Dafny/Resolver.ssc @@ -267,6 +267,10 @@ namespace Microsoft.Dafny { Error(r, "a reads-clause expression must denote an object or a collection of objects (instead got {0})", r.Type);
}
}
+ foreach (Expression r in f.Decreases) {
+ ResolveExpression(r, false);
+ // any type is fine
+ }
if (f.Body != null) {
ResolveExpression(f.Body, false);
assert f.Body.Type != null; // follows from postcondition of ResolveExpression
@@ -795,10 +799,16 @@ namespace Microsoft.Dafny { }
// type check the arguments
for (int i = 0; i < method.Ins.Count; i++) {
- UnifyTypes((!)s.Args[i].Type, SubstType(method.Ins[i].Type, subst));
+ Type st = SubstType(method.Ins[i].Type, subst);
+ if (!UnifyTypes((!)s.Args[i].Type, st)) {
+ Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
+ }
}
for (int i = 0; i < method.Outs.Count; i++) {
- UnifyTypes((!)s.Lhs[i].Type, SubstType(method.Outs[i].Type, subst));
+ Type st = SubstType(method.Outs[i].Type, subst);
+ if (!UnifyTypes((!)s.Lhs[i].Type, st)) {
+ Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, s.Lhs[i].Type);
+ }
}
}
}
@@ -1202,7 +1212,10 @@ namespace Microsoft.Dafny { Expression farg = e.Args[i];
ResolveExpression(farg, twoState);
assert farg.Type != null; // follows from postcondition of ResolveExpression
- UnifyTypes(farg.Type, SubstType(function.Formals[i].Type, subst));
+ Type s = SubstType(function.Formals[i].Type, subst);
+ if (!UnifyTypes(farg.Type, s)) {
+ Error(expr, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
+ }
}
expr.Type = SubstType(function.ResultType, subst);
}
@@ -1384,6 +1397,9 @@ namespace Microsoft.Dafny { scope.PopMarker();
expr.Type = Type.Bool;
+ } else if (expr is WildcardExpr) {
+ expr.Type = new SetType(new ObjectType());
+
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
assert !twoState;
diff --git a/Dafny/Scanner.ssc b/Dafny/Scanner.ssc index 1e0e8e8f..2d38d972 100644 --- a/Dafny/Scanner.ssc +++ b/Dafny/Scanner.ssc @@ -39,7 +39,7 @@ public class Scanner { start[39] = 1;
start[40] = 12;
start[41] = 13;
- start[42] = 17;
+ start[42] = 14;
start[43] = 40;
start[44] = 8;
start[45] = 41;
@@ -58,7 +58,7 @@ public class Scanner { start[58] = 9;
start[59] = 7;
start[60] = 10;
- start[61] = 14;
+ start[61] = 15;
start[62] = 11;
start[63] = 1;
start[65] = 1;
@@ -293,18 +293,18 @@ public class Scanner { case "function": t.kind = 28; break;
case "use": t.kind = 29; break;
case "reads": t.kind = 30; break;
- case "if": t.kind = 31; break;
- case "else": t.kind = 32; break;
- case "match": t.kind = 33; break;
- case "case": t.kind = 34; break;
- case "label": t.kind = 36; break;
- case "break": t.kind = 37; break;
- case "return": t.kind = 38; break;
- case "new": t.kind = 40; break;
- case "havoc": t.kind = 41; break;
- case "while": t.kind = 42; break;
- case "invariant": t.kind = 43; break;
- case "decreases": t.kind = 44; break;
+ case "decreases": t.kind = 31; break;
+ case "if": t.kind = 33; break;
+ case "else": t.kind = 34; break;
+ case "match": t.kind = 35; break;
+ case "case": t.kind = 36; break;
+ case "label": t.kind = 38; break;
+ case "break": t.kind = 39; break;
+ case "return": t.kind = 40; break;
+ case "new": t.kind = 42; break;
+ case "havoc": t.kind = 43; break;
+ case "while": t.kind = 44; break;
+ case "invariant": t.kind = 45; break;
case "call": t.kind = 46; break;
case "foreach": t.kind = 47; break;
case "in": t.kind = 48; break;
@@ -355,7 +355,7 @@ public class Scanner { case 8:
{t.kind = 10; goto done;}
case 9:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 16;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}
else if (ch == ':') {buf.Append(ch); NextCh(); goto case 52;}
else {t.kind = 11; goto done;}
case 10:
@@ -369,15 +369,15 @@ public class Scanner { case 13:
{t.kind = 22; goto done;}
case 14:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 15;}
+ {t.kind = 32; goto done;}
+ case 15:
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 16;}
else if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
else {t.kind = noSym; goto done;}
- case 15:
- {t.kind = 35; goto done;}
case 16:
- {t.kind = 39; goto done;}
+ {t.kind = 37; goto done;}
case 17:
- {t.kind = 45; goto done;}
+ {t.kind = 41; goto done;}
case 18:
if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;}
else {t.kind = 49; goto done;}
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc index 6e9030c3..e490e8b4 100644 --- a/Dafny/Translator.ssc +++ b/Dafny/Translator.ssc @@ -283,10 +283,7 @@ namespace Microsoft.Dafny { } else if (member is Function) {
Function f = (Function)member;
AddFrameAxiom(f);
- // TODO: also need a well-formedness check for the preconditions
- if (f.Body != null) {
- AddWellformednessCheck(f);
- }
+ AddWellformednessCheck(f);
}
}
} else {
@@ -434,6 +431,8 @@ namespace Microsoft.Dafny { // the axiom. Moreover, leaving it out does not introduce any soundness problem, because the Dafny
// allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is
// sound after that, then it would also have been sound just before the allocation.
+ //
+ // TODO: Add a CanAssumeFunctionDefs antecedent to this axiom (see Dafny lecture notes from Marktoberdorf 2008).
Bpl.VariableSeq formals = new Bpl.VariableSeq();
Bpl.ExprSeq args = new Bpl.ExprSeq();
Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
@@ -490,7 +489,7 @@ namespace Microsoft.Dafny { assert r != null;
Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
substMap.Add(specializationFormal, r);
- body = Substitute(body, new ThisExpr(f.tok), substMap);
+ body = Substitute(body, null, substMap);
}
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.TrExpr(body))));
return new Bpl.Axiom(f.tok, ax);
@@ -671,13 +670,25 @@ namespace Microsoft.Dafny { /// <summary>
/// Generates:
- /// axiom (forall h0: [ref, Field x]x, h1: [ref, Field x]x, formals... ::
+ /// axiom (forall h0: HeapType, h1: HeapType, formals... ::
/// { F(h0,formals), F(h1,formals) }
- /// (forall(alpha) o: ref, f: Field alpha :: o != null AND h0[o,alloc] AND o in reads clause of formals in h0 IMPLIES h0[o,f] == h1[o,f]) AND
- /// (forall(alpha) o: ref, f: Field alpha :: o != null AND h1[o,alloc] AND o in reads clause of formals in h1 IMPLIES h0[o,f] == h1[o,f])
+ /// heaps are well-formed and formals are allocated
+ /// AND
+ /// (forall(alpha) o: ref, f: Field alpha ::
+ /// o != null AND h0[o,alloc] AND h1[o,alloc] AND
+ /// o in reads clause of formals in h0
+ /// IMPLIES h0[o,f] == h1[o,f])
+ /// AND
+ /// (forall(alpha) o: ref, f: Field alpha ::
+ /// o != null AND h1[o,alloc] AND h0[o,alloc] AND
+ /// o in reads clause of formals in h1
+ /// IMPLIES h0[o,f] == h1[o,f])
/// IMPLIES
/// F(h0,formals) == F(h1,formals)
/// );
+ /// Note, the second h?[o,alloc] in the antecedent of each inner forall above is sound
+ /// because user expressions are not allowed to quantify over all allocated objects, and
+ /// in particular, they have no way to depend on the .alloc field of an object.
/// </summary>
void AddFrameAxiom(Function! f)
requires sink != null && predef != null;
@@ -689,22 +700,25 @@ namespace Microsoft.Dafny { ExpressionTranslator etran0 = new ExpressionTranslator(this, predef, h0);
ExpressionTranslator etran1 = new ExpressionTranslator(this, predef, h1);
+ Bpl.Expr wellFormed = Bpl.Expr.And(
+ FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),
+ FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr));
+
Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");
Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));
Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);
Bpl.BoundVariable fieldVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$f", predef.FieldName(f.tok, alpha)));
Bpl.Expr field = new Bpl.IdentifierExpr(f.tok, fieldVar);
Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
- Bpl.Expr oNotNullAlloced0 = Bpl.Expr.And(oNotNull, etran0.IsAlloced(f.tok, o));
- Bpl.Expr oNotNullAlloced1 = Bpl.Expr.And(oNotNull, etran1.IsAlloced(f.tok, o));
+ Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));
Bpl.Expr unchanged = Bpl.Expr.Eq(Bpl.Expr.SelectTok(f.tok, h0, o, field), Bpl.Expr.SelectTok(f.tok, h1, o, field));
- Bpl.Expr r0 = InRWClause(f.tok, o, f.Reads, etran0);
- Bpl.Expr r1 = InRWClause(f.tok, o, f.Reads, etran1);
+ Bpl.Expr r0 = InRWClause(f.tok, o, f.Reads, etran0, null, null);
+ Bpl.Expr r1 = InRWClause(f.tok, o, f.Reads, etran1, null, null);
Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
- Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced0, r0), unchanged));
+ Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));
Bpl.Expr q1 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),
- Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced1, r1), unchanged));
+ Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r1), unchanged));
// bvars: h0, h1, formals
// f0args: h0, formals
@@ -717,12 +731,22 @@ namespace Microsoft.Dafny { bvars.Add(h0Var); bvars.Add(h1Var); bvars.Add(thVar);
f0args.Add(h0); f0args.Add(th);
f1args.Add(h1); f1args.Add(th);
+
+ Type thisType = Resolver.GetThisType(f.tok, (!)f.EnclosingClass);
+ Bpl.Expr wh = Bpl.Expr.And(Bpl.Expr.Neq(th, predef.Null),
+ Bpl.Expr.And(etran0.GoodRef(f.tok, th, thisType), etran1.GoodRef(f.tok, th, thisType)));
+ wellFormed = Bpl.Expr.And(wellFormed, wh);
+
foreach (Formal p in f.Formals) {
Bpl.BoundVariable bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
bvars.Add(bv);
Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);
f0args.Add(formal);
f1args.Add(formal);
+ wh = GetWhereClause(p.tok, formal, p.Type, etran0);
+ if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
+ wh = GetWhereClause(p.tok, formal, p.Type, etran1);
+ if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
}
Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
@@ -732,18 +756,30 @@ namespace Microsoft.Dafny { Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(F0, F1));
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr, Bpl.Expr.Imp(Bpl.Expr.And(q0, q1), eq));
+ Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,
+ Bpl.Expr.Imp(wellFormed,
+ Bpl.Expr.Imp(Bpl.Expr.And(q0, q1), eq)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, "frame axiom for " + f.FullName));
}
- Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, List<Expression!>! rw, ExpressionTranslator! etran)
+ Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, List<Expression!>! rw, ExpressionTranslator! etran,
+ Expression receiverReplacement, Dictionary<IVariable,Expression!> substMap)
requires predef != null;
// requires o to denote an expression of type RefType
+ // "rw" is is allowed to contain a WildcardExpr
+ requires receiverReplacement == null <==> substMap == null;
{
Bpl.Expr disjunction = null;
- foreach (Expression e in rw) {
+ foreach (Expression rwComponent in rw) {
+ Expression e = rwComponent;
+ if (substMap != null) {
+ assert receiverReplacement != null;
+ e = Substitute(e, receiverReplacement, substMap);
+ }
Bpl.Expr disjunct;
- if (e.Type is SetType) {
+ if (e is WildcardExpr) {
+ disjunct = Bpl.Expr.True;
+ } else if (e.Type is SetType) {
// old(e)[Box(o)]
disjunct = etran.TrInSet(tok, o, e, ((SetType)e.Type).Arg);
} else if (e.Type is SeqType) {
@@ -775,7 +811,6 @@ namespace Microsoft.Dafny { void AddWellformednessCheck(Function! f)
requires sink != null && predef != null;
- requires f.Body != null;
{
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
// parameters of the procedure
@@ -791,21 +826,30 @@ namespace Microsoft.Dafny { inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));
}
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
- // preconditions of the procedure
- Bpl.RequiresSeq req = new Bpl.RequiresSeq();
- string comment = "user-defined preconditions";
- foreach (Expression p in f.Req) {
- req.Add(Requires(p.tok, false, etran.TrExpr(p), null, comment));
- comment = null;
- }
// the procedure itself
Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),
- req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());
+ new Bpl.RequiresSeq(), new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());
sink.TopLevelDeclarations.Add(proc);
Bpl.VariableSeq locals = new Bpl.VariableSeq();
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
- CheckWellformed(f.Body, f, Position.Positive, locals, builder, etran);
+ // check well-formedness of the preconditions, and then assume each one of them
+ foreach (Expression p in f.Req) {
+ // Note, in this well-formedness check, function is passed in as null. This will cause there to be
+ // no reads checks or decreases checks. This seems like a good idea, and I hope it is also sound.
+ 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.
+ // check well-formedness of the decreases clauses
+ foreach (Expression p in f.Decreases) {
+ CheckWellformed(p, f, Position.Positive, locals, builder, etran);
+ }
+ // check well-formedness of the body
+ if (f.Body != null) {
+ CheckWellformed(f.Body, f, Position.Positive, locals, builder, etran);
+ }
Bpl.Implementation impl = new Bpl.Implementation(f.tok, proc.Name,
typeParams,
@@ -818,7 +862,7 @@ namespace Microsoft.Dafny { Bpl.Expr! IsTotal(Expression! expr, ExpressionTranslator! etran)
requires predef != null;
{
- if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr) {
+ if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {
return Bpl.Expr.True;
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
@@ -971,7 +1015,7 @@ namespace Microsoft.Dafny { CheckWellformed(e.Obj, func, Position.Neither, locals, builder, etran);
CheckNonNull(expr.tok, e.Obj, builder, etran);
if (func != null) {
- builder.Add(Assert(expr.tok, InRWClause(expr.tok, etran.TrExpr(e.Obj), func.Reads, etran), "insufficient reads clause to read field"));
+ builder.Add(Assert(expr.tok, InRWClause(expr.tok, etran.TrExpr(e.Obj), func.Reads, etran, null, null), "insufficient reads clause to read field"));
}
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
@@ -981,11 +1025,11 @@ namespace Microsoft.Dafny { if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
CheckWellformed(e.E0, func, Position.Neither, locals, builder, etran);
- builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, e0, seq, null, !e.SelectOne)));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, null, !e.SelectOne), "index out of range"));
}
if (e.E1 != null) {
CheckWellformed(e.E1, func, Position.Neither, locals, builder, etran);
- builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true)));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true), "end-of-range beyond length of sequence"));
}
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
@@ -993,17 +1037,102 @@ namespace Microsoft.Dafny { Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr index = etran.TrExpr(e.Index);
CheckWellformed(e.Index, func, Position.Neither, locals, builder, etran);
- builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, index, seq, null, false)));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, null, false), "index out of range"));
CheckWellformed(e.Value, func, Position.Neither, locals, builder, etran);
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
+ assert e.Function != null; // follows from the fact that expr has been successfully resolved
+ // check well-formedness of receiver
CheckWellformed(e.Receiver, func, Position.Neither, locals, builder, etran);
CheckNonNull(expr.tok, e.Receiver, builder, etran);
+ // check well-formedness of the other parameters
foreach (Expression arg in e.Args) {
CheckWellformed(arg, func, Position.Neither, locals, builder, etran);
}
- // TODO: check wellformedness of call (call.reads is subset of reads, and either e.Function returns a boolean and is in a positive position, or e.Function returns something else and the subset is a proper subset)
- // TODO: and check preconditions of call
+ // 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 < e.Function.Formals.Count; i++) {
+ Formal p = e.Function.Formals[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(e.Args[i]));
+ builder.Add(cmd);
+ }
+ // check that the preconditions for the call hold
+ foreach (Expression p in e.Function.Req) {
+ Expression precond = Substitute(p, e.Receiver, substMap);
+ builder.Add(Assert(expr.tok, etran.TrExpr(precond), "possible violation of function precondition"));
+ }
+ if (func != null) {
+ // check that the callee reads only what the caller is already allowed to read
+ // emit: assert (forall o: ref :: o != null && o in callee.reads ==> o in caller.reads);
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType));
+ Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);
+ Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
+ Bpl.Expr oInCallee = InRWClause(expr.tok, o, e.Function.Reads, etran, e.Receiver, substMap);
+ Bpl.Expr oInCaller = InRWClause(expr.tok, o, func.Reads, etran, null, null);
+ Bpl.Expr q = new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInCallee), oInCaller));
+ 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);
+ }
+ }
+ builder.Add(Assert(expr.tok, decrExpr, "failure to decrease termination measure"));
+ }
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
foreach (Expression arg in dtv.Arguments) {
@@ -1017,7 +1146,6 @@ namespace Microsoft.Dafny { } else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
CheckWellformed(e.E0, func, e.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp ? Negate(pos) : pos, locals, builder, etran);
-
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.And:
case BinaryExpr.ResolvedOpcode.Imp:
@@ -1050,7 +1178,7 @@ namespace Microsoft.Dafny { substMap.Add(bv, ie);
locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
}
- Expression body = Substitute(e.Body, new ThisExpr(expr.tok), substMap);
+ Expression body = Substitute(e.Body, null, substMap);
CheckWellformed(body, func, pos, locals, builder, etran);
} else if (expr is ITEExpr) {
@@ -1366,7 +1494,7 @@ namespace Microsoft.Dafny { Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.Old.IsAlloced(tok, o));
Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);
- consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, modifiesClause, etran.Old));
+ consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, modifiesClause, etran.Old, null, null));
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));
return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));
@@ -1417,7 +1545,7 @@ namespace Microsoft.Dafny { // ----- Statement ----------------------------------------------------------------------------
- Bpl.AssertCmd! Assert(Token! tok, Bpl.Expr! condition, string! errorMessage)
+ Bpl.AssertCmd! Assert(Bpl.IToken! tok, Bpl.Expr! condition, string! errorMessage)
{
Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition);
cmd.ErrorData = "Error: " + errorMessage;
@@ -1464,7 +1592,7 @@ namespace Microsoft.Dafny { int pieces = 0;
foreach (Expression p in SplitExpr(s.Expr, true)) {
builder.Add(Assert(stmt.Tok, IsTotal(p, etran), "assert condition must be well defined")); // totality check
- builder.Add(new Bpl.AssertCmd(stmt.Tok, etran.TrExpr(p)));
+ builder.Add(Assert(stmt.Tok, etran.TrExpr(p), "assertion violation"));
pieces++;
}
if (2 <= pieces) {
@@ -1644,7 +1772,7 @@ namespace Microsoft.Dafny { int pieces = 0;
if (!loopInv.IsFree) {
foreach (Expression se in SplitExpr(loopInv.E, true)) {
- invariants.Add(new Bpl.AssertCmd(se.tok, etran.TrExpr(se)));
+ invariants.Add(Assert(se.tok, etran.TrExpr(se), "loop invariant violation"));
pieces++;
}
}
@@ -1681,10 +1809,11 @@ namespace Microsoft.Dafny { loopBodyBuilder.Add(new Bpl.CallCmd(stmt.Tok, "CevStepEvent",
new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_entered", predef.CevEventType)),
new Bpl.IdentifierExprSeq()));
- if (s.Decreases.Count == 0) {
+ if (exists{Expression e in s.Decreases; e is WildcardExpr}) {
+ // omit termination checking for this loop
TrStmt(s.Body, loopBodyBuilder, locals, etran);
} else {
- List<Bpl.IdentifierExpr!> oldBfs = new List<Bpl.IdentifierExpr!>();
+ List<Bpl.Expr!> oldBfs = new List<Bpl.Expr!>();
int c = 0;
foreach (Expression e in s.Decreases) {
Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, "$decr" + loopId + "$" + c, TrType((!)e.Type)));
@@ -1692,7 +1821,7 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr bf = new Bpl.IdentifierExpr(e.tok, bfVar);
oldBfs.Add(bf);
// record value of each decreases expression at beginning of the loop iteration
- invariants.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at top of each loop iteration")); // totality check
+ loopBodyBuilder.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at top of each loop iteration")); // totality check
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(e.tok, bf, etran.TrExpr(e));
loopBodyBuilder.Add(cmd);
@@ -1701,84 +1830,18 @@ namespace Microsoft.Dafny { // time for the actual loop body
TrStmt(s.Body, loopBodyBuilder, locals, etran);
// check definedness of decreases expressions
+ List<Type!> types = new List<Type!>();
+ List<Bpl.Expr!> decrsTotal = new List<Bpl.Expr!>();
+ List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
foreach (Expression e in s.Decreases) {
// 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.
- loopBodyBuilder.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at end of loop iteration")); // totality check
- }
- // compute eq and less for each component of the lexicographic pair
- List<Bpl.Expr!> Eq = new List<Bpl.Expr!>();
- List<Bpl.Expr!> Less = new List<Bpl.Expr!>();
- for (int i = 0; i < s.Decreases.Count; i++) {
- Expression e = s.Decreases[i];
- Bpl.Expr d = etran.TrExpr(e);
- Bpl.IdentifierExpr bf = oldBfs[i];
-
- Bpl.Expr less;
- Bpl.Expr eq;
- Type ty = (!)e.Type;
- if (ty is BoolType) {
- eq = Bpl.Expr.Iff(d, bf);
- less = Bpl.Expr.And(Bpl.Expr.Not(d), bf);
- } else if (ty is IntType) {
- eq = Bpl.Expr.Eq(d, bf);
- less = Bpl.Expr.Lt(d, bf);
- } else if (ty is SetType) {
- eq = FunctionCall(stmt.Tok, BuiltinFunction.SetEqual, null, d, bf);
- less = etran.ProperSubset(stmt.Tok, d, bf);
- } else if (ty is SeqType) {
- Bpl.Expr e0 = FunctionCall(stmt.Tok, BuiltinFunction.SeqLength, null, d);
- Bpl.Expr e1 = FunctionCall(stmt.Tok, BuiltinFunction.SeqLength, null, bf);
- eq = Bpl.Expr.Eq(e0, e1);
- less = Bpl.Expr.Lt(e0, e1);
- } else if (ty.IsDatatype) {
- Bpl.Expr e0 = FunctionCall(stmt.Tok, BuiltinFunction.DtRank, null, d);
- Bpl.Expr e1 = FunctionCall(stmt.Tok, BuiltinFunction.DtRank, null, bf);
- eq = Bpl.Expr.Eq(e0, e1);
- less = Bpl.Expr.Lt(e0, e1);
-
- } else {
- // reference type
- Bpl.Expr e0 = Bpl.Expr.Neq(d, predef.Null);
- Bpl.Expr e1 = Bpl.Expr.Neq(bf, predef.Null);
- eq = Bpl.Expr.Iff(e0, e1);
- less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
- }
- Eq.Add(eq);
- Less.Add(less);
- }
- // check: 0 <= old(decreases)
- // more precisely, for component k of the lexicographic decreases function, check:
- // 0 <= old(dec(k)) || dec0 < old(dec0) || dec1 < old(dec1) || ... || dec(k-1) < old(dec((k-1) || old(dec(k)) == dec(k)
- for (int k = 0; k < s.Decreases.Count; k++) {
- Expression e = s.Decreases[k];
- // we only need to check lower bound for integers--sets, sequences, booleans, and references all have natural lower bounds
- if (e.Type is IntType) {
- Bpl.IdentifierExpr bf = oldBfs[k];
- Bpl.Expr bounded = Bpl.Expr.Le(Bpl.Expr.Literal(0), bf);
- for (int i = 0; i < k; i++) {
- bounded = Bpl.Expr.Or(bounded, Less[i]);
- }
- Bpl.Cmd cmd = Assert(e.tok, Bpl.Expr.Or(bounded, Eq[k]), "decreases expression must be bounded below by 0");
- loopBodyBuilder.Add(cmd);
- }
- }
- // check: decreases < old(decreases)
- Bpl.Expr decrCheck = null;
- for (int i = s.Decreases.Count; 0 <= --i; )
- invariant i != s.Decreases.Count ==> decrCheck != null;
- {
- Bpl.Expr less = Less[i];
- Bpl.Expr eq = Eq[i];
- if (decrCheck == null) {
- decrCheck = less;
- } else {
- // decrCheck = less || (eq && decrCheck)
- decrCheck = Bpl.Expr.Or(less, Bpl.Expr.And(eq, decrCheck));
- }
+ types.Add((!)e.Type);
+ decrsTotal.Add(IsTotal(e, etran));
+ decrs.Add(etran.TrExpr(e));
}
- assert decrCheck != null; // follows from loop invariant and the fact that s.Decreases.Count != 0
+ Bpl.Expr decrCheck = DecreasesCheck(stmt.Tok, 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);
@@ -1826,7 +1889,7 @@ namespace Microsoft.Dafny { foreach (Expression se in SplitExpr(ps.Expr, true)) {
Bpl.Expr e = etran.TrExpr(se);
Bpl.Expr q = new Bpl.ForallExpr(se.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
- builder.Add(new Bpl.AssertCmd(se.tok, q));
+ builder.Add(Assert(se.tok, q, "assertion violation"));
pieces++;
}
}
@@ -1881,6 +1944,121 @@ namespace Microsoft.Dafny { }
}
+ /// <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.StmtListBuilder! builder, ExpressionTranslator! etran, string! suffixMsg)
+ requires predef != null;
+ requires types.Count == ee0.Count && ee0.Count == ee1.Count;
+ {
+ int N = types.Count;
+
+ // compute eq and less for each component of the lexicographic pair
+ List<Bpl.Expr!> Eq = new List<Bpl.Expr!>(N);
+ 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);
+ Eq.Add(eq);
+ Less.Add(less);
+ }
+ // check: total(ee0)
+ // 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] || total0[k]
+ // Also:
+ // check: 0 <= ee1
+ // 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
+ 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);
+ builder.Add(cmd);
+
+ if (types[k] is IntType) {
+ Bpl.Expr bounded = Bpl.Expr.Le(Bpl.Expr.Literal(0), ee1[k]);
+ 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);
+ builder.Add(cmd);
+ }
+ }
+ // check: ee0 < ee1
+ Bpl.Expr decrCheck = null;
+ for (int i = N; 0 <= --i; )
+ invariant i != N ==> decrCheck != null;
+ {
+ Bpl.Expr less = Less[i];
+ Bpl.Expr eq = Eq[i];
+ if (decrCheck == null) {
+ decrCheck = less;
+ } else {
+ // decrCheck = less || (eq && decrCheck)
+ decrCheck = Bpl.Expr.Or(less, Bpl.Expr.And(eq, decrCheck));
+ }
+ }
+ if (decrCheck == null) {
+ return Bpl.Expr.False;
+ } else {
+ return decrCheck;
+ }
+ }
+
+ bool CompatibleDecreasesTypes(Type! t, Type! u) {
+ if (t is BoolType) {
+ return u is BoolType;
+ } else if (t is IntType) {
+ return u is IntType;
+ } else if (t is SetType) {
+ return u is SetType;
+ } else if (t is SeqType) {
+ return u is SeqType;
+ } else if (t.IsDatatype) {
+ return u.IsDatatype;
+ } else {
+ assert t.IsRefType;
+ return u.IsRefType;
+ }
+ }
+
+ void ComputeLessEq(Token! tok, Type! ty, Bpl.Expr! e0, Bpl.Expr! e1, out Bpl.Expr! less, out Bpl.Expr! eq, ExpressionTranslator! etran)
+ requires predef != null;
+ {
+ if (ty is BoolType) {
+ eq = Bpl.Expr.Iff(e0, e1);
+ less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
+ } else if (ty is IntType) {
+ eq = Bpl.Expr.Eq(e0, e1);
+ less = Bpl.Expr.Lt(e0, e1);
+ } else if (ty is SetType) {
+ eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, e0, e1);
+ less = etran.ProperSubset(tok, e0, e1);
+ } else if (ty is SeqType) {
+ Bpl.Expr b0 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
+ Bpl.Expr b1 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
+ eq = Bpl.Expr.Eq(b0, b1);
+ less = Bpl.Expr.Lt(b0, b1);
+ } else if (ty.IsDatatype) {
+ Bpl.Expr b0 = FunctionCall(tok, BuiltinFunction.DtRank, null, e0);
+ Bpl.Expr b1 = FunctionCall(tok, BuiltinFunction.DtRank, null, e1);
+ eq = Bpl.Expr.Eq(b0, b1);
+ less = Bpl.Expr.Lt(b0, b1);
+
+ } else {
+ // reference type
+ Bpl.Expr b0 = Bpl.Expr.Neq(e0, predef.Null);
+ Bpl.Expr b1 = Bpl.Expr.Neq(e1, predef.Null);
+ eq = Bpl.Expr.Iff(b0, b1);
+ less = Bpl.Expr.And(Bpl.Expr.Not(b0), b1);
+ }
+ }
+
void AddComment(Bpl.StmtListBuilder! builder, Statement! stmt, string! comment) {
builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));
}
@@ -2827,13 +3005,13 @@ namespace Microsoft.Dafny { yield return expr;
}
- static Expression! Substitute(Expression! expr, Expression! receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
+ static Expression! Substitute(Expression! expr, Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
Expression newExpr = null; // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end
- if (expr is LiteralExpr) {
+ if (expr is LiteralExpr || expr is WildcardExpr) {
// nothing to substitute
} else if (expr is ThisExpr) {
- return receiverReplacement;
+ return receiverReplacement == null ? expr : receiverReplacement;
} else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
Expression substExpr;
@@ -2958,7 +3136,7 @@ namespace Microsoft.Dafny { }
static List<Expression!>! SubstituteExprList(List<Expression!>! elist,
- Expression! receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
+ Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
List<Expression!> newElist = null; // initialized lazily
for (int i = 0; i < elist.Count; i++)
invariant newElist == null || newElist.Count == i;
@@ -2981,7 +3159,7 @@ namespace Microsoft.Dafny { }
}
- static Triggers SubstTriggers(Triggers trigs, Expression! receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
+ static Triggers SubstTriggers(Triggers trigs, Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
if (trigs != null) {
List<Expression!> terms = SubstituteExprList(trigs.Terms, receiverReplacement, substMap);
Triggers prev = SubstTriggers(trigs.Prev, receiverReplacement, substMap);
@@ -2992,7 +3170,7 @@ namespace Microsoft.Dafny { return trigs;
}
- static Attributes SubstAttributes(Attributes attrs, Expression! receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
+ static Attributes SubstAttributes(Attributes attrs, Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {
if (attrs != null) {
List<Attributes.Argument!> newArgs = new List<Attributes.Argument!>(); // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes
bool anyArgSubst = false;
diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index a9fd2367..954ca3b0 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -9,7 +9,7 @@ Dafny program verifier finished with 3 verified, 0 errors -------------------- b3.dfy --------------------
-Dafny program verifier finished with 4 verified, 0 errors
+Dafny program verifier finished with 5 verified, 0 errors
-------------------- b4.dfy --------------------
@@ -29,4 +29,4 @@ Dafny program verifier finished with 11 verified, 0 errors -------------------- b8.dfy --------------------
-Dafny program verifier finished with 21 verified, 0 errors
+Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index 8026e60f..34ff5f57 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -17,8 +17,8 @@ class Queue<T> { tail.next == null &&
(forall n ::
n in spine ==>
- n != null && n.Valid() &&
- n.footprint <= footprint &&
+ n != null && n.footprint <= footprint && this !in n.footprint &&
+ n.Valid() &&
(n.next == null ==> n == tail)) &&
(forall n ::
n in spine ==>
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index bc26ee85..a0cb6e74 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -59,7 +59,7 @@ class Glossary { invariant (forall d :: d in glossary.values ==> null !in d);
invariant q !in rs.footprint;
invariant q.contents == glossary.keys;
- // we leave out the decreases clause - unbounded stream
+ decreases *; // we leave out the decreases clause - unbounded stream
{
call term,definition := readDefinition(rs);
if (term == null) {
@@ -135,7 +135,7 @@ class Glossary { while (true)
invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));
invariant null !in definition;
- // we leave out the decreases clause - unbounded stream
+ decreases *; // we leave out the decreases clause - unbounded stream
{
call w := rs.GetWord();
if (w == null)
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 62457ec4..043a4cfd 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -56,8 +56,18 @@ Dafny program verifier finished with 0 verified, 0 errors Boogie program verifier finished with 8 verified, 0 errors
+-------------------- TypeTests.dfy --------------------
+TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
+TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
+TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
+TypeTests.dfy(11,4): Error: incorrect type of method in-parameter 0 (expected int, got bool)
+TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected int, got C)
+TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)
+7 resolution/type errors detected in synthetic program
+
-------------------- SmallTests.dfy --------------------
-SmallTests.dfy(29,7): Error: RHS expression must be well defined
+SmallTests.dfy(30,7): Error: RHS expression must be well defined
Execution trace:
(0,0): anon0
@@ -85,47 +95,47 @@ Dafny program verifier finished with 5 verified, 0 errors -------------------- SchorrWaite.dfy --------------------
-Dafny program verifier finished with 4 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
-------------------- Termination.dfy --------------------
Dafny program verifier finished with 6 verified, 0 errors
-------------------- Use.dfy --------------------
-Use.dfy(12,5): Error BP5001: This assertion might not hold.
+Use.dfy(12,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(25,5): Error BP5001: This assertion might not hold.
+Use.dfy(25,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(50,5): Error BP5001: This assertion might not hold.
+Use.dfy(50,5): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 6 verified, 3 errors
-------------------- DTypes.dfy --------------------
-DTypes.dfy(15,5): Error BP5001: This assertion might not hold.
+DTypes.dfy(15,5): Error: assertion violation
Execution trace:
(0,0): anon0
-DTypes.dfy(28,5): Error BP5001: This assertion might not hold.
+DTypes.dfy(28,5): Error: assertion violation
Execution trace:
(0,0): anon0
-DTypes.dfy(54,5): Error BP5001: This assertion might not hold.
+DTypes.dfy(54,5): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 5 verified, 3 errors
-------------------- TypeParameters.dfy --------------------
-TypeParameters.dfy(41,5): Error BP5001: This assertion might not hold.
+TypeParameters.dfy(41,5): Error: assertion violation
Execution trace:
(0,0): anon0
-TypeParameters.dfy(63,5): Error BP5001: This assertion might not hold.
+TypeParameters.dfy(63,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 9 verified, 2 errors
+Dafny program verifier finished with 10 verified, 2 errors
-------------------- Datatypes.dfy --------------------
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy index 138a22df..54a98a56 100644 --- a/Test/dafny0/BinaryTree.dfy +++ b/Test/dafny0/BinaryTree.dfy @@ -10,9 +10,9 @@ class IntSet { this in footprint &&
(root == null ==> contents == {}) &&
(root != null ==>
- root in footprint && root.Valid() &&
- contents == root.contents &&
- root.footprint <= footprint && this !in root.footprint)
+ root in footprint && root.footprint <= footprint && this !in root.footprint &&
+ root.Valid() &&
+ contents == root.contents)
}
method Init()
@@ -110,12 +110,14 @@ class Node { this in footprint &&
null !in footprint &&
(left != null ==>
- left in footprint && left.Valid() &&
+ left in footprint &&
left.footprint <= footprint && this !in left.footprint &&
+ left.Valid() &&
(forall y :: y in left.contents ==> y < data)) &&
(right != null ==>
- right in footprint && right.Valid() &&
+ right in footprint &&
right.footprint <= footprint && this !in right.footprint &&
+ right.Valid() &&
(forall y :: y in right.contents ==> data < y)) &&
(left == null && right == null ==>
contents == {data}) &&
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index c468cff4..c6f0737c 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -58,7 +58,9 @@ class C { {
var a := new CP<int,C>;
var b := new CP<int,object>;
- while (a != null) {
+ while (a != null)
+ decreases *; // omit loop termination check (in fact, the loop does not terminate)
+ {
var x: object := a;
var y: object := b;
assert x == y ==> x == null;
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 61ae9cb6..8492f217 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -8,7 +8,8 @@ class Node { var next: Node;
function Repr(list: List<int>): bool
- reads this;
+ reads *;
+ decreases list;
{ match list
case Nil =>
next == null
@@ -38,7 +39,8 @@ class AnotherNode { var next: AnotherNode;
function Repr(n: AnotherNode, list: List<int>): bool
- reads n;
+ reads *;
+ decreases list;
{ match list
case Nil =>
n == null
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy index 759c6afd..952c47d2 100644 --- a/Test/dafny0/ListContents.dfy +++ b/Test/dafny0/ListContents.dfy @@ -75,6 +75,7 @@ class Node<T> { (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
invariant
(forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
+ decreases current, |current.list|;
{
var nx := current.next;
assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma
diff --git a/Test/dafny0/ListCopy.dfy b/Test/dafny0/ListCopy.dfy index f3c64fe2..52f5cf76 100644 --- a/Test/dafny0/ListCopy.dfy +++ b/Test/dafny0/ListCopy.dfy @@ -31,6 +31,7 @@ class Node { invariant prev in newRegion;
invariant fresh(newRegion);
invariant newRegion !! existingRegion;
+ decreases *; // omit loop termination check
{
var tmp := new Node;
call tmp.Init();
diff --git a/Test/dafny0/ListReverse.dfy b/Test/dafny0/ListReverse.dfy index 08b14751..ef029b88 100644 --- a/Test/dafny0/ListReverse.dfy +++ b/Test/dafny0/ListReverse.dfy @@ -16,6 +16,7 @@ class Node { invariant current == null || current in r;
invariant reverse == null || reverse in r;
invariant (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure
+ decreases *; // omit loop termination check
{
var tmp := current.nxt;
current.nxt := reverse;
diff --git a/Test/dafny0/Queue.dfy b/Test/dafny0/Queue.dfy index 5c22ec92..da1ab2c5 100644 --- a/Test/dafny0/Queue.dfy +++ b/Test/dafny0/Queue.dfy @@ -17,12 +17,12 @@ class Queue<T> { head != null && head in spine &&
tail != null && tail in spine &&
tail.next == null &&
- (forall n :: // { n in spine }
+ (forall n ::
n in spine ==>
- n != null && n.Valid() &&
- n.footprint <= footprint &&
+ n != null && n.footprint <= footprint && this !in n.footprint &&
+ n.Valid() &&
(n.next == null ==> n == tail)) &&
- (forall n :: // { n.next }
+ (forall n ::
n in spine ==>
n.next != null ==> n.next in spine) &&
contents == head.tailContents
diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy index 20db882a..527d379f 100644 --- a/Test/dafny0/SchorrWaite.dfy +++ b/Test/dafny0/SchorrWaite.dfy @@ -7,6 +7,7 @@ class Node { var marked: bool;
var childrenVisited: int;
var children: seq<Node>;
+ var pathFromRoot: Path; // used only as ghost variable
}
class Main {
@@ -61,11 +62,13 @@ class Main { invariant (forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
n.children == old(n.children));
+ decreases |root.children| - i;
{
var c := root.children[i];
if (c != null) {
call RecursiveMarkWorker(c, S, stackNodes + {root});
}
+ i := i + 1;
}
}
}
@@ -140,24 +143,48 @@ class Main { // ---------------------------------------------------------------------------------
+ function Reachable(from: Node, to: Node, S: set<Node>): bool
+ requires null !in S;
+ reads S;
+ decreases 1;
+ {
+ (exists via: Path :: ReachableVia(from, via, to, S))
+ }
+
+ function ReachableVia(from: Node, via: Path, to: Node, S: set<Node>): bool
+ requires null !in S;
+ reads S;
+ decreases 0, via;
+ {
+ match via
+ case Empty => from == to
+ case Extend(prefix, n) => n in S && to in n.children && ReachableVia(from, prefix, n, S)
+ }
+
method SchorrWaite(root: Node, S: set<Node>)
requires root in S;
// 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
requires (forall n :: n in S ==> ! n.marked && n.childrenVisited == 0);
modifies S;
- ensures root.marked;
// 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
+ ensures (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));
+ // 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;
t.marked := true;
+ t.pathFromRoot := path;
var stackNodes := []; // used as ghost variable
var unmarkedNodes := S - {t}; // used as ghost variable
while (true)
@@ -183,6 +210,11 @@ 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
+ 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)));
+ invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));
// the current values of m.children[m.childrenVisited] for m's on the stack:
invariant 0 < |stackNodes| ==> stackNodes[0].children[stackNodes[0].childrenVisited] == null;
invariant (forall k :: 0 < k && k < |stackNodes| ==>
@@ -208,10 +240,12 @@ class Main { p := oldP;
stackNodes := stackNodes[..|stackNodes| - 1];
t.childrenVisited := t.childrenVisited + 1;
+ path := t.pathFromRoot;
} else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) {
// just advance to next child
t.childrenVisited := t.childrenVisited + 1;
+
} else {
// push
@@ -220,10 +254,17 @@ class Main { t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..];
p := t;
stackNodes := stackNodes + [t];
+ path := #Path.Extend(path, t);
t := newT;
t.marked := true;
+ t.pathFromRoot := path;
unmarkedNodes := unmarkedNodes - {t};
}
}
}
}
+
+datatype Path {
+ Empty;
+ Extend(Path, Node);
+}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 01c9f1ea..17f0168a 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -2,9 +2,10 @@ class Node { var next: Node;
function IsList(r: set<Node>): bool
- reads this, r;
+ reads r;
{
- next != null ==> next.IsList(r - {this})
+ this in r &&
+ (next != null ==> next.IsList(r - {this}))
}
method Test(n: Node, nodes: set<Node>)
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy new file mode 100644 index 00000000..4cb02858 --- /dev/null +++ b/Test/dafny0/TypeTests.dfy @@ -0,0 +1,18 @@ +class C {
+ function F(c: C, d: D): bool { true }
+ method M(x: int) returns (y: int, c: C)
+ requires F(#D.A, this); // 2 errors
+ requires F(4, 5); // 2 errors
+ requires F(this, #D.A); // good
+ { }
+
+ method Caller()
+ {
+ call m,n := M(true); // error on in-parameter
+ call n,m := M(m); // 2 errors on out-parameters
+ }
+}
+
+datatype D {
+ A;
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 4fa6832e..f1bcfde0 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,7 +17,7 @@ for %%f in (BQueue.bpl) do ( %BPLEXE% %* %%f
)
-for %%f in (SmallTests.dfy Queue.dfy ListCopy.dfy
+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) do (
|