summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Dafny/Translator.ssc165
-rw-r--r--Test/VSI-Benchmarks/b2.dfy2
-rw-r--r--Test/VSI-Benchmarks/b3.dfy6
-rw-r--r--Test/VSI-Benchmarks/b6.dfy90
-rw-r--r--Test/dafny0/Answer175
-rw-r--r--Test/dafny0/ListContents.dfy2
-rw-r--r--Test/dafny0/SchorrWaite.dfy4
-rw-r--r--Test/dafny0/SmallTests.dfy169
8 files changed, 474 insertions, 139 deletions
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 9750b620..89a02ce7 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -10,8 +10,6 @@ using Microsoft.Contracts;
using Bpl = Microsoft.Boogie;
using System.Text;
-// TODO: totality checks for statements
-
namespace Microsoft.Dafny {
public class Translator {
[NotDelayed]
@@ -691,7 +689,6 @@ namespace Microsoft.Dafny {
// play havoc with the heap according to the modifies clause
builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
- Bpl.IdentifierExprSeq outH = new Bpl.IdentifierExprSeq();
// assume (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] } $_Frame[o] || $Heap[o,f] == old($Heap)[o,f]);
Bpl.TypeVariable alpha = new Bpl.TypeVariable(m.tok, "alpha");
Bpl.BoundVariable oVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$o", predef.RefType));
@@ -708,10 +705,13 @@ namespace Microsoft.Dafny {
builder.Add(new Bpl.AssumeCmd(m.tok, qq));
// also play havoc with the out parameters
- foreach (Bpl.Variable! f in outParams) {
- outH.Add(new Bpl.IdentifierExpr(f.tok, f));
+ if (outParams.Length != 0) { // don't create an empty havoc statement
+ Bpl.IdentifierExprSeq outH = new Bpl.IdentifierExprSeq();
+ foreach (Bpl.Variable! f in outParams) {
+ outH.Add(new Bpl.IdentifierExpr(f.tok, f));
+ }
+ builder.Add(new Bpl.HavocCmd(m.tok, outH));
}
- builder.Add(new Bpl.HavocCmd(m.tok, outH));
// check wellformedness of postconditions
foreach (MaybeFreeExpression p in m.Ens) {
@@ -1662,6 +1662,16 @@ namespace Microsoft.Dafny {
return cmd;
}
+ Bpl.AssertCmd! AssertNS(Bpl.IToken! tok, Bpl.Expr! condition, string! errorMessage)
+ {
+ List<object!> args = new List<object!>();
+ args.Add(Bpl.Expr.Literal(0));
+ Bpl.QKeyValue kv = new Bpl.QKeyValue(tok, "subsumption", args, null);
+ Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition, kv);
+ cmd.ErrorData = "Error: " + errorMessage;
+ return cmd;
+ }
+
Bpl.Ensures! Ensures(Token! tok, bool free, Bpl.Expr! condition, string errorMessage, string comment)
{
Bpl.Ensures ens = new Bpl.Ensures(tok, free, condition, comment);
@@ -1699,10 +1709,10 @@ namespace Microsoft.Dafny {
if (stmt is AssertStmt) {
AddComment(builder, stmt, "assert statement");
AssertStmt s = (AssertStmt)stmt;
+ builder.Add(AssertNS(s.Expr.tok, IsTotal(s.Expr, etran), "assert condition must be well defined")); // totality check
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(Assert(stmt.Tok, etran.TrExpr(p), "assertion violation"));
+ builder.Add(Assert(p.tok, etran.TrExpr(p), "assertion violation"));
pieces++;
}
if (2 <= pieces) {
@@ -1711,12 +1721,13 @@ namespace Microsoft.Dafny {
} else if (stmt is AssumeStmt) {
AddComment(builder, stmt, "assume statement");
AssumeStmt s = (AssumeStmt)stmt;
- builder.Add(Assert(stmt.Tok, IsTotal(s.Expr, etran), "assume condition must be well defined")); // totality check
+ builder.Add(AssertNS(stmt.Tok, IsTotal(s.Expr, etran), "assume condition must be well defined")); // totality check
builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
} else if (stmt is UseStmt) {
AddComment(builder, stmt, "use statement");
UseStmt s = (UseStmt)stmt;
- builder.Add(Assert(stmt.Tok, IsTotal(s.Expr, etran), "use expression must be well defined")); // totality check
+ // Skip the totality check. This makes the 'use' statement easier to use and it has no executable analog anyhow
+ // builder.Add(Assert(stmt.Tok, IsTotal(s.Expr, etran), "use expression must be well defined")); // totality check
builder.Add(new Bpl.AssumeCmd(stmt.Tok, (s.EvalInOld ? etran.Old : etran).TrUseExpr(s.FunctionCallExpr)));
} else if (stmt is LabelStmt) {
AddComment(builder, stmt, "label statement"); // TODO: ouch, comments probably mess up what the label labels in the Boogie program
@@ -1795,6 +1806,7 @@ namespace Microsoft.Dafny {
Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified?
Expression actual = s.Args[i];
+ builder.Add(Assert(actual.tok, IsTotal(actual, etran), "argument must be well defined")); // totality check
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);
@@ -1865,7 +1877,13 @@ namespace Microsoft.Dafny {
builder.Add(new Bpl.CallCmd(s.Tok, "CevEvent",
new Bpl.ExprSeq(CevLocation(s.Tok), new Bpl.IdentifierExpr(s.Tok, "conditional_moment", predef.CevEventType)),
new Bpl.IdentifierExprSeq()));
- Bpl.Expr guard = s.Guard == null ? null : etran.TrExpr(s.Guard);
+ Bpl.Expr guard;
+ if (s.Guard == null) {
+ guard = null;
+ } else {
+ builder.Add(Assert(s.Guard.tok, IsTotal(s.Guard, etran), "if guard must be well defined")); // totality check
+ guard = etran.TrExpr(s.Guard);
+ }
Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
b.Add(new Bpl.CallCmd(s.Thn.Tok, "CevEvent",
new Bpl.ExprSeq(CevLocation(s.Thn.Tok), new Bpl.IdentifierExpr(s.Thn.Tok, "took_then_branch", predef.CevEventType)),
@@ -1907,6 +1925,13 @@ namespace Microsoft.Dafny {
ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
builder.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, preLoopHeap, etran.HeapExpr)); // TODO: does this screw up labeled breaks for this loop?
+ // the variable w is used to coordinate the definedness checking of the loop invariant
+ Bpl.LocalVariable wVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$w" + loopId, Bpl.Type.Bool));
+ Bpl.IdentifierExpr w = new Bpl.IdentifierExpr(stmt.Tok, wVar);
+ locals.Add(wVar);
+ // havoc w;
+ builder.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq(w)));
+
// CEV information
Bpl.LocalVariable preLoopCevPCVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$PreLoopCevPC" + loopId, Bpl.Type.Int));
locals.Add(preLoopCevPCVar);
@@ -1916,20 +1941,30 @@ namespace Microsoft.Dafny {
new Bpl.ExprSeq(CevLocation(stmt.Tok)),
new Bpl.IdentifierExprSeq(preLoopCevPC))); // TODO: does this screw up labeled breaks for this loop?
- Bpl.Expr guard = s.Guard == null ? null : etran.TrExpr(s.Guard);
List<Bpl.PredicateCmd!> invariants = new List<Bpl.PredicateCmd!>();
+ Bpl.StmtListBuilder invDefinednessBuilder = new Bpl.StmtListBuilder();
foreach (MaybeFreeExpression loopInv in s.Invariants) {
int pieces = 0;
- if (!loopInv.IsFree) {
+ if (loopInv.IsFree) {
+ // still check the free invariant to be well defined
+ invDefinednessBuilder.Add(AssertNS(loopInv.E.tok, IsTotal(loopInv.E, etran), "free loop invariant must be well defined")); // totality check
+ } else {
+ invDefinednessBuilder.Add(AssertNS(loopInv.E.tok, IsTotal(loopInv.E, etran), "loop invariant must be well defined")); // totality check
+ invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
foreach (Expression se in SplitExpr(loopInv.E, true)) {
- invariants.Add(Assert(se.tok, etran.TrExpr(se), "loop invariant violation"));
+ invariants.Add(Assert(se.tok, Bpl.Expr.Imp(w, etran.TrExpr(se)), "loop invariant violation"));
pieces++;
}
}
if (pieces != 1) {
- invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
+ invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
}
}
+ // check definedness of decreases clause
+ foreach (Expression e in s.Decreases) {
+ invDefinednessBuilder.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at top of each loop iteration")); // totality check
+ }
+ // include boilerplate invariants
foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(stmt.Tok, currentMethod, etranPreLoop, etran)) {
if (tri.IsFree) {
invariants.Add(new Bpl.AssumeCmd(stmt.Tok, tri.Expr));
@@ -1956,9 +1991,25 @@ namespace Microsoft.Dafny {
}
Bpl.StmtListBuilder loopBodyBuilder = new Bpl.StmtListBuilder();
+ // as the first thing inside the loop, generate: if (!w) { assert IsTotal(inv); assume false; }
+ invDefinednessBuilder.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));
+ loopBodyBuilder.Add(new Bpl.IfCmd(stmt.Tok, Bpl.Expr.Not(w), invDefinednessBuilder.Collect(stmt.Tok), null, null));
+ // generate: assert IsTotal(guard); if (!guard) { break; }
+ Bpl.Expr guard;
+ if (s.Guard == null) {
+ guard = null;
+ } else {
+ loopBodyBuilder.Add(Assert(s.Guard.tok, IsTotal(s.Guard, etran), "loop guard must be well defined")); // totality check
+ Bpl.StmtListBuilder guardBreak = new Bpl.StmtListBuilder();
+ guardBreak.Add(new Bpl.BreakCmd(s.Guard.tok, null));
+ loopBodyBuilder.Add(new Bpl.IfCmd(s.Guard.tok, Bpl.Expr.Not(etran.TrExpr(s.Guard)), guardBreak.Collect(s.Guard.tok), null, null));
+ guard = Bpl.Expr.True;
+ }
+ // CEV information
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()));
+ // termination checking
if (exists{Expression e in s.Decreases; e is WildcardExpr}) {
// omit termination checking for this loop
TrStmt(s.Body, loopBodyBuilder, locals, etran);
@@ -1971,7 +2022,6 @@ 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
- 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);
@@ -1982,18 +2032,13 @@ namespace Microsoft.Dafny {
// check definedness of decreases expressions
List<Token!> toks = new List<Token!>();
List<Type!> types = new List<Type!>();
- List<Bpl.Expr!> decrsTotal = new List<Bpl.Expr!>();
List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
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.
toks.Add(e.tok);
types.Add((!)e.Type);
- decrsTotal.Add(IsTotal(e, etran));
decrs.Add(etran.TrExpr(e));
}
- Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrsTotal, decrs, oldBfs, loopBodyBuilder, etran, " at end of loop iteration");
+ Bpl.Expr decrCheck = DecreasesCheck(toks, types, 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);
@@ -2006,12 +2051,13 @@ 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 && Range(o) ==> Expr);
+ // assert/assume (forall o: ref :: o != null && o in S && Range(o) ==> Expr);
+ // assert (forall o: ref :: o != null && o in S && Range(o) ==> IsTotal(RHS));
// 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 && Range(o)));
+ // assume (forall o: ref, f: Field :: $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && 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
@@ -2022,6 +2068,8 @@ namespace Microsoft.Dafny {
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);
+ // colection
+ builder.Add(Assert(s.Collection.tok, IsTotal(s.Collection, etran), "collection expression must be well defined"));
Bpl.Expr oInS;
if (s.Collection.Type is SetType) {
oInS = etran.TrInSet(stmt.Tok, o, s.Collection, ((SetType)s.Collection.Type).Arg);
@@ -2035,17 +2083,32 @@ 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(Bpl.Expr.Neq(o, predef.Null), oInS);
+
+ // range
+ Bpl.Expr qr = new Bpl.ForallExpr(s.Range.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(s.Range, etran)));
+ builder.Add(AssertNS(s.Range.tok, qr, "range expression must be well defined"));
oInS = Bpl.Expr.And(oInS, etran.TrExpr(s.Range));
+ // sequence of asserts and assumes and uses
foreach (PredicateStmt ps in s.BodyPrefix) {
int pieces = 0;
if (ps is AssertStmt) {
+ Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(ps.Expr, etran)));
+ builder.Add(AssertNS(ps.Expr.tok, q, "assert condition must be well defined")); // totality check
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));
+ q = new Bpl.ForallExpr(se.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
builder.Add(Assert(se.tok, q, "assertion violation"));
pieces++;
}
+ } else if (ps is AssumeStmt) {
+ Bpl.Expr eIsTotal = IsTotal(ps.Expr, etran);
+ Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, eIsTotal));
+ builder.Add(AssertNS(ps.Expr.tok, q, "assume condition must be well defined")); // totality check
+ } else {
+ assert ps is UseStmt;
+ // no totality check (see UseStmt case above)
}
if (pieces != 1) {
Bpl.Expr e;
@@ -2059,11 +2122,18 @@ namespace Microsoft.Dafny {
builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, q));
}
}
-
- // 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));
+
+ // Check RHS of assignment to be well defined
+ ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
+ if (rhsExpr != null) {
+ // assert (forall o: ref :: o != null && o in S && Range(o) ==> IsTotal(RHS));
+ Bpl.Expr bbb = Bpl.Expr.Imp(oInS, IsTotal(rhsExpr.Expr, etran));
+ Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);
+ builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined")); // totality check
+ }
+
+ // Here comes: assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o]);
+ Bpl.Expr body = Bpl.Expr.Imp(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"));
@@ -2073,7 +2143,7 @@ namespace Microsoft.Dafny {
builder.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
builder.Add(new Bpl.AssumeCmd(stmt.Tok, FunctionCall(stmt.Tok, BuiltinFunction.HeapSucc, null, prevHeap, etran.HeapExpr)));
- // Here comes: assume (forall<alpha> o: ref, f: Field alpha :: $Heap[o,f] = oldHeap[o,f] || (f = F && o in S));
+ // Here comes: assume (forall<alpha> o: ref, f: Field alpha :: $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
Bpl.TypeVariable alpha = new Bpl.TypeVariable(stmt.Tok, "alpha");
Bpl.BoundVariable fVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$f", predef.FieldName(stmt.Tok, alpha)));
Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(stmt.Tok, fVar);
@@ -2087,14 +2157,14 @@ namespace Microsoft.Dafny {
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]);
- Bpl.Expr heapOField = Bpl.Expr.SelectTok(stmt.Tok, etran.HeapExpr, o, GetField((FieldSelectExpr)(s.BodyAssign).Lhs));
- ExpressionTranslator oldEtran = new ExpressionTranslator(this, predef, prevHeap);
- body = Bpl.Expr.Imp(
- Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS),
- Bpl.Expr.Eq(heapOField, oldEtran.TrExpr(((ExprRhs)s.BodyAssign.Rhs).Expr)));
- qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
- builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
+ // Here comes: assume (forall o: ref :: o != null && o in S && Range(o) ==> $Heap[o,F] = RHS[$Heap := oldHeap]);
+ if (rhsExpr != null) {
+ Bpl.Expr heapOField = Bpl.Expr.SelectTok(stmt.Tok, etran.HeapExpr, o, GetField((FieldSelectExpr)(s.BodyAssign).Lhs));
+ ExpressionTranslator oldEtran = new ExpressionTranslator(this, predef, prevHeap);
+ body = Bpl.Expr.Imp(oInS, Bpl.Expr.Eq(heapOField, oldEtran.TrExpr(rhsExpr.Expr)));
+ qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
+ builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
+ }
// CEV information
builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHeap",
@@ -2117,7 +2187,6 @@ namespace Microsoft.Dafny {
int N = min{contextDecreases.Count, calleeDecreases.Count};
List<Token!> toks = new List<Token!>();
List<Type!> types = new List<Type!>();
- List<Bpl.Expr!> calleeTotal = new List<Bpl.Expr!>();
List<Bpl.Expr!> callee = new List<Bpl.Expr!>();
List<Bpl.Expr!> caller = new List<Bpl.Expr!>();
for (int i = 0; i < N; i++) {
@@ -2128,11 +2197,10 @@ namespace Microsoft.Dafny {
}
toks.Add(tok);
types.Add(e0.Type);
- calleeTotal.Add(IsTotal(e0, etran));
callee.Add(etran.TrExpr(e0));
caller.Add(etran.TrExpr(e1));
}
- Bpl.Expr decrExpr = DecreasesCheck(toks, types, calleeTotal, callee, caller, builder, etran, "");
+ Bpl.Expr decrExpr = DecreasesCheck(toks, types, callee, caller, builder, etran, "");
builder.Add(Assert(tok, decrExpr, "failure to decrease termination measure"));
}
@@ -2140,7 +2208,7 @@ namespace Microsoft.Dafny {
/// 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(List<Token!>! toks, List<Type!>! types, List<Bpl.Expr!>! total0, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,
+ Bpl.Expr! DecreasesCheck(List<Token!>! toks, List<Type!>! types, List<Bpl.Expr!>! ee0, List<Bpl.Expr!>! ee1,
Bpl.StmtListBuilder! builder, ExpressionTranslator! etran, string! suffixMsg)
requires predef != null;
requires types.Count == ee0.Count && ee0.Count == ee1.Count;
@@ -2156,10 +2224,6 @@ namespace Microsoft.Dafny {
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]
@@ -2169,16 +2233,13 @@ namespace Microsoft.Dafny {
for (int i = 0; i < k; i++) {
prefixIsLess = Bpl.Expr.Or(prefixIsLess, Less[i]);
}
- string component = N == 1 ? "" : " (component " + k + ")";
- Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(prefixIsLess, total0[k]), "decreases expression" + component + " must be well-defined" + suffixMsg);
- builder.Add(cmd);
-
if (types[k] is IntType) {
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(toks[k], Bpl.Expr.Or(bounded, Eq[k]), "decreases expression" + component + " must be bounded below by 0" + suffixMsg);
+ string component = N == 1 ? "" : " (component " + k + ")";
+ Bpl.Cmd cmd = Assert(toks[k], Bpl.Expr.Or(bounded, Eq[k]), "decreases expression" + component + " must be bounded below by 0" + suffixMsg);
builder.Add(cmd);
}
}
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 457bc894..7d964061 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -17,7 +17,7 @@ class Benchmark2 {
var high := a.Length();
while (low < high)
- invariant 0 <= low && high <= a.Length();
+ invariant 0 <= low && low <= high && high <= a.Length();
invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);
invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));
decreases high - low;
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index d45db684..37b73cba 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -61,10 +61,10 @@ class Benchmark3 {
var n := 0;
while (n < |q.contents|)
- invariant n <=|q.contents| ;
- invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
+ invariant n <= |q.contents|;
invariant n == |p|;
- decreases |q.contents| -n;
+ invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
+ decreases |q.contents| - n;
{
p := p + [n];
n := n + 1;
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index d320f9e9..90f484bd 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -6,22 +6,22 @@ class Collection<T> {
function Valid():bool
reads this, footprint;
{
- this in footprint
+ this in footprint
}
method GetCount() returns (c:int)
requires Valid();
ensures 0<=c;
{
- c:=|elements|;
+ c:=|elements|;
}
method Init()
modifies this;
ensures Valid() && fresh(footprint -{this});
{
- elements := [];
- footprint := {this};
+ elements := [];
+ footprint := {this};
}
method GetItem(i:int ) returns (x:T)
@@ -29,7 +29,7 @@ class Collection<T> {
requires 0<=i && i<|elements|;
ensures elements[i] ==x;
{
- x:=elements[i];
+ x:=elements[i];
}
method Add(x:T )
@@ -38,7 +38,7 @@ class Collection<T> {
ensures Valid() && fresh(footprint - old(footprint));
ensures elements == old(elements) + [x];
{
- elements:= elements + [x];
+ elements:= elements + [x];
}
method GetIterator() returns (iter:Iterator<T>)
@@ -63,7 +63,7 @@ class Iterator<T> {
function Valid():bool
reads this, footprint;
{
- this in footprint && c!= null && -1<= pos && null !in footprint
+ this in footprint && c!= null && -1<= pos && null !in footprint
}
method Init(coll:Collection<T>)
@@ -72,9 +72,9 @@ class Iterator<T> {
ensures Valid() && fresh(footprint -{this}) && pos ==-1;
ensures c == coll;
{
- c:= coll;
- pos:=-1;
- footprint := {this};
+ c:= coll;
+ pos:=-1;
+ footprint := {this};
}
method MoveNext() returns (b:bool)
@@ -83,22 +83,22 @@ class Iterator<T> {
ensures fresh(footprint - old(footprint)) && Valid() && pos == old(pos) + 1;
ensures b == HasCurrent() && c == old(c);
{
- pos:= pos+1;
- b:= pos < |c.elements|;
+ pos:= pos+1;
+ b:= pos < |c.elements|;
}
function HasCurrent():bool //???
- requires Valid();
- reads this, c;
+ requires Valid();
+ reads this, c;
{
- 0<= pos && pos < |c.elements|
+ 0<= pos && pos < |c.elements|
}
method GetCurrent() returns (x:T)
requires Valid() && HasCurrent();
ensures c.elements[pos] == x;
{
- x:=c.elements[pos];
+ x:=c.elements[pos];
}
}
@@ -106,34 +106,34 @@ class Iterator<T> {
class Client
{
- method Main()
- {
- var c:= new Collection<int>;
- call c.Init();
- call c.Add(33);
- call c.Add(45);
- call c.Add(78);
-
- var s:= [ ];
-
- call iter:=c.GetIterator();
- call b:= iter.MoveNext();
-
- while (b)
- invariant b == iter.HasCurrent() && fresh(iter.footprint) && iter.Valid();
- invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints
- invariant 0<= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;
- invariant iter.c == c;
- decreases |c.elements| - iter.pos;
- {
- call x:= iter.GetCurrent();
- s:= s + [x];
- call b:= iter.MoveNext();
- }
-
- assert s == c.elements; //verifies that the iterator returns the correct things
- call c.Add(100);
- }
-
+ method Main()
+ {
+ var c:= new Collection<int>;
+ call c.Init();
+ call c.Add(33);
+ call c.Add(45);
+ call c.Add(78);
+
+ var s:= [ ];
+
+ call iter := c.GetIterator();
+ call b := iter.MoveNext();
+
+ while (b)
+ invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);
+ invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints
+ invariant 0 <= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;
+ invariant iter.c == c;
+ decreases |c.elements| - iter.pos;
+ {
+ call x:= iter.GetCurrent();
+ s:= s + [x];
+ call b:= iter.MoveNext();
+ }
+
+ assert s == c.elements; //verifies that the iterator returns the correct things
+ call c.Add(100);
+ }
+
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a364d4e9..3186ae01 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -98,6 +98,12 @@ Execution trace:
(0,0): anon3
(0,0): anon11_Then
(0,0): anon6
+SmallTests.dfy(82,20): Error: decreases expression must be well defined at top of each loop iteration
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(81,5): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ (0,0): anon8_Then
SmallTests.dfy(95,5): Error: call may violate caller's modifies clause
Execution trace:
(0,0): anon0
@@ -141,103 +147,214 @@ Execution trace:
SmallTests.dfy(209,18): Error: target object may be null
Execution trace:
(0,0): anon0
+SmallTests.dfy(231,9): Error: LHS expression must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(232,12): Error: LHS expression must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(233,7): Error: RHS expression must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(238,18): Error: assert condition must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(239,5): Error: assume condition must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(244,16): Error: if guard must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(251,19): Error: loop guard must be well defined
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(251,5): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ SmallTests.dfy(251,5): anon9_Else
+ (0,0): anon3
+SmallTests.dfy(260,23): Error: decreases expression must be well defined at top of each loop iteration
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(259,5): anon13_LoopHead
+ (0,0): anon13_LoopBody
+ (0,0): anon14_Then
+SmallTests.dfy(266,17): Error: decreases expression must be well defined at top of each loop iteration
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(259,5): anon13_LoopHead
+ (0,0): anon13_LoopBody
+ SmallTests.dfy(259,5): anon14_Else
+ (0,0): anon3
+ (0,0): anon15_Then
+ (0,0): anon6
+ SmallTests.dfy(265,5): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ (0,0): anon17_Then
+SmallTests.dfy(276,22): Error: loop invariant must be well defined
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(275,5): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ (0,0): anon8_Then
+SmallTests.dfy(276,22): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(277,17): Error: decreases expression must be well defined at top of each loop iteration
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(275,5): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ (0,0): anon8_Then
+SmallTests.dfy(286,24): Error: loop guard must be well defined
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(286,5): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ SmallTests.dfy(286,5): anon8_Else
+ (0,0): anon3
+SmallTests.dfy(305,24): Error: loop guard must be well defined
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(299,5): anon13_LoopHead
+ (0,0): anon13_LoopBody
+ SmallTests.dfy(299,5): anon14_Else
+ (0,0): anon3
+ (0,0): anon15_Then
+ (0,0): anon6
+ SmallTests.dfy(305,5): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ SmallTests.dfy(305,5): anon17_Else
+ (0,0): anon9
+SmallTests.dfy(326,44): Error: loop invariant must be well defined
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(316,5): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ SmallTests.dfy(316,5): anon17_Else
+ (0,0): anon3
+ (0,0): anon18_Then
+ (0,0): anon6
+ SmallTests.dfy(324,5): anon19_LoopHead
+ (0,0): anon19_LoopBody
+ (0,0): anon20_Then
+SmallTests.dfy(347,21): Error: collection expression must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(349,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(351,33): Error: range expression must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(357,18): Error: RHS of assignment must be well defined
+Execution trace:
+ (0,0): anon0
+SmallTests.dfy(366,23): Error: loop invariant must be well defined
+Execution trace:
+ (0,0): anon0
+ SmallTests.dfy(364,5): anon7_LoopHead
+ (0,0): anon7_LoopBody
+ (0,0): anon8_Then
+SmallTests.dfy(366,23): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 30 verified, 16 errors
+Dafny program verifier finished with 43 verified, 38 errors
-------------------- Queue.dfy --------------------
-Dafny program verifier finished with 12 verified, 0 errors
+Dafny program verifier finished with 22 verified, 0 errors
-------------------- ListCopy.dfy --------------------
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 4 verified, 0 errors
-------------------- BinaryTree.dfy --------------------
-Dafny program verifier finished with 13 verified, 0 errors
+Dafny program verifier finished with 24 verified, 0 errors
-------------------- ListReverse.dfy --------------------
-Dafny program verifier finished with 1 verified, 0 errors
+Dafny program verifier finished with 2 verified, 0 errors
-------------------- ListContents.dfy --------------------
-Dafny program verifier finished with 5 verified, 0 errors
+Dafny program verifier finished with 9 verified, 0 errors
-------------------- SchorrWaite.dfy --------------------
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
-------------------- Termination.dfy --------------------
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 13 verified, 0 errors
-------------------- Use.dfy --------------------
-Use.dfy(15,5): Error: assertion violation
+Use.dfy(15,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(26,5): Error: assertion violation
+Use.dfy(26,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(35,5): Error: assertion violation
+Use.dfy(35,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(56,5): Error: assertion violation
+Use.dfy(56,12): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(88,5): Error: assertion violation
+Use.dfy(88,17): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(130,5): Error: assertion violation
+Use.dfy(130,23): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(152,5): Error: assertion violation
+Use.dfy(144,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(170,5): Error: assertion violation
+Use.dfy(144,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(215,5): Error: assertion violation
+Use.dfy(215,19): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 20 verified, 9 errors
+Dafny program verifier finished with 38 verified, 9 errors
-------------------- DTypes.dfy --------------------
-DTypes.dfy(15,5): Error: assertion violation
+DTypes.dfy(15,14): Error: assertion violation
Execution trace:
(0,0): anon0
-DTypes.dfy(28,5): Error: assertion violation
+DTypes.dfy(28,13): Error: assertion violation
Execution trace:
(0,0): anon0
-DTypes.dfy(54,5): Error: assertion violation
+DTypes.dfy(54,18): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 5 verified, 3 errors
+Dafny program verifier finished with 13 verified, 3 errors
-------------------- TypeParameters.dfy --------------------
-TypeParameters.dfy(41,5): Error: assertion violation
+TypeParameters.dfy(41,22): Error: assertion violation
Execution trace:
(0,0): anon0
-TypeParameters.dfy(63,5): Error: assertion violation
+TypeParameters.dfy(63,27): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 10 verified, 2 errors
+Dafny program verifier finished with 20 verified, 2 errors
-------------------- Datatypes.dfy --------------------
-Dafny program verifier finished with 6 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
-------------------- UnboundedStack.dfy --------------------
-Dafny program verifier finished with 7 verified, 0 errors
+Dafny program verifier finished with 12 verified, 0 errors
-------------------- SumOfCubes.dfy --------------------
-Dafny program verifier finished with 10 verified, 0 errors
+Dafny program verifier finished with 17 verified, 0 errors
-------------------- TerminationDemos.dfy --------------------
-Dafny program verifier finished with 7 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 07dc2f7e..62636ce5 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -75,7 +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|;
+ decreases if current != null then |current.list| else -1;
{
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/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index fb06d211..f429b9ed 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -115,7 +115,7 @@ class Main {
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
invariant (forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited));
- invariant (forall n: Node :: n.children == old(n.children));
+ invariant (forall n: Node :: n in S ==> n.children == old(n.children));
invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);
decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited;
{
@@ -205,7 +205,7 @@ class Main {
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
invariant (forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited));
- invariant (forall n :: n in stackNodes || n.children == old(n.children));
+ invariant (forall n :: n in S ==> n in stackNodes || n.children == old(n.children));
invariant (forall n :: n in stackNodes ==>
|n.children| == old(|n.children|) &&
(forall j :: 0 <= j && j < |n.children| ==>
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 3e626f25..3bf5ed3f 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -58,9 +58,9 @@ class Node {
}
function PoorlyDefined(x: int): int
- requires if next == null then 5/x < 20 else true; // ill-defined then branch
- requires if next == null then true else 0 <= 5/x; // ill-defined then branch
- requires if next.next == null then true else true; // ill-defined guard
+ requires if next == null then 5/x < 20 else true; // error: ill-defined then branch
+ requires if next == null then true else 0 <= 5/x; // error: ill-defined then branch
+ requires if next.next == null then true else true; // error: ill-defined guard
requires 10/x != 8; // this is well-defined, because we get here only if x is non-0
reads this;
{
@@ -79,9 +79,9 @@ class Modifies {
{
x := x + 1;
while (p != null && p.x < 75)
- decreases 75 - p.x;
- {
- p.x := p.x + 1;
+ decreases 75 - p.x; // error: not defined at top of each iteration (there's good reason to
+ { // insist on this; for example, the decrement check could not be performed
+ p.x := p.x + 1; // at the end of the loop body if p were set to null in the loop body)
}
}
@@ -213,3 +213,160 @@ class SoWellformed {
modifies s;
ensures next.xyz < 100; // fine
}
+
+// ---------------------- welldefinedness checks for statements -------------------
+
+class StatementTwoShoes {
+ var x: int;
+
+ function method F(b: int): StatementTwoShoes
+ requires 0 <= b;
+ {
+ this
+ }
+
+ method M(p: StatementTwoShoes, a: int)
+ modifies this, p;
+ {
+ p.x := a; // error: receiver may be null
+ F(a).x := a; // error: LHS may not be well defined
+ x := F(a-10).x; // error: RHS may not be well defined
+ }
+
+ method N(a: int, b: int)
+ {
+ assert 5 / a == 5 / a; // error: expression may not be well defined
+ assume 20 / b == 5; // error: expression may not be well defined
+ }
+
+ method O(a: int) returns (b: int)
+ {
+ if (20 / a == 5) { // error: expression may not be well defined
+ b := a;
+ }
+ }
+
+ method P(a: int)
+ {
+ while (20 / a == 5) { // error: expression may not be well defined
+ break;
+ }
+ }
+
+ method Q(a: int, b: int)
+ {
+ var i := 1;
+ while (i < a)
+ decreases F(i), F(a), a - i; // error: component 1 may not be well defined
+ {
+ i := i + 1;
+ }
+ i := 1;
+ while (i < a)
+ decreases F(b), a - i; // error: component 0 may not be well defined
+ {
+ i := i + 1;
+ }
+ }
+
+ method R(a: int)
+ {
+ var i := 0;
+ while (i < 100) // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption
+ invariant F(a) != null; // error: expression may not be well defined, and error: loop invariant may not hold
+ decreases F(a), 100 - i; // error: component 0 not well defined
+ {
+ i := i + 1;
+ }
+ }
+
+ method S(a: int)
+ {
+ var j := 0;
+ while (20 / a == 5 && j < 100) // error: guard may not be well defined
+ invariant j <= 100;
+ decreases F(101 - j), 100 - j;
+ {
+ j := j + 1;
+ }
+ }
+
+ method T(a: int)
+ requires a != 0 && 20 / a == 5;
+ {
+ var k := a;
+ var j := 0;
+ while (20 / k == 5 && j < 100) // fine
+ decreases 100 - j;
+ {
+ j := j + 1;
+ }
+ j := 0;
+ while (20 / k == 5 && j < 100) // error: guard may not be well defined
+ decreases 100 - j;
+ {
+ havoc k;
+ j := j + 1;
+ }
+ }
+
+ method U()
+ {
+ var i := 0;
+ while (i < 100)
+ invariant i <= 100;
+ decreases 100 - i;
+ invariant F(123 - i) == this;
+ {
+ i := i + 1;
+ }
+ i := 0;
+ while (i < 100)
+ decreases 100 - i;
+ invariant F(if i==77 then -3 else i) == this; // error: expression may not be well defined
+ {
+ i := i + 1;
+ if (i == 77) { i := i + 1; }
+ }
+ }
+
+ use function G(w: int): int { 5 }
+ function method H(x: int): int;
+
+ method V(s: set<StatementTwoShoes>, a: int, b: int)
+ modifies s;
+ {
+ use G(12 / b); // fine, because there are no welldefinedness checks on use statements
+ foreach (m in s | m.x < 200) // s may contain null, but the foreach excludes null
+ {
+ assume 0 <= m.x;
+ assert m.x < 1000;
+ use G(5 / m.x); // fine, because there are no welldefinedness checks on use statements
+ m.x := m.x + 1;
+ }
+ foreach (m in s + {F(a)}) // error: collection expression may not be well defined
+ {
+ m.x := 5; // error: possible modifies clause violation
+ }
+ foreach (m in s | F(H(m.x)) == this) // error: range expression may not be well defined
+ {
+ m.x := H(m.x);
+ }
+ foreach (m in s)
+ {
+ m.x := 100 / m.x; // error: RhS may not be well defined
+ }
+ }
+
+ method W(x: int)
+ {
+ var i := 0;
+ while (i < 100)
+ // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking
+ invariant 5 / x != 5 / x; // error: not well-defined, and error: loop invariant does not hold initially
+ decreases 100 - i;
+ {
+ i := i + 1;
+ }
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 23:28:12 +0000