summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Dafny/Compiler.cs15
-rw-r--r--Dafny/Dafny.atg10
-rw-r--r--Dafny/DafnyAst.cs32
-rw-r--r--Dafny/Parser.cs154
-rw-r--r--Dafny/Printer.cs5
-rw-r--r--Dafny/RefinementTransformer.cs4
-rw-r--r--Dafny/Resolver.cs16
-rw-r--r--Dafny/Scanner.cs26
-rw-r--r--Dafny/Translator.cs36
-rw-r--r--Test/dafny0/Answer10
-rw-r--r--Test/dafny0/ParallelResolveErrors.dfy2
-rw-r--r--Test/dafny0/SmallTests.dfy24
-rw-r--r--Test/dafny0/TypeTests.dfy25
-rw-r--r--Test/dafny2/Answer2
-rw-r--r--Test/dafny2/MajorityVote.dfy122
15 files changed, 360 insertions, 123 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 58c73561..911e5aac 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -838,7 +838,10 @@ namespace Microsoft.Dafny {
if (stmt is AssumeStmt) {
Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line);
} else if (stmt is AssignSuchThatStmt) {
- Error("an assign-such-that statement cannot be compiled (line {0})", stmt.Tok.line);
+ var s = (AssignSuchThatStmt)stmt;
+ if (s.AssumeToken != null) {
+ Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);
+ }
} else {
foreach (var ss in stmt.SubStatements) {
CheckHasNoAssumes(ss);
@@ -914,6 +917,16 @@ namespace Microsoft.Dafny {
Contract.Assert(!(s.Lhs is SeqSelectExpr) || ((SeqSelectExpr)s.Lhs).SelectOne); // multi-element array assignments are not allowed
TrRhs(null, s.Lhs, s.Rhs, indent);
+ } else if (stmt is AssignSuchThatStmt) {
+ var s = (AssignSuchThatStmt)stmt;
+ foreach (var lhs in s.Lhss) {
+ // assigning to a local ghost variable or to a ghost field is okay
+ if (!AssignStmt.LhsIsToGhost(lhs)) {
+ Error("compiling an assign-such-that statement with a non-ghost left-hand side is currently not supported (line {0})", stmt.Tok.line);
+ break; // no need to say more
+ }
+ }
+
} else if (stmt is VarDecl) {
TrVarDecl((VarDecl)stmt, true, indent);
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 195495aa..a1ff0ffb 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -725,6 +725,7 @@ UpdateStmt<out Statement/*!*/ s>
Expression lhs0;
IToken x;
Attributes attrs = null;
+ IToken suchThatAssume = null;
Expression suchThat = null;
.)
Lhs<out e> (. x = e.tok; .)
@@ -738,13 +739,15 @@ UpdateStmt<out Statement/*!*/ s>
{ "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
| ":|" (. x = t; .)
+ [ "assume" (. suchThatAssume = t; .)
+ ]
Expression<out suchThat>
)
";"
| ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
)
(. if (suchThat != null) {
- s = new AssignSuchThatStmt(x, lhss, suchThat);
+ s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
s = new UpdateStmt(x, lhss, rhss);
}
@@ -807,6 +810,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
AssignmentRhs r; IdentifierExpr lhs0;
List<VarDecl> lhss = new List<VarDecl>();
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+ IToken suchThatAssume = null;
Expression suchThat = null;
.)
[ "ghost" (. isGhost = true; x = t; .)
@@ -824,6 +828,8 @@ VarDeclStatement<.out Statement/*!*/ s.>
{ "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
| ":|" (. assignTok = t; .)
+ [ "assume" (. suchThatAssume = t; .)
+ ]
Expression<out suchThat>
]
";"
@@ -833,7 +839,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
foreach (var lhs in lhss) {
ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));
}
- update = new AssignSuchThatStmt(assignTok, ies, suchThat);
+ update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);
} else if (rhss.Count == 0) {
update = null;
} else {
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 95110629..f8b78692 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1703,14 +1703,22 @@ namespace Microsoft.Dafny {
public class AssignSuchThatStmt : ConcreteUpdateStatement
{
- public readonly AssumeStmt Assume;
- public AssignSuchThatStmt(IToken tok, List<Expression> lhss, Expression expr)
+ public readonly Expression Expr;
+ public readonly IToken AssumeToken;
+ /// <summary>
+ /// "assumeToken" is allowed to be "null", in which case the verifier will check that a RHS value exists.
+ /// If "assumeToken" is non-null, then it should denote the "assume" keyword used in the statement.
+ /// </summary>
+ public AssignSuchThatStmt(IToken tok, List<Expression> lhss, Expression expr, IToken assumeToken)
: base(tok, lhss) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(lhss));
Contract.Requires(lhss.Count != 0);
Contract.Requires(expr != null);
- Assume = new AssumeStmt(tok, expr);
+ Expr = expr;
+ if (assumeToken != null) {
+ AssumeToken = assumeToken;
+ }
}
}
@@ -1771,6 +1779,24 @@ namespace Microsoft.Dafny {
}
}
}
+
+ /// <summary>
+ /// This method assumes "lhs" has been successfully resolved.
+ /// </summary>
+ public static bool LhsIsToGhost(Expression lhs) {
+ Contract.Requires(lhs != null);
+ lhs = lhs.Resolved;
+ if (lhs is IdentifierExpr) {
+ var x = (IdentifierExpr)lhs;
+ return x.Var.IsGhost;
+ } else if (lhs is FieldSelectExpr) {
+ var x = (FieldSelectExpr)lhs;
+ return x.Field.IsGhost;
+ } else {
+ // LHS denotes an array element, which is always non-ghost
+ return false;
+ }
+ }
}
public class VarDecl : Statement, IVariable {
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 52bbc90c..068aa2f6 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1056,11 +1056,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s = bs;
break;
}
- case 65: {
+ case 66: {
AssertStmt(out s);
break;
}
- case 66: {
+ case 54: {
AssumeStmt(out s);
break;
}
@@ -1076,15 +1076,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
VarDeclStatement(out s);
break;
}
- case 58: {
+ case 59: {
IfStmt(out s);
break;
}
- case 62: {
+ case 63: {
WhileStmt(out s);
break;
}
- case 64: {
+ case 65: {
MatchStmt(out s);
break;
}
@@ -1136,7 +1136,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression/*!*/ e = null; Attributes attrs = null;
- Expect(65);
+ Expect(66);
x = t; s = null;
while (IsAttribute()) {
Attribute(ref attrs);
@@ -1157,7 +1157,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(66);
+ Expect(54);
x = t;
Expression(out e);
Expect(18);
@@ -1188,6 +1188,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression lhs0;
IToken x;
Attributes attrs = null;
+ IToken suchThatAssume = null;
Expression suchThat = null;
Lhs(out e);
@@ -1218,6 +1219,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 53) {
Get();
x = t;
+ if (la.kind == 54) {
+ Get();
+ suchThatAssume = t;
+ }
Expression(out suchThat);
} else SynErr(145);
Expect(18);
@@ -1226,7 +1231,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
} else SynErr(146);
if (suchThat != null) {
- s = new AssignSuchThatStmt(x, lhss, suchThat);
+ s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1239,6 +1244,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
AssignmentRhs r; IdentifierExpr lhs0;
List<VarDecl> lhss = new List<VarDecl>();
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+ IToken suchThatAssume = null;
Expression suchThat = null;
if (la.kind == 8) {
@@ -1271,6 +1277,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else {
Get();
assignTok = t;
+ if (la.kind == 54) {
+ Get();
+ suchThatAssume = t;
+ }
Expression(out suchThat);
}
}
@@ -1281,7 +1291,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
foreach (var lhs in lhss) {
ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));
}
- update = new AssignSuchThatStmt(assignTok, ies, suchThat);
+ update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);
} else if (rhss.Count == 0) {
update = null;
} else {
@@ -1306,7 +1316,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(58);
+ Expect(59);
x = t;
if (la.kind == 27 || la.kind == 33) {
if (la.kind == 33) {
@@ -1316,9 +1326,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
guardOmitted = true;
}
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 59) {
+ if (la.kind == 60) {
Get();
- if (la.kind == 58) {
+ if (la.kind == 59) {
IfStmt(out s);
els = s;
} else if (la.kind == 6) {
@@ -1351,7 +1361,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(62);
+ Expect(63);
x = t;
if (la.kind == 27 || la.kind == 33) {
if (la.kind == 33) {
@@ -1395,11 +1405,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(64);
+ Expect(65);
x = t;
Expression(out e);
Expect(6);
- while (la.kind == 60) {
+ while (la.kind == 61) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1476,16 +1486,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
r = null; // to please compiler
Attributes attrs = null;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 33 || la.kind == 43 || la.kind == 55) {
- if (la.kind == 55) {
+ if (la.kind == 33 || la.kind == 43 || la.kind == 56) {
+ if (la.kind == 56) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(56);
+ Expect(57);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else if (la.kind == 43) {
@@ -1527,7 +1537,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 57) {
+ } else if (la.kind == 58) {
Get();
x = t;
Expression(out e);
@@ -1550,13 +1560,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 43 || la.kind == 55) {
+ while (la.kind == 43 || la.kind == 56) {
Suffix(ref e);
}
} else if (StartOf(15)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 43 || la.kind == 55) {
+ while (la.kind == 43 || la.kind == 56) {
Suffix(ref e);
}
} else SynErr(152);
@@ -1593,11 +1603,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Statement> body;
Expect(6);
- while (la.kind == 60) {
+ while (la.kind == 61) {
Get();
x = t;
Expression(out e);
- Expect(61);
+ Expect(62);
body = new List<Statement>();
while (StartOf(10)) {
Stmt(body);
@@ -1615,7 +1625,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod = null;
while (StartOf(16)) {
- if (la.kind == 29 || la.kind == 63) {
+ if (la.kind == 29 || la.kind == 64) {
Invariant(out invariant);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}
Expect(18);
@@ -1653,12 +1663,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 29 || la.kind == 63)) {SynErr(159); Get();}
+ while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(159); Get();}
if (la.kind == 29) {
Get();
isFree = true;
}
- Expect(63);
+ Expect(64);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -1673,7 +1683,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(60);
+ Expect(61);
x = t;
Ident(out id);
if (la.kind == 33) {
@@ -1687,7 +1697,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(34);
}
- Expect(61);
+ Expect(62);
while (StartOf(10)) {
Stmt(body);
}
@@ -2032,18 +2042,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 19: case 38: case 58: case 64: case 65: case 66: case 101: case 102: case 103: case 104: {
+ case 19: case 38: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 43 || la.kind == 55) {
+ while (la.kind == 43 || la.kind == 56) {
Suffix(ref e);
}
break;
}
- case 6: case 55: {
+ case 6: case 56: {
DisplayExpr(out e);
break;
}
@@ -2057,7 +2067,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
ConstAtomExpression(out e);
- while (la.kind == 43 || la.kind == 55) {
+ while (la.kind == 43 || la.kind == 56) {
Suffix(ref e);
}
break;
@@ -2096,18 +2106,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<BoundVar> letVars; List<Expression> letRHSs;
switch (la.kind) {
- case 58: {
+ case 59: {
Get();
x = t;
Expression(out e);
Expect(99);
Expression(out e0);
- Expect(59);
+ Expect(60);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 64: {
+ case 65: {
MatchExpression(out e);
break;
}
@@ -2119,7 +2129,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ComprehensionExpr(out e);
break;
}
- case 65: {
+ case 66: {
Get();
x = t;
Expression(out e0);
@@ -2128,7 +2138,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new AssertExpr(x, e0, e1);
break;
}
- case 66: {
+ case 54: {
Get();
x = t;
Expression(out e0);
@@ -2208,7 +2218,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 55) {
+ } else if (la.kind == 56) {
Get();
x = t;
if (StartOf(9)) {
@@ -2225,7 +2235,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 20 || la.kind == 56) {
+ } else if (la.kind == 20 || la.kind == 57) {
while (la.kind == 20) {
Get();
Expression(out ee);
@@ -2267,7 +2277,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- Expect(56);
+ Expect(57);
} else SynErr(173);
}
@@ -2284,14 +2294,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e = new SetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 55) {
+ } else if (la.kind == 56) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(9)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(56);
+ Expect(57);
} else SynErr(174);
}
@@ -2329,14 +2339,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(41);
x = t;
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
elements = new List<ExpressionPair/*!*/>();
if (StartOf(9)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(x, elements);
- Expect(56);
+ Expect(57);
} else if (la.kind == 1) {
BoundVar/*!*/ bv;
List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
@@ -2472,10 +2482,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(64);
+ Expect(65);
x = t;
Expression(out e);
- while (la.kind == 60) {
+ while (la.kind == 61) {
CaseExpression(out c);
cases.Add(c);
}
@@ -2542,7 +2552,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(60);
+ Expect(61);
x = t;
Ident(out id);
if (la.kind == 33) {
@@ -2556,7 +2566,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(34);
}
- Expect(61);
+ Expect(62);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
@@ -2610,7 +2620,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,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, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,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, 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, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,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,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,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,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,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},
@@ -2619,18 +2629,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
{x,x,x,x, 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,T, 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,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,x,x,x, 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,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,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, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,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, T,T,T,T, T,T,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, T,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,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,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, x,T,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, 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, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, 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, T,T,T,T, T,T,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, T,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, 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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, 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,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, 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,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,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, 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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T,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,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, 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,x,x,x, T,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
- {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, 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,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
};
} // end Parser
@@ -2709,19 +2719,19 @@ public class Errors {
case 51: s = "\"return\" expected"; break;
case 52: s = "\":=\" expected"; break;
case 53: s = "\":|\" expected"; break;
- case 54: s = "\"new\" expected"; break;
- case 55: s = "\"[\" expected"; break;
- case 56: s = "\"]\" expected"; break;
- case 57: s = "\"choose\" expected"; break;
- case 58: s = "\"if\" expected"; break;
- case 59: s = "\"else\" expected"; break;
- case 60: s = "\"case\" expected"; break;
- case 61: s = "\"=>\" expected"; break;
- case 62: s = "\"while\" expected"; break;
- case 63: s = "\"invariant\" expected"; break;
- case 64: s = "\"match\" expected"; break;
- case 65: s = "\"assert\" expected"; break;
- case 66: s = "\"assume\" expected"; break;
+ case 54: s = "\"assume\" expected"; break;
+ case 55: s = "\"new\" expected"; break;
+ case 56: s = "\"[\" expected"; break;
+ case 57: s = "\"]\" expected"; break;
+ case 58: s = "\"choose\" expected"; break;
+ case 59: s = "\"if\" expected"; break;
+ case 60: s = "\"else\" expected"; break;
+ case 61: s = "\"case\" expected"; break;
+ case 62: s = "\"=>\" expected"; break;
+ case 63: s = "\"while\" expected"; break;
+ case 64: s = "\"invariant\" expected"; break;
+ case 65: s = "\"match\" expected"; break;
+ case 66: s = "\"assert\" expected"; break;
case 67: s = "\"print\" expected"; break;
case 68: s = "\"parallel\" expected"; break;
case 69: s = "\"<==>\" expected"; break;
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index e58a39de..fb46ba4b 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -661,7 +661,10 @@ namespace Microsoft.Dafny {
} else if (s is AssignSuchThatStmt) {
var update = (AssignSuchThatStmt)s;
wr.Write(" :| ");
- PrintExpression(update.Assume.Expr);
+ if (update.AssumeToken != null) {
+ wr.Write("assume ");
+ }
+ PrintExpression(update.Expr);
} else {
Contract.Assert(s == null); // otherwise, unknown type
}
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index ba3cae19..51b22443 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -493,7 +493,7 @@ namespace Microsoft.Dafny {
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
- r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Assume.Expr));
+ r = new AssignSuchThatStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), CloneExpr(s.Expr), s.AssumeToken == null ? null : Tok(s.AssumeToken));
} else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
@@ -914,7 +914,7 @@ namespace Microsoft.Dafny {
doMerge = true;
} else if (cOld.Update is AssignSuchThatStmt) {
doMerge = true;
- addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Assume.Expr);
+ addedAssert = CloneExpr(((AssignSuchThatStmt)cOld.Update).Expr);
} else {
var updateOld = (UpdateStmt)cOld.Update; // if cast fails, there are more ConcreteUpdateStatement subclasses than expected
if (updateOld.Rhss.Count == 1 && updateOld.Rhss[0] is HavocRhs) {
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index e013367b..3780e0d9 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1845,7 +1845,9 @@ namespace Microsoft.Dafny {
int prevErrorCount = ErrorCount;
// First, resolve all LHS's and expression-looking RHS's.
SeqSelectExpr arrayRangeLhs = null;
+ var update = s as UpdateStmt;
foreach (var lhs in s.Lhss) {
+ var ec = ErrorCount;
if (lhs is SeqSelectExpr) {
var sse = (SeqSelectExpr)lhs;
ResolveSeqSelectExpr(sse, true, true);
@@ -1855,14 +1857,24 @@ namespace Microsoft.Dafny {
} else {
ResolveExpression(lhs, true);
}
+ if (update == null && ec == ErrorCount && specContextOnly && !AssignStmt.LhsIsToGhost(lhs)) {
+ Error(lhs, "cannot assign to non-ghost variable in a ghost context");
+ }
}
IToken firstEffectfulRhs = null;
CallRhs callRhs = null;
- var update = s as UpdateStmt;
// Resolve RHSs
if (update == null) {
var suchThat = (AssignSuchThatStmt)s; // this is the other possible subclass
- s.ResolvedStatements.Add(suchThat.Assume);
+ ResolveExpression(suchThat.Expr, true);
+ if (suchThat.AssumeToken == null) {
+ // to ease in the verification, only allow local variables as LHSs
+ foreach (var lhs in s.Lhss) {
+ if (!(lhs.Resolved is IdentifierExpr)) {
+ Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");
+ }
+ }
+ }
} else {
foreach (var rhs in update.Rhss) {
bool isEffectful;
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 2388716b..d35fc22f 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -520,16 +520,16 @@ public class Scanner {
case "label": t.kind = 49; break;
case "break": t.kind = 50; break;
case "return": t.kind = 51; break;
- case "new": t.kind = 54; break;
- case "choose": t.kind = 57; break;
- case "if": t.kind = 58; break;
- case "else": t.kind = 59; break;
- case "case": t.kind = 60; break;
- case "while": t.kind = 62; break;
- case "invariant": t.kind = 63; break;
- case "match": t.kind = 64; break;
- case "assert": t.kind = 65; break;
- case "assume": t.kind = 66; break;
+ case "assume": t.kind = 54; break;
+ case "new": t.kind = 55; break;
+ case "choose": t.kind = 58; break;
+ case "if": t.kind = 59; break;
+ case "else": t.kind = 60; break;
+ case "case": t.kind = 61; break;
+ case "while": t.kind = 63; break;
+ case "invariant": t.kind = 64; break;
+ case "match": t.kind = 65; break;
+ case "assert": t.kind = 66; break;
case "print": t.kind = 67; break;
case "parallel": t.kind = 68; break;
case "in": t.kind = 82; break;
@@ -666,11 +666,11 @@ public class Scanner {
case 27:
{t.kind = 53; break;}
case 28:
- {t.kind = 55; break;}
- case 29:
{t.kind = 56; break;}
+ case 29:
+ {t.kind = 57; break;}
case 30:
- {t.kind = 61; break;}
+ {t.kind = 62; break;}
case 31:
if (ch == '>') {AddCh(); goto case 32;}
else {goto case 0;}
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 2325734f..a98b49fd 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3414,7 +3414,11 @@ namespace Microsoft.Dafny {
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
AddComment(builder, s, "assign-such-that statement");
- // treat like a parallel havoc, followed by an assume
+ // Essentially, treat like an assert, a parallel havoc, and an assume. However, we also need to check
+ // the well-formedness of the expression, which is easiest to do after the havoc. So, we do the havoc
+ // first, then the well-formedness check, then the assert (unless the whole statement is an assume), and
+ // finally the assume.
+
// Here comes the havoc part
var lhss = new List<Expression>();
var havocRhss = new List<AssignmentRhs>();
@@ -3426,8 +3430,36 @@ namespace Microsoft.Dafny {
List<Bpl.IdentifierExpr> bLhss;
ProcessLhss(lhss, false, builder, locals, etran, out lhsBuilder, out bLhss);
ProcessRhss(lhsBuilder, bLhss, lhss, havocRhss, builder, locals, etran);
+ // Here comes the well-formedness check
+ TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
+ // Here comes the assert part
+ if (s.AssumeToken == null) {
+ var substMap = new Dictionary<IVariable, Expression>();
+ var bvars = new List<BoundVar>();
+ foreach (var lhs in s.Lhss) {
+ var l = lhs.Resolved;
+ if (l is IdentifierExpr) {
+ var x = (IdentifierExpr)l;
+ BoundVar bv;
+ IdentifierExpr ie;
+ CloneVariableAsBoundVar(x.tok, x.Var, "$as#" + x.Name, out bv, out ie);
+ bvars.Add(bv);
+ substMap.Add(x.Var, ie);
+ } else {
+ // other forms of LHSs have been ruled out by the resolver (it would be possible to
+ // handle them, but it would involve heap-update expressions--the translation would take
+ // effort, and it's not certain that the existential would be successful in verification).
+ Contract.Assume(false); // unexpected case
+ }
+ }
+ var bvs = new VariableSeq();
+ var typeAntecedent = etran.TrBoundVariables(bvars, bvs);
+ var substE = etran.TrExpr(Substitute(s.Expr, null, substMap));
+ var ex = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, substE));
+ builder.Add(Assert(s.Tok, ex, "cannot establish the existence of LHS values that satisfy the such-that predicate"));
+ }
// End by doing the assume
- TrStmt(s.Assume, builder, locals, etran);
+ builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Expr)));
builder.Add(CaptureState(s.Tok)); // just do one capture state--here, at the very end (that is, don't do one before the assume)
} else if (stmt is UpdateStmt) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 8866491e..a64cf3f3 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -91,8 +91,10 @@ TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the
TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
-34 resolution/type errors detected in TypeTests.dfy
+36 resolution/type errors detected in TypeTests.dfy
-------------------- NatTypes.dfy --------------------
NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
@@ -280,7 +282,7 @@ Execution trace:
(0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-SmallTests.dfy(584,18): Error: target object may be null
+SmallTests.dfy(584,25): Error: target object may be null
Execution trace:
(0,0): anon0
SmallTests.dfy(597,10): Error: assertion violation
@@ -1720,7 +1722,7 @@ Execution trace:
(0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-SmallTests.dfy(584,18): Error: target object may be null
+SmallTests.dfy(584,25): Error: target object may be null
Execution trace:
(0,0): anon0
SmallTests.dfy(597,10): Error: assertion violation
@@ -1868,7 +1870,7 @@ Execution trace:
(0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-out.tmp.dfy(530,18): Error: target object may be null
+out.tmp.dfy(530,25): Error: target object may be null
Execution trace:
(0,0): anon0
out.tmp.dfy(543,10): Error: assertion violation
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index ab711d02..f260edb5 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -103,6 +103,6 @@ method M1() {
method M2() {
var a := new int[100];
parallel (x | 0 <= x < 100) {
- a[x] :| a[x] > 0; // error: not allowed to update heap location in a parallel statement with a(n implicit) assume
+ a[x] :| assume a[x] > 0; // error: not allowed to update heap location in a parallel statement with an assume
}
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 4d219cd3..e8b618d7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -542,21 +542,21 @@ method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)
ensures x == a && y == b;
{
if (*) {
- x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;
+ x, y :| assume a <= x < a + 1 && b + a <= y + a && y <= b;
} else {
- var xx, yy :| a <= xx < a + 1 && b + a <= yy + a && yy <= b;
+ var xx, yy :| assume a <= xx < a + 1 && b + a <= yy + a && yy <= b;
x, y := xx, yy;
}
}
method AssignSuchThat1(a: int, b: int) returns (x: int, y: int)
{
- var k :| 0 <= k < a - b; // this acts like an 'assume 0 < a - b;'
+ var k :| assume 0 <= k < a - b; // this acts like an 'assume 0 < a - b;'
assert b < a;
- k :| k == old(2*k); // note, the 'old' has no effect on local variables like k
+ k :| assume k == old(2*k); // note, the 'old' has no effect on local variables like k
assert k == 0;
var S := {2, 4, 7};
- var T :| T <= S;
+ var T :| assume T <= S;
assert 3 !in T;
assert T == {}; // error: T may be larger
}
@@ -568,38 +568,38 @@ method AssignSuchThat2(i: int, j: int, ghost S: set<Node>)
var a := new int[25];
var t;
if (0 <= i < j < 25) {
- a[i], t, a[j], n.next, n :| true;
+ a[i], t, a[j], n.next, n :| assume true;
}
if (n != null && n.next != null) {
assume n in S && n.next in S;
- n.next.next, n.next :| n != null && n.next != null && n.next.next == n.next; // error: n.next may equal n (thus aliasing n.next.next and n.next)
+ n.next.next, n.next :| assume n != null && n.next != null && n.next.next == n.next; // error: n.next may equal n (thus aliasing n.next.next and n.next)
} else if (0 <= i < 25 && 0 <= j < 25) {
- t, a[i], a[j] :| t < a[i] < a[j]; // error: i may equal j (thus aliasing a[i] and a[j])
+ t, a[i], a[j] :| assume t < a[i] < a[j]; // error: i may equal j (thus aliasing a[i] and a[j])
}
}
method AssignSuchThat3()
{
var n := new Node;
- n, n.next :| n.next == n; // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)
+ n, n.next :| assume n.next == n; // error: RHS is not well defined (RHS is evaluated after the havocking of the LHS)
}
method AssignSuchThat4()
{
var n := new Node;
- n, n.next :| n != null && n.next == n; // that's the ticket
+ n, n.next :| assume n != null && n.next == n; // that's the ticket
}
method AssignSuchThat5()
{
var n := new Node;
- n :| fresh(n); // fine
+ n :| assume fresh(n); // fine
assert false; // error
}
method AssignSuchThat6()
{
var n: Node;
- n :| n != null && fresh(n); // there is no non-null fresh object, so this amounts to 'assume false;'
+ n :| assume n != null && fresh(n); // there is no non-null fresh object, so this amounts to 'assume false;'
assert false; // no problemo
}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 29274381..8434f06c 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -92,3 +92,28 @@ method K(s: set<nat>) { // error: not allowed to instantiate 'set' with 'nat'
var b := new nat[100,200]; // error: not allowed the type array2<nat>
}
+// --------------------- more ghost tests, for assign-such-that statements
+
+method M()
+{
+ ghost var b: bool;
+ ghost var k: int, l: int;
+ var m: int;
+
+ // These three statements are allowed by the resolver, but the compiler will complain
+ // if it ever gets them.
+ k :| k < 10;
+ k, m :| 0 <= k < m;
+ m :| m < 10;
+
+ // Because of the ghost guard, these 'if' statements are ghost contexts, so only
+ // assignments to ghosts are allowed.
+ if (b) {
+ k :| k < 10; // should be allowed
+ k, l :| 0 <= k < l; // ditto
+ }
+ if (b) {
+ m :| m < 10; // error: not allowed in ghost context
+ k, m :| 0 <= k < m; // error: not allowed in ghost context
+ }
+}
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index b0bbfe05..93524dfa 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -41,7 +41,7 @@ Dafny program verifier finished with 22 verified, 0 errors
-------------------- MajorityVote.dfy --------------------
-Dafny program verifier finished with 7 verified, 0 errors
+Dafny program verifier finished with 11 verified, 0 errors
-------------------- SegmentSum.dfy --------------------
diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index 0adba718..a7512486 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -1,3 +1,62 @@
+// Rustan Leino, June 2012.
+// This file verifies an algorithm, due to Boyer and Moore, that finds the majority choice
+// among a sequence of votes, see http://www.cs.utexas.edu/~moore/best-ideas/mjrty/.
+// Actually, this algorithm is a slight variation on theirs, but the general idea for why
+// it is correct is the same. In the Boyer and Moore algorithm, the loop counter is advanced
+// by exactly 1 each iteration, which means that there may or may not be a "current leader".
+// In my program below, I had instead written the loop invariant to say there is always a
+// "current leader", which requires the loop index sometimes to skip a value.
+//
+// This file has two versions of the algorithm. In the first version, the given sequence
+// of votes is assumed to have a (strict) majority choice, meaning that strictly more than
+// 50% of the votes are for one candidate. It is convenient to have a name for the majority
+// choice, in order to talk about it in specifications. The easiest way to do this in
+// Dafny is probably to introduce a ghost parameter with the given properties. That's what
+// the algorithm does, see parameter K. The postcondition is thus to output the value of
+// K, which is done in the non-ghost out-parameter k.
+// The proof of the algorithm requires two lemmas. These lemmas are proved automatically
+// by Dafny's induction tactic.
+//
+// In the second version of the program, the main method does not assume there is a majority
+// choice. Rather, it eseentially uses the first algorithm and then checks if what it
+// returns really is a majority choice. To do this, the specification of the first algorithm
+// needs to be changed slightly to accommodate the possibility that there is no majority
+// choice. That change in specification is also reflected in the loop invariant. Moreover,
+// the algorithm itself now needs to extra 'if' statements to see if the entire sequence
+// has been searched through. (This extra 'if' is essentially already handled by Boyer and
+// Moore's algorithm, because it increments the loop index by 1 each iteration and therefore
+// already has a special case for the case of running out of sequence elements without a
+// current leader.)
+// The calling harness, DetermineElection, somewhat existentially comes up with the majority
+// choice, if there is such a choice, and then passes in that choice as the ghost parameter K
+// to the main algorithm. Neat, huh?
+
+// Advanced remark:
+// There is a subtle situation in the verification of DetermineElection. Suppose the type
+// parameter Candidate denotes some type whose instances depend on which object are
+// allocated. For example, if Candidate is some class type, then more candidates can come
+// into being by object allocations (using "new"). What does the quantification of
+// candidates "c" in the postcondition of DetermineElection now mean--all candidates that
+// existed in the pre-state or (the possibly larger set of) all candidates that exist in the
+// post-state? (It means the latter.) And if there does not exist a candidate in majority
+// in the pre-state, could there be a (newly created) candidate in majority in the post-state?
+// This will require some proof. The simplest argument seems to be that even if more candidates
+// are created during the course of DetermineElection, such candidates cannot possibly
+// be in majority in the sequence "a", since "a" can only contain candidates that were already
+// created in the pre-state. This property is easily specified by adding a postcondition
+// to the Count function. Alternatively, one could have added the antecedent "c in a" or
+// "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.
+
+function method Count<T>(a: seq<T>, s: int, t: int, x: T): int
+ requires 0 <= s <= t <= |a|;
+ ensures Count(a, s, t, x) == 0 || x in a;
+{
+ if s == t then 0 else
+ Count(a, s, t-1, x) + if a[t-1] == x then 1 else 0
+}
+
+// Here is the first version of the algorithm, the one that assumes there is a majority choice.
+
method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)
requires 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
ensures k == K; // find K
@@ -29,6 +88,62 @@ method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k:
Lemma_Unique(a, s, |a|, K, k); // both k and K have a majority, so K == k
}
+// ------------------------------------------------------------------------------
+
+// Here is the second version of the program, the one that also computes whether or not
+// there is a majority choice.
+
+method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)
+ ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;
+ ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;
+{
+ ghost var b := exists c :: 2 * Count(a, 0, |a|, c) > |a|;
+ ghost var w :| b ==> 2 * Count(a, 0, |a|, w) > |a|;
+ cand := SearchForWinner(a, b, w);
+ return 2 * Count(a, 0, |a|, cand) > |a|, cand;
+}
+
+// The difference between SearchForWinner for FindWinner above are the occurrences of the
+// antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"
+// statement.
+
+method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)
+ requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
+ ensures hasWinner ==> k == K; // find K
+{
+ if (|a| == 0) { return; }
+ k := a[0];
+ var n, c, s := 1, 1, 0;
+ while (n < |a|)
+ invariant 0 <= s <= n <= |a|;
+ invariant hasWinner ==> 2 * Count(a, s, |a|, K) > |a| - s; // K has majority among a[s..]
+ invariant 2 * Count(a, s, n, k) > n - s; // k has majority among a[s..n]
+ invariant c == Count(a, s, n, k);
+ {
+ if (a[n] == k) {
+ n, c := n + 1, c + 1;
+ } else if (2 * c > n + 1 - s) {
+ n := n + 1;
+ } else {
+ n := n + 1;
+ // We have 2*Count(a, s, n, k) == n-s, and thus the following lemma
+ // lets us conclude 2*Count(a, s, n, K) <= n-s.
+ Lemma_Unique(a, s, n, K, k);
+ // We also have 2*Count(a, s, |a|, K) > |a|-s, and the following lemma
+ // tells us Count(a, s, |a|, K) == Count(a, s, n, K) + Count(a, n, |a|, K),
+ // and thus we can conclude 2*Count(a, n, |a|, K) > |a|-n.
+ Lemma_Split(a, s, n, |a|, K);
+ if (|a| == n) { return; }
+ k, n, c, s := a[n], n + 1, 1, n;
+ }
+ }
+ Lemma_Unique(a, s, |a|, K, k); // both k and K have a majority, so K == k
+}
+
+// ------------------------------------------------------------------------------
+
+// Here are two lemmas about Count that are used in the methods above.
+
ghost method Lemma_Split<T>(a: seq<T>, s: int, t: int, u: int, x: T)
requires 0 <= s <= t <= u <= |a|;
ensures Count(a, s, t, x) + Count(a, t, u, x) == Count(a, s, u, x);
@@ -54,10 +169,3 @@ ghost method Lemma_Unique<T>(a: seq<T>, s: int, t: int, x: T, y: T)
}
*/
}
-
-function Count<T>(a: seq<T>, s: int, t: int, x: T): int
- requires 0 <= s <= t <= |a|;
-{
- if s == t then 0 else
- Count(a, s, t-1, x) + if a[t-1] == x then 1 else 0
-}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-13 00:49:29 +0000