diff options
| -rw-r--r-- | Dafny/Dafny.atg | 7 | ||||
| -rw-r--r-- | Dafny/DafnyAst.ssc | 4 | ||||
| -rw-r--r-- | Dafny/Parser.ssc | 7 | ||||
| -rw-r--r-- | Dafny/Printer.ssc | 10 | ||||
| -rw-r--r-- | Dafny/Resolver.ssc | 37 | ||||
| -rw-r--r-- | Dafny/Translator.ssc | 116 | ||||
| -rw-r--r-- | DafnyDriver/DafnyDriver.ssc | 5 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 20 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 84 |
10 files changed, 234 insertions, 64 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 069c88c3..33a1d903 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -753,7 +753,12 @@ ForeachStmt<out Statement! s> ( AssignStmt<out s> (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
| HavocStmt<out s> (. if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } .)
)
- "}" (. s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign); .)
+ "}" (. if (bodyAssign != null) {
+ s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
+ } else {
+ s = dummyStmt; // some error occurred in parsing the bodyAssign
+ }
+ .)
(. parseVarScope.PopMarker(); .)
.
diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc index b73bacc9..2a0fa32c 100644 --- a/Dafny/DafnyAst.ssc +++ b/Dafny/DafnyAst.ssc @@ -800,9 +800,9 @@ namespace Microsoft.Dafny public readonly Expression! Collection;
public readonly Expression! Range;
public readonly List<PredicateStmt!>! BodyPrefix;
- public readonly AssignStmt BodyAssign;
+ public readonly AssignStmt! BodyAssign;
- public ForeachStmt(Token! tok, BoundVar! boundVar, Expression! collection, Expression! range, List<PredicateStmt!>! bodyPrefix, AssignStmt bodyAssign) {
+ public ForeachStmt(Token! tok, BoundVar! boundVar, Expression! collection, Expression! range, List<PredicateStmt!>! bodyPrefix, AssignStmt! bodyAssign) {
this.BoundVar = boundVar;
this.Collection = collection;
this.Range = range;
diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc index 3a349f43..ca1eed51 100644 --- a/Dafny/Parser.ssc +++ b/Dafny/Parser.ssc @@ -1045,7 +1045,12 @@ List<Expression!>! decreases) { if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
} else Error(109);
Expect(6);
- s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
+ if (bodyAssign != null) {
+ s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
+ } else {
+ s = dummyStmt; // some error occurred in parsing the bodyAssign
+ }
+
parseVarScope.PopMarker();
}
diff --git a/Dafny/Printer.ssc b/Dafny/Printer.ssc index 93b793f2..cf3d8294 100644 --- a/Dafny/Printer.ssc +++ b/Dafny/Printer.ssc @@ -272,7 +272,7 @@ namespace Microsoft.Dafny { } else if (stmt is AssumeStmt) {
wr.Write("assume ");
- PrintExpression(((AssertStmt)stmt).Expr);
+ PrintExpression(((AssumeStmt)stmt).Expr);
wr.Write(";");
} else if (stmt is UseStmt) {
@@ -399,11 +399,9 @@ namespace Microsoft.Dafny { PrintStatement(t, ind);
wr.WriteLine();
}
- if (s.BodyAssign != null) {
- Indent(ind);
- PrintStatement(s.BodyAssign, ind);
- wr.WriteLine();
- }
+ Indent(ind);
+ PrintStatement(s.BodyAssign, ind);
+ wr.WriteLine();
Indent(indent);
wr.Write("}");
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc index 11dabf9d..953f429a 100644 --- a/Dafny/Resolver.ssc +++ b/Dafny/Resolver.ssc @@ -1016,18 +1016,19 @@ namespace Microsoft.Dafny { } else if (stmt is ForeachStmt) {
ForeachStmt s = (ForeachStmt)stmt;
- scope.PushMarker();
- bool b = scope.Push(s.BoundVar.Name, s.BoundVar);
- assert b; // since we just pushed a marker, we expect the Push to succeed
- ResolveType(s.BoundVar.Type);
- int prevErrorCount = ErrorCount;
-
+
ResolveExpression(s.Collection, true, true);
assert s.Collection.Type != null; // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) {
Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type);
}
+ scope.PushMarker();
+ bool b = scope.Push(s.BoundVar.Name, s.BoundVar);
+ assert b; // since we just pushed a marker, we expect the Push to succeed
+ ResolveType(s.BoundVar.Type);
+ int prevErrorCount = ErrorCount;
+
ResolveExpression(s.Range, true, true);
assert s.Range.Type != null; // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Range.Type, Type.Bool)) {
@@ -1038,19 +1039,19 @@ namespace Microsoft.Dafny { foreach (PredicateStmt ss in s.BodyPrefix) {
ResolveStatement(ss, specContextOnly);
}
- if (s.BodyAssign != null) {
- bool specOnly = specContextOnly ||
- (successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range)));
- ResolveStatement(s.BodyAssign, specOnly);
- // check for correct usage of BoundVar in LHS and RHS of this assignment
- FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr;
- IdentifierExpr obj = lhs == null ? null : lhs.Obj as IdentifierExpr;
- if (obj != null && obj.Var == s.BoundVar) {
- // exemplary!
- } else {
- Error(s, "assignment inside foreach must assign to a field of the bound variable of the foreach statement");
- }
+
+ bool specOnly = specContextOnly ||
+ (successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range)));
+ ResolveStatement(s.BodyAssign, specOnly);
+ // check for correct usage of BoundVar in LHS and RHS of this assignment
+ FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr;
+ IdentifierExpr obj = lhs == null ? null : lhs.Obj as IdentifierExpr;
+ if (obj != null && obj.Var == s.BoundVar) {
+ // exemplary!
+ } else {
+ Error(s, "assignment inside foreach must assign to a field of the bound variable of the foreach statement");
}
+
scope.PopMarker();
} else {
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc index 0615f644..d7841313 100644 --- a/Dafny/Translator.ssc +++ b/Dafny/Translator.ssc @@ -676,8 +676,9 @@ namespace Microsoft.Dafny { currentMethod = m;
Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
-
Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
+
+ // Add CEV prelude
builder.Add(Bpl.Cmd.SimpleAssign(m.tok, Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Add(Bpl.Expr.Ident("#cev_pc", Bpl.Type.Int), Bpl.Expr.Literal(1))));
foreach (Bpl.Variable p in proc.InParams) {
assert p != null;
@@ -700,6 +701,24 @@ namespace Microsoft.Dafny { new Bpl.IdentifierExprSeq()));
}
+ // set up the information used to verify the method's modifies clause
+ {
+ ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
+ // Declare a local variable $_Frame: [ref]bool
+ Bpl.IdentifierExpr theFrame = etran.TheFrame(m.tok); // this is a throw-away expression, used only to extract the name and type of the $_Frame variable
+ assert theFrame.Type != null; // follows from the postcondition of TheFrame
+ Bpl.LocalVariable frame = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, theFrame.Name, theFrame.Type));
+ localVariables.Add(frame);
+ // $_Frame := (lambda $o: ref :: $o != null && $Heap[$o,alloc] ==> $o in ModifiesClause);
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(m.tok, oVar);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(m.tok, o));
+ Bpl.Expr consequent = InRWClause(m.tok, o, m.Mod, etran, null, null);
+ Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(), new Bpl.VariableSeq(oVar), null, Bpl.Expr.Imp(ante, consequent));
+
+ builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));
+ }
+
Bpl.StmtList stmts = TrStmt2StmtList(builder, m.Body, localVariables, new ExpressionTranslator(this, predef, m.tok));
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,
@@ -1502,9 +1521,10 @@ namespace Microsoft.Dafny { {
List<BoilerplateTriple!> boilerplate = new List<BoilerplateTriple!>();
- boilerplate.Add(new BoilerplateTriple(tok, false, FrameCondition(tok, method.Mod, etranPre, etran), "frame condition does not hold", "frame condition"));
+ // the frame condition, which is free since it is checked with every heap update and call
+ boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, method.Mod, etranPre, etran), null, "frame condition"));
- // free specifications
+ // HeapSucc(S1, S2)
Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);
boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));
@@ -1701,21 +1721,38 @@ namespace Microsoft.Dafny { new Bpl.IdentifierExprSeq()));
} else if (stmt is CallStmt) {
- AddComment(builder, stmt, "call statement");
CallStmt s = (CallStmt)stmt;
foreach (VarDecl local in s.NewVars) {
TrStmt(local, builder, locals, etran);
}
+ AddComment(builder, stmt, "call statement");
Bpl.ExprSeq ins = new Bpl.ExprSeq();
assert s.Method != null; // follows from the fact that stmt has been successfully resolved
if (!s.Method.IsClass) {
ins.Add(etran.TrExpr(s.Receiver));
}
- for (int i = 0; i < s.Args.Count; i++) {
- Expression e = s.Args[i];
- Type t = s.Method.Ins[i].Type;
- ins.Add(etran.CondApplyBox(stmt.Tok, etran.TrExpr(e), (!)e.Type, t));
+
+ // Ideally, the modifies and decreases checks would be done after the precondition check,
+ // but Boogie doesn't give us a hook for that. So, we set up our own local variables here to
+ // store the actual parameters.
+ // Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
+ Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, 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?
+ Expression actual = s.Args[i];
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(stmt.Tok, etran.TrExpr(actual), (!)actual.Type, s.Method.Ins[i].Type));
+ builder.Add(cmd);
+ ins.Add(lhs);
}
+ // Also create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>(s.Lhs.Count);
for (int i = 0; i < s.Lhs.Count; i++) {
@@ -1734,27 +1771,26 @@ namespace Microsoft.Dafny { }
}
+ // Check modifies clause
+ {
+ // assert (forall o: ref :: o != null && $Heap[o,alloc] && o in CalleeModifiesClause ==> $_Frame[o]);
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(stmt.Tok, oVar);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(stmt.Tok, o));
+ Bpl.Expr calleeModifies = InRWClause(stmt.Tok, o, s.Method.Mod, etran, s.Receiver, substMap);
+ Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o);
+ Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(Bpl.Expr.And(ante, calleeModifies), inEnclosingFrame));
+ builder.Add(Assert(stmt.Tok, qq, "call may violate caller's modifies clause"));
+ }
+
+ // Check termination
if (currentMethod.Decreases.Count == 0 || exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {
// omit termination checking for calls in this context
} else {
- // Check termination. Ideally, this would be checked after the precondition check.
- // Create a local variable for each formal parameter, and assign each actual parameter to the corresponding local
- Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
- for (int i = 0; i < s.Method.Ins.Count; i++) {
- Formal p = s.Method.Ins[i];
- VarDecl local = new VarDecl(p.tok, p.Name, p.Type, p.IsGhost, null);
- local.type = local.OptionalType; // resolve local here
- IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);
- ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here
- substMap.Add(p, ie);
- locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));
- Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
- Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.TrExpr(s.Args[i]));
- builder.Add(cmd);
- }
CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);
}
+ // Make the call
Bpl.CallCmd call = new Bpl.CallCmd(stmt.Tok, s.Method.FullName, ins, outs);
builder.Add(call);
for (int i = 0; i < s.Lhs.Count; i++) {
@@ -1923,18 +1959,19 @@ namespace Microsoft.Dafny { } else if (stmt is ForeachStmt) {
AddComment(builder, stmt, "foreach statement");
ForeachStmt s = (ForeachStmt)stmt;
- // assert/assume (forall o: ref :: o in S ==> Expr);
+ // assert/assume (forall o: ref :: o in S && Range(o) ==> Expr);
+ // assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o]); // this checks the enclosing modifies clause
// var oldHeap := $Heap;
// havoc $Heap;
// assume $HeapSucc(oldHeap, $Heap);
- // assume (forall o: ref, f: Field :: $Heap[o,f] = oldHeap[o,f] || (f = F && o in S));
- // assume (forall o: ref :: o != null && o in S ==> $Heap[o,F] = RHS[$Heap := oldHeap]);
+ // assume (forall o: ref, f: Field :: $Heap[o,f] = oldHeap[o,f] || (f = F && o in S && Range(o)));
+ // assume (forall o: ref :: o != null && o in S && Range(o) ==> $Heap[o,F] = RHS[$Heap := oldHeap]);
// Note, $Heap[o,alloc] is intentionally omitted from the antecedent of the quantifier in the previous line. That
// allocatedness property should hold automatically, because the set/seq quantified is a program expression, which
// will have been constructed from allocated objects.
// For sets, "o in S" means just that. For sequences, "o in S" is:
// (exists i :: { Seq#Index(S,i) } 0 <= i && i < Seq#Length(S) && Seq#Index(S,i) == o)
-
+
Bpl.BoundVariable oVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.BoundVar.UniqueName, TrType(s.BoundVar.Type)));
Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(stmt.Tok, oVar);
@@ -1951,6 +1988,7 @@ namespace Microsoft.Dafny { // TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences
oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, o)));
}
+ oInS = Bpl.Expr.And(oInS, etran.TrExpr(s.Range));
foreach (PredicateStmt ps in s.BodyPrefix) {
int pieces = 0;
@@ -1975,6 +2013,14 @@ namespace Microsoft.Dafny { }
}
+ // Here comes: assert (forall o: ref :: o != null && o in S ==> $_Frame[o]);
+ Bpl.Expr body = Bpl.Expr.Imp(
+ Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS),
+ Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o));
+ Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
+ builder.Add(Assert(s.BodyAssign.Tok, qq, "foreach assignment may update an object not in the enclosing method's modifies clause"));
+
+ // Set up prevHeap
Bpl.IdentifierExpr prevHeap = GetPrevHeapVar_IdExpr(stmt.Tok, locals);
builder.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, prevHeap, etran.HeapExpr));
builder.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
@@ -1986,12 +2032,12 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(stmt.Tok, fVar);
Bpl.Expr heapOF = Bpl.Expr.SelectTok(stmt.Tok, etran.HeapExpr, o, f);
Bpl.Expr oldHeapOF = Bpl.Expr.SelectTok(stmt.Tok, prevHeap, o, f);
- Bpl.Expr body = Bpl.Expr.Or(
+ body = Bpl.Expr.Or(
Bpl.Expr.Eq(heapOF, oldHeapOF),
Bpl.Expr.And(
- Bpl.Expr.Eq(f, GetField((FieldSelectExpr)((!)s.BodyAssign).Lhs)),
+ Bpl.Expr.Eq(f, GetField((FieldSelectExpr)s.BodyAssign.Lhs)),
oInS));
- Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), body);
+ qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), body);
builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
// Here comes: assume (forall o: ref :: o != null && o in S ==> $Heap[o,F] = RHS[$Heap := oldHeap]);
@@ -2240,6 +2286,9 @@ namespace Microsoft.Dafny { } else {
FieldSelectExpr fse = (FieldSelectExpr)lhs;
assert fse.Field != null;
+ // check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj];
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(fse.Obj)), "assignment may update an object not in the enclosing method's modifies clause"));
+
Bpl.IdentifierExpr h = (Bpl.IdentifierExpr!)etran.HeapExpr; // TODO: is this cast always justified?
bRhs = etran.CondApplyBox(tok, bRhs, (!)((ExprRhs)rhs).Expr.Type, fse.Field.Type);
Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, h, etran.TrExpr(fse.Obj), new Bpl.IdentifierExpr(tok, GetField(fse.Field)), bRhs);
@@ -2320,6 +2369,13 @@ namespace Microsoft.Dafny { return new ExpressionTranslator(translator, predef, HeapExpr, true);
}
}
+
+ public Bpl.IdentifierExpr! TheFrame(Token! tok)
+ ensures result.Type != null;
+ {
+ Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(predef.RefType), Bpl.Type.Bool);
+ return new Bpl.IdentifierExpr(tok, "$_Frame", ty);
+ }
public Bpl.Expr! TrExpr(Expression! expr)
requires predef != null;
diff --git a/DafnyDriver/DafnyDriver.ssc b/DafnyDriver/DafnyDriver.ssc index fa86c6e7..dc6e20b4 100644 --- a/DafnyDriver/DafnyDriver.ssc +++ b/DafnyDriver/DafnyDriver.ssc @@ -490,6 +490,11 @@ namespace Microsoft.Boogie program.Emit(new TokenTextWriter(Console.Out));
}
+ if (CommandLineOptions.Clo.ExpandLambdas) {
+ LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+
// ---------- Verify ------------------------------------------------------------
if (!CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index e3a91ab2..d45db684 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -10,8 +10,6 @@ // pperm, had to write invariants over p and perm rather than pperm and we couldn't use
// "x in p".
-//would be nice if we could mark pperm as a ghost variable
-
class Queue<T> {
var contents: seq<T>;
method Init();
@@ -43,7 +41,7 @@ class Comparable { class Benchmark3 {
- method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)
+ method Sort(q: Queue<int>) returns (r: Queue<int>, ghost perm:seq<int>)
requires q != null;
modifies q;
ensures r != null && fresh(r);
@@ -59,7 +57,7 @@ class Benchmark3 { {
r := new Queue<int>;
call r.Init();
- var p:= [];
+ ghost var p:= [];
var n := 0;
while (n < |q.contents|)
@@ -72,7 +70,7 @@ class Benchmark3 { n := n + 1;
}
perm:= [];
- var pperm := p + perm;
+ ghost var pperm := p + perm;
while (|q.contents| != 0)
invariant |r.contents| == |old(q.contents)| - |q.contents|;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 1edbeedc..d46dc7fe 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -98,8 +98,26 @@ Execution trace: (0,0): anon3
(0,0): anon11_Then
(0,0): anon6
+SmallTests.dfy(95,5): Error: call may violate caller's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+ (0,0): anon3
+SmallTests.dfy(108,7): Error: call may violate caller's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+SmallTests.dfy(110,7): Error: call may violate caller's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+SmallTests.dfy(150,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+ (0,0): anon3
-Dafny program verifier finished with 6 verified, 4 errors
+Dafny program verifier finished with 10 verified, 8 errors
-------------------- Queue.dfy --------------------
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 6ac9879d..3a2ca13c 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -67,3 +67,87 @@ class Node { 12
}
}
+
+// ------------------ modifies clause tests ------------------------
+
+class Modifies {
+ var x: int;
+ var next: Modifies;
+
+ method A(p: Modifies)
+ modifies this, p;
+ {
+ x := x + 1;
+ while (p != null && p.x < 75)
+ decreases 75 - p.x;
+ {
+ p.x := p.x + 1;
+ }
+ }
+
+ method B(p: Modifies)
+ modifies this;
+ {
+ call A(this);
+ if (p == this) {
+ call p.A(p);
+ }
+ call A(p); // error: may violate modifies clause
+ }
+
+ method C(b: bool)
+ modifies this;
+ ensures !b ==> x == old(x) && next == old(next);
+ {
+ }
+
+ method D(p: Modifies, y: int)
+ requires p != null;
+ {
+ if (y == 3) {
+ call p.C(true); // error: may violate modifies clause
+ } else {
+ call p.C(false); // error: may violation modifies clause (the check is done without regard
+ // for the postcondition, which also makes sense, since there may, in
+ // principle, be other fields of the object that are not constrained by the
+ // postcondition)
+ }
+ }
+
+ method E()
+ modifies this;
+ {
+ call A(null); // allowed
+ }
+
+ method F(s: set<Modifies>)
+ modifies s;
+ {
+ foreach (m in s | 2 <= m.x) {
+ m.x := m.x + 1;
+ }
+ if (this in s) {
+ x := 2 * x;
+ }
+ }
+
+ method G(s: set<Modifies>)
+ modifies this;
+ {
+ var m := 3; // this is a different m
+
+ foreach (m in s | m == this) {
+ m.x := m.x + 1;
+ }
+ if (s <= {this}) {
+ foreach (m in s) {
+ m.x := m.x + 1;
+ }
+ call F(s);
+ }
+ foreach (m in s) {
+ assert m.x < m.x + 10; // nothing wrong with asserting something
+ m.x := m.x + 1; // error: may violate modifies clause
+ }
+ }
+}
|