diff options
| -rw-r--r-- | Dafny/Compiler.cs | 40 | ||||
| -rw-r--r-- | Dafny/DafnyAst.cs | 132 | ||||
| -rw-r--r-- | Dafny/Resolver.cs | 393 | ||||
| -rw-r--r-- | Dafny/Translator.cs | 72 | ||||
| -rw-r--r-- | Test/VSComp2010/Answer | 2 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem4-Queens.dfy | 54 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 14 | ||||
| -rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy | 125 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/dafny1/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny1/Induction.dfy | 19 |
11 files changed, 771 insertions, 84 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index dc7caac7..decc5223 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -102,7 +102,7 @@ namespace Microsoft.Dafny { void CompileBuiltIns(BuiltIns builtIns) {
wr.WriteLine("namespace Dafny {");
Indent(IndentAmount);
- wr.WriteLine("public class Helpers {");
+ wr.WriteLine("public partial class Helpers {");
foreach (var decl in builtIns.SystemModule.TopLevelDecls) {
if (decl is ArrayClassDecl) {
int dims = ((ArrayClassDecl)decl).Dims;
@@ -1262,7 +1262,43 @@ namespace Microsoft.Dafny { }
} else if (expr is QuantifierExpr) {
- Contract.Assert(false); throw new cce.UnreachableException(); // a quantifier is always a ghost
+ var e = (QuantifierExpr)expr;
+ Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds
+ var n = e.BoundVars.Count;
+ Contract.Assert(e.Bounds.Count == n);
+ for (int i = n; 0 <= --i; ) {
+ var bound = e.Bounds[i];
+ var bv = e.BoundVars[i];
+ // emit: Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
+ if (bound is QuantifierExpr.BoolBoundedPool) {
+ wr.Write("Dafny.Helpers.QuantBool(");
+ } else if (bound is QuantifierExpr.IntBoundedPool) {
+ var b = (QuantifierExpr.IntBoundedPool)bound;
+ wr.Write("Dafny.Helpers.QuantInt(");
+ TrExpr(b.LowerBound);
+ wr.Write(", ");
+ TrExpr(b.UpperBound);
+ wr.Write(", ");
+ } else if (bound is QuantifierExpr.SetBoundedPool) {
+ var b = (QuantifierExpr.SetBoundedPool)bound;
+ wr.Write("Dafny.Helpers.QuantSet(");
+ TrExpr(b.Set);
+ wr.Write(", ");
+ } else if (bound is QuantifierExpr.SeqBoundedPool) {
+ var b = (QuantifierExpr.SeqBoundedPool)bound;
+ wr.Write("Dafny.Helpers.QuantSeq(");
+ TrExpr(b.Seq);
+ wr.Write(", ");
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
+ }
+ wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");
+ wr.Write("{0} => ", bv.Name);
+ }
+ TrExpr(e.Body);
+ for (int i = 0; i < n; i++) {
+ wr.Write(")");
+ }
} else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index a8acb013..b26e1288 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -1732,6 +1732,10 @@ namespace Microsoft.Dafny { this.tok = tok;
}
+
+ public virtual IEnumerable<Expression> SubExpressions {
+ get { yield break; }
+ }
}
public class LiteralExpr : Expression {
@@ -1802,7 +1806,10 @@ namespace Microsoft.Dafny { this.DatatypeName = datatypeName;
this.MemberName = memberName;
this.Arguments = arguments;
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get { return Arguments; }
}
}
@@ -1835,8 +1842,6 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(name != null);
Name = name;
-
-
}
}
@@ -1851,7 +1856,10 @@ namespace Microsoft.Dafny { : base(tok) {
Contract.Requires(cce.NonNullElements(elements));
Elements = elements;
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get { return Elements; }
}
}
@@ -1882,7 +1890,6 @@ namespace Microsoft.Dafny { Contract.Invariant(FieldName != null);
}
-
public FieldSelectExpr(IToken tok, Expression obj, string fieldName)
: base(tok) {
Contract.Requires(tok != null);
@@ -1890,7 +1897,10 @@ namespace Microsoft.Dafny { Contract.Requires(fieldName != null);
this.Obj = obj;
this.FieldName = fieldName;
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return Obj; }
}
}
@@ -1918,6 +1928,14 @@ namespace Microsoft.Dafny { E0 = e0;
E1 = e1;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Seq;
+ if (E0 != null) yield return E0;
+ if (E1 != null) yield return E1;
+ }
+ }
}
public class MultiSelectExpr : Expression {
@@ -1939,6 +1957,15 @@ namespace Microsoft.Dafny { Array = array;
Indices = indices;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Array;
+ foreach (var e in Indices) {
+ yield return e;
+ }
+ }
+ }
}
public class SeqUpdateExpr : Expression {
@@ -1955,7 +1982,14 @@ namespace Microsoft.Dafny { Seq = seq;
Index = index;
Value = val;
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Seq;
+ yield return Index;
+ yield return Value;
+ }
}
}
@@ -1990,6 +2024,15 @@ namespace Microsoft.Dafny { this.Receiver = receiver;
this.Args = args;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Receiver;
+ foreach (var e in Args) {
+ yield return e;
+ }
+ }
+ }
}
public class OldExpr : Expression {
@@ -2008,6 +2051,10 @@ namespace Microsoft.Dafny { cce.Owner.AssignSame(this, expr);
E = expr;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return E; }
+ }
}
public class FreshExpr : Expression {
@@ -2023,6 +2070,10 @@ namespace Microsoft.Dafny { Contract.Requires(expr != null);
E = expr;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return E; }
+ }
}
public class AllocatedExpr : Expression
@@ -2039,6 +2090,10 @@ namespace Microsoft.Dafny { Contract.Requires(expr != null);
E = expr;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return E; }
+ }
}
public class UnaryExpr : Expression
@@ -2054,7 +2109,6 @@ namespace Microsoft.Dafny { Contract.Invariant(E != null);
}
-
public UnaryExpr(IToken tok, Opcode op, Expression e)
: base(tok) {
Contract.Requires(tok != null);
@@ -2063,6 +2117,10 @@ namespace Microsoft.Dafny { this.E = e;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return E; }
+ }
}
public class BinaryExpr : Expression {
@@ -2195,7 +2253,13 @@ namespace Microsoft.Dafny { this.Op = op;
this.E0 = e0;
this.E1 = e1;
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return E0;
+ yield return E1;
+ }
}
}
@@ -2209,10 +2273,36 @@ namespace Microsoft.Dafny { Contract.Invariant(Body != null);
}
-
public readonly Triggers Trigs;
public readonly Attributes Attributes;
+ public abstract class BoundedPool { }
+ public class IntBoundedPool : BoundedPool
+ {
+ public readonly Expression LowerBound;
+ public readonly Expression UpperBound;
+ public IntBoundedPool(Expression lowerBound, Expression upperBound) {
+ LowerBound = lowerBound;
+ UpperBound = upperBound;
+ }
+ }
+ public class SetBoundedPool : BoundedPool
+ {
+ public readonly Expression Set;
+ public SetBoundedPool(Expression set) { Set = set; }
+ }
+ public class SeqBoundedPool : BoundedPool
+ {
+ public readonly Expression Seq;
+ public SeqBoundedPool(Expression seq) { Seq = seq; }
+ }
+ public class BoolBoundedPool : BoundedPool
+ {
+ }
+
+ public List<BoundedPool> Bounds; // initialized and filled in by resolver; it remains null for quantifiers in specification contexts
+ // invariant bounds == null || bounds.Count == BoundVars.Count;
+
public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ body, Triggers trigs, Attributes attrs)
: base(tok) {
Contract.Requires(tok != null);
@@ -2223,7 +2313,10 @@ namespace Microsoft.Dafny { this.Body = body;
this.Trigs = trigs;
this.Attributes = attrs;
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return Body; }
}
}
@@ -2264,7 +2357,6 @@ namespace Microsoft.Dafny { public WildcardExpr(IToken tok)
: base(tok) {
Contract.Requires(tok != null);
-
}
}
@@ -2279,7 +2371,6 @@ namespace Microsoft.Dafny { Contract.Invariant(Els != null);
}
-
public ITEExpr(IToken tok, Expression test, Expression thn, Expression els)
: base(tok) {
Contract.Requires(tok != null);
@@ -2289,7 +2380,14 @@ namespace Microsoft.Dafny { this.Test = test;
this.Thn = thn;
this.Els = els;
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Test;
+ yield return Thn;
+ yield return Els;
+ }
}
}
@@ -2302,7 +2400,6 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(Cases));
}
-
public MatchExpr(IToken tok, Expression source, [Captured] List<MatchCaseExpr/*!*/>/*!*/ cases)
: base(tok) {
Contract.Requires(tok != null);
@@ -2310,8 +2407,15 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(cases));
this.Source = source;
this.Cases = cases;
+ }
-
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Source;
+ foreach (var mc in Cases) {
+ yield return mc.Body;
+ }
+ }
}
}
@@ -2368,7 +2472,6 @@ namespace Microsoft.Dafny { Contract.Invariant(ToType != null);
}
-
public BoxingCastExpr(Expression e, Type fromType, Type toType)
: base(e.tok) {
Contract.Requires(e != null);
@@ -2379,6 +2482,10 @@ namespace Microsoft.Dafny { FromType = fromType;
ToType = toType;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return E; }
+ }
}
public class UnboxingCastExpr : Expression { // an UnboxingCastExpr is used only as a temporary placeholding during translation
@@ -2392,7 +2499,6 @@ namespace Microsoft.Dafny { Contract.Invariant(ToType != null);
}
-
public UnboxingCastExpr(Expression e, Type fromType, Type toType)
: base(e.tok) {
Contract.Requires(e != null);
@@ -2403,6 +2509,10 @@ namespace Microsoft.Dafny { FromType = fromType;
ToType = toType;
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get { yield return E; }
+ }
}
public class MaybeFreeExpression {
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 82cb6651..09bed6dd 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -1091,8 +1091,10 @@ namespace Microsoft.Dafny { }
}
- public void ResolveStatement(Statement stmt, bool specContextOnly, Method method){Contract.Requires(stmt != null);Contract.Requires(method != null);
- Contract.Requires(!(stmt is LabelStmt)); // these should be handled inside lists of statements
+ public void ResolveStatement(Statement stmt, bool specContextOnly, Method method) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(method != null);
+ Contract.Requires(!(stmt is LabelStmt)); // these should be handled inside lists of statements
if (stmt is UseStmt) {
UseStmt s = (UseStmt)stmt;
s.IsGhost = true;
@@ -2157,10 +2159,8 @@ namespace Microsoft.Dafny { } else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
+ int prevErrorCount = ErrorCount;
scope.PushMarker();
- if (!specContext) {
- Error(expr, "quantifiers are allowed only in specification contexts");
- }
foreach (BoundVar v in e.BoundVars) {
if (!scope.Push(v.Name, v)) {
Error(v, "Duplicate bound-variable name: {0}", v.Name);
@@ -2178,6 +2178,17 @@ namespace Microsoft.Dafny { ResolveTriggers(e.Trigs, twoState);
scope.PopMarker();
expr.Type = Type.Bool;
+
+ if (prevErrorCount == ErrorCount) {
+ if (specContext) {
+ // any quantifier is allowed
+ } else {
+ // ...but in non-spec contexts, it is necessary to compile the quantifier, so only certain quantifiers
+ // whose bound variables draw their values from bounded pools of values are allowed. To check for such
+ // "bounded pools", this resolving code looks for certain patterns.
+ e.Bounds = DiscoverBounds(e);
+ }
+ }
} else if (expr is WildcardExpr) {
expr.Type = new SetType(new ObjectType());
@@ -2305,6 +2316,378 @@ namespace Microsoft.Dafny { expr.Type = Type.Flexible;
}
}
+
+ /// <summary>
+ /// Tries to find a bounded pool for each of the bound variables of "e". If this process fails, appropriate
+ /// error messages are reported and "null" is returned.
+ /// Requires "e" to be successfully resolved.
+ /// </summary>
+ List<QuantifierExpr.BoundedPool> DiscoverBounds(QuantifierExpr e) {
+ Contract.Requires(e != null);
+ Contract.Requires(e.Type != null); // a sanity check (but not a complete proof) that "e" has been resolved
+ Contract.Ensures(Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == e.BoundVars.Count);
+
+ var bounds = new List<QuantifierExpr.BoundedPool>();
+ for (int j = 0; j < e.BoundVars.Count; j++) {
+ var bv = e.BoundVars[j];
+ if (bv.Type == Type.Bool) {
+ // easy
+ bounds.Add(new QuantifierExpr.BoolBoundedPool());
+ } else {
+ // Go through the conjuncts of the range expression look for bounds.
+ Expression lowerBound = null;
+ Expression upperBound = null;
+ foreach (var conjunct in NormalizedConjuncts(e.Body, e is ExistsExpr)) {
+ var c = conjunct as BinaryExpr;
+ if (c == null) {
+ goto CHECK_NEXT_CONJUNCT;
+ }
+ var e0 = c.E0;
+ var e1 = c.E1;
+ var op = c.ResolvedOp;
+ int whereIsBv = SanitizeForBoundDiscovery(e.BoundVars, j, ref op, ref e0, ref e1);
+ if (whereIsBv < 0) {
+ goto CHECK_NEXT_CONJUNCT;
+ }
+ switch (op) {
+ case BinaryExpr.ResolvedOpcode.InSet:
+ if (whereIsBv == 0) {
+ bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
+ goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.InSeq:
+ if (whereIsBv == 0) {
+ bounds.Add(new QuantifierExpr.SetBoundedPool(e1));
+ goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.EqCommon:
+ if (bv.Type == Type.Int) {
+ var otherOperand = whereIsBv == 0 ? e1 : e0;
+ bounds.Add(new QuantifierExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));
+ goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.Gt:
+ case BinaryExpr.ResolvedOpcode.Ge:
+ Contract.Assert(false); throw new cce.UnreachableException(); // promised by postconditions of NormalizedConjunct and SanitizeForBoundDiscovery
+ case BinaryExpr.ResolvedOpcode.Lt:
+ if (whereIsBv == 0 && upperBound == null) {
+ upperBound = e1; // bv < E
+ } else if (whereIsBv == 1 && lowerBound == null) {
+ lowerBound = Plus(e0, 1); // E < bv
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.Le:
+ if (whereIsBv == 0 && upperBound == null) {
+ upperBound = Plus(e1, 1); // bv <= E
+ } else if (whereIsBv == 1 && lowerBound == null) {
+ lowerBound = e0; // E <= bv
+ }
+ break;
+ default:
+ break;
+ }
+ if (lowerBound != null && upperBound != null) {
+ // we have found two halves
+ bounds.Add(new QuantifierExpr.IntBoundedPool(lowerBound, upperBound));
+ goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ CHECK_NEXT_CONJUNCT: ;
+ }
+ // we have checked every conjunct in the range expression and still have not discovered good bounds
+ Error(e, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ return null;
+ }
+ CHECK_NEXT_BOUND_VARIABLE: ; // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)
+ }
+ return bounds;
+ }
+
+ /// <summary>
+ /// If the return value is negative, the resulting "op", "e0", and "e1" should not be used.
+ /// Otherwise, the following is true on return:
+ /// The new "e0 op e1" is equivalent to the old "e0 op e1".
+ /// One of "e0" and "e1" is the identifier "boundVars[bvi]"; the return value is either 0 or 1, and indicates which.
+ /// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".
+ /// Requires the initial value of "op" not to be Gt or Ge, and ensures the same about the final value of "op".
+ /// </summary>
+ int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, ref BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1)
+ {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Requires(boundVars != null);
+ Contract.Requires(0 <= bvi && bvi < boundVars.Count);
+ Contract.Ensures(Contract.Result<int>() < 2);
+
+ var bv = boundVars[bvi];
+
+ // make an initial assessment of where bv is; to continue, we need bv to appear in exactly one operand
+ var fv0 = FreeVariables(e0);
+ var fv1 = FreeVariables(e1);
+ Expression thisSide;
+ Expression thatSide;
+ int whereIsBv;
+ if (fv0.Contains(bv)) {
+ if (fv1.Contains(bv)) {
+ return -1;
+ }
+ whereIsBv = 0;
+ thisSide = e0; thatSide = e1;
+ } else if (fv1.Contains(bv)) {
+ whereIsBv = 1;
+ thisSide = e1; thatSide = e0;
+ } else {
+ return -1;
+ }
+
+ // Next, clean up the side where bv is by adjusting both sides of the expression
+ while (true) {
+ switch (op) {
+ case BinaryExpr.ResolvedOpcode.EqCommon:
+ case BinaryExpr.ResolvedOpcode.NeqCommon:
+ case BinaryExpr.ResolvedOpcode.Gt:
+ case BinaryExpr.ResolvedOpcode.Ge:
+ case BinaryExpr.ResolvedOpcode.Le:
+ case BinaryExpr.ResolvedOpcode.Lt:
+ var bin = thisSide as BinaryExpr;
+ if (bin != null) {
+ if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {
+ // Change "A+B op C" into either "A op C-B" or "B op C-A", depending on where we find bv among A and B.
+ if (!FreeVariables(bin.E1).Contains(bv)) {
+ thisSide = bin.E0;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E1);
+ } else {
+ thisSide = bin.E1;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E0);
+ }
+ ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ thatSide.Type = bin.Type;
+ continue; // continue simplifying
+
+ } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub) {
+ // Change "A-B op C" in a similar way.
+ if (!FreeVariables(bin.E1).Contains(bv)) {
+ // change to "A op C+B"
+ thisSide = bin.E0;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Add, thatSide, bin.E1);
+ ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Add;
+ } else {
+ // In principle, change to "-B op C-A" and then to "B dualOp A-C". But since we don't want
+ // to return with the operator being > or >=, we instead end with "A-C op B" and switch the
+ // mapping of thisSide/thatSide to e0/e1 (by inverting "whereIsBv").
+ thisSide = bin.E1;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, bin.E0, thatSide);
+ ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ whereIsBv = 1 - whereIsBv;
+ }
+ thatSide.Type = bin.Type;
+ continue; // continue simplifying
+ }
+ }
+ break; // done simplifying
+ default:
+ break; // done simplifying
+ }
+ break; // done simplifying
+ }
+
+ // Now, see if the interesting side is simply bv itself
+ if (thisSide is IdentifierExpr && ((IdentifierExpr)thisSide).Var == bv) {
+ // we're cool
+ } else {
+ // no, the situation is more complicated than we care to understand
+ return -1;
+ }
+
+ // Finally, check that the other side does not contain "bv" or any of the bound variables
+ // listed after "bv" in the quantifier.
+ var fv = FreeVariables(thatSide);
+ for (int i = bvi; i < boundVars.Count; i++) {
+ if (fv.Contains(boundVars[i])) {
+ return -1;
+ }
+ }
+
+ // As we return, also return the adjusted sides
+ if (whereIsBv == 0) {
+ e0 = thisSide; e1 = thatSide;
+ } else {
+ e0 = thatSide; e1 = thisSide;
+ }
+ return whereIsBv;
+ }
+
+ /// <summary>
+ /// Returns all conjuncts of "expr" in "polarity" positions. That is, if "polarity" is "true", then
+ /// returns the conjuncts of "expr" in positive positions; else, returns the conjuncts of "expr" in
+ /// negative positions. The method considers a canonical-like form of the expression that pushes
+ /// negations inwards far enough that one can determine what the result is going to be (so, almost
+ /// a negation normal form).
+ /// As a convenience, arithmetic inequalities are rewritten so that the negation of an arithmetic
+ /// inequality is never returned and the comparisons > and >= are never returned; the negation of
+ /// a common equality or disequality is rewritten analogously.
+ /// Requires "expr" to be successfully resolved.
+ /// </summary>
+ IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {
+ // We consider 5 cases. To describe them, define P(e)=Conjuncts(e,true) and N(e)=Conjuncts(e,false).
+ // * X ==> Y is treated as a shorthand for !X || Y, and so is described by the remaining cases
+ // * X && Y P(_) = P(X),P(Y) and N(_) = !(X && Y)
+ // * X || Y P(_) = (X || Y) and N(_) = N(X),N(Y)
+ // * !X P(_) = N(X) and N(_) = P(X)
+ // * else P(_) = else and N(_) = !else
+ // So for ==>, we have:
+ // * X ==> Y P(_) = P(!X || Y) = (!X || Y) = (X ==> Y)
+ // N(_) = N(!X || Y) = N(!X),N(Y) = P(X),N(Y)
+
+ // Binary expressions
+ var b = expr as BinaryExpr;
+ if (b != null) {
+ bool breakDownFurther = false;
+ bool p0 = polarity;
+ if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
+ breakDownFurther = polarity;
+ } else if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {
+ breakDownFurther = !polarity;
+ } else if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
+ breakDownFurther = !polarity;
+ p0 = !p0;
+ }
+ if (breakDownFurther) {
+ foreach (var c in NormalizedConjuncts(b.E0, p0)) {
+ yield return c;
+ }
+ foreach (var c in NormalizedConjuncts(b.E1, polarity)) {
+ yield return c;
+ }
+ yield break;
+ }
+ }
+
+ // Unary expression
+ var u = expr as UnaryExpr;
+ if (u != null && u.Op == UnaryExpr.Opcode.Not) {
+ foreach (var c in NormalizedConjuncts(u.E, !polarity)) {
+ yield return c;
+ }
+ yield break;
+ }
+
+ // no other case applied, so return the expression or its negation, but first clean it up a little
+ b = expr as BinaryExpr;
+ if (b != null) {
+ BinaryExpr.Opcode newOp;
+ BinaryExpr.ResolvedOpcode newROp;
+ bool swapOperands;
+ switch (b.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Gt: // A > B yield polarity ? (B < A) : (A <= B);
+ newOp = polarity ? BinaryExpr.Opcode.Lt : BinaryExpr.Opcode.Le;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.Lt : BinaryExpr.ResolvedOpcode.Le;
+ swapOperands = polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.Ge: // A >= B yield polarity ? (B <= A) : (A < B);
+ newOp = polarity ? BinaryExpr.Opcode.Le : BinaryExpr.Opcode.Lt;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.Le : BinaryExpr.ResolvedOpcode.Lt;
+ swapOperands = polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.Le: // A <= B yield polarity ? (A <= B) : (B < A);
+ newOp = polarity ? BinaryExpr.Opcode.Le : BinaryExpr.Opcode.Lt;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.Le : BinaryExpr.ResolvedOpcode.Lt;
+ swapOperands = !polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.Lt: // A < B yield polarity ? (A < B) : (B <= A);
+ newOp = polarity ? BinaryExpr.Opcode.Lt : BinaryExpr.Opcode.Le;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.Lt : BinaryExpr.ResolvedOpcode.Le;
+ swapOperands = !polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.EqCommon: // A == B yield polarity ? (A == B) : (A != B);
+ newOp = polarity ? BinaryExpr.Opcode.Eq : BinaryExpr.Opcode.Neq;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.EqCommon : BinaryExpr.ResolvedOpcode.NeqCommon;
+ swapOperands = false;
+ break;
+ case BinaryExpr.ResolvedOpcode.NeqCommon: // A != B yield polarity ? (A != B) : (A == B);
+ newOp = polarity ? BinaryExpr.Opcode.Neq : BinaryExpr.Opcode.Eq;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.NeqCommon : BinaryExpr.ResolvedOpcode.EqCommon;
+ swapOperands = false;
+ break;
+ default:
+ goto JUST_RETURN_IT;
+ }
+ if (newROp != b.ResolvedOp || swapOperands) {
+ b = new BinaryExpr(b.tok, newOp, swapOperands ? b.E1 : b.E0, swapOperands ? b.E0 : b.E1);
+ b.ResolvedOp = newROp;
+ b.Type = Type.Bool;
+ yield return b;
+ }
+ }
+ JUST_RETURN_IT: ;
+ if (polarity) {
+ yield return expr;
+ } else {
+ expr = new UnaryExpr(expr.tok, UnaryExpr.Opcode.Not, expr);
+ expr.Type = Type.Bool;
+ yield return expr;
+ }
+ }
+
+ Expression Plus(Expression e, int n) {
+ Contract.Requires(0 <= n);
+
+ var nn = new LiteralExpr(e.tok, n);
+ nn.Type = Type.Int;
+ var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Add, e, nn);
+ p.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;
+ p.Type = Type.Int;
+ return p;
+ }
+
+ /// <summary>
+ /// Returns the set of free variables in "expr".
+ /// Requires "expr" to be successfully resolved.
+ /// Ensures that the set returned has no aliases.
+ /// </summary>
+ ISet<IVariable> FreeVariables(Expression expr) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(expr.Type != null);
+
+ if (expr is IdentifierExpr) {
+ var e = (IdentifierExpr)expr;
+ return new HashSet<IVariable>() { e.Var };
+
+ } else if (expr is QuantifierExpr) {
+ var e = (QuantifierExpr)expr;
+ var s = FreeVariables(e.Body);
+ foreach (var bv in e.BoundVars) {
+ s.Remove(bv);
+ }
+ return s;
+
+ } else if (expr is MatchExpr) {
+ var e = (MatchExpr)expr;
+ var s = FreeVariables(e.Source);
+ foreach (MatchCaseExpr mc in e.Cases) {
+ var t = FreeVariables(mc.Body);
+ foreach (var bv in mc.Arguments) {
+ t.Remove(bv);
+ }
+ s.UnionWith(t);
+ }
+ return s;
+
+ } else {
+ ISet<IVariable> s = null;
+ foreach (var e in expr.SubExpressions) {
+ var t = FreeVariables(e);
+ if (s == null) {
+ s = t;
+ } else {
+ s.UnionWith(t);
+ }
+ }
+ return s == null ? new HashSet<IVariable>() : s;
+ }
+ }
void ResolveReceiver(Expression expr, bool twoState, bool specContext)
{
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index b641b69d..a480d2c4 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -1290,7 +1290,12 @@ namespace Microsoft.Dafny { // check that postconditions hold
foreach (Expression p in f.Ens) {
- bodyCheckBuilder.Add(Assert(p.tok, etran.TrExpr(p), "possible violation of function postcondition"));
+ bool splitHappened;
+ foreach (var s in TrSplitExpr(p, etran, out splitHappened)) {
+ if (!s.IsFree) {
+ bodyCheckBuilder.Add(Assert(s.E.tok, s.E, "possible violation of function postcondition"));
+ }
+ }
}
}
// Combine the two
@@ -3294,18 +3299,15 @@ namespace Microsoft.Dafny { Contract.Requires(expr.Type is BoolType);
Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));
- if (expr is BinaryExpr) {
- BinaryExpr bin = (BinaryExpr)expr;
- if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
- foreach (Expression e in Conjuncts(bin.E0)) {
- yield return e;
- }
- Contract.Assert(bin != null); // the necessity of this cast is a compiler bug, but perhaps an irrepairable one
- foreach (Expression e in Conjuncts(bin.E1)) {
- yield return e;
- }
- yield break;
+ var bin = expr as BinaryExpr;
+ if (bin != null && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
+ foreach (Expression e in Conjuncts(bin.E0)) {
+ yield return e;
+ }
+ foreach (Expression e in Conjuncts(bin.E1)) {
+ yield return e;
}
+ yield break;
}
yield return expr;
}
@@ -5068,20 +5070,60 @@ namespace Microsoft.Dafny { for (var a = e.Attributes; a != null; a = a.Prev) {
if (a.Name == "induction") {
- // return 'true', except if there is one argument and it is 'false'
+ // Here are the supported forms of the :induction attribute.
+ // :induction -- apply induction to all bound variables
+ // :induction false -- suppress induction, that is, don't apply it to any bound variable
+ // :induction L where L is a list consisting entirely of bound variables:
+ // -- apply induction to the specified bound variables
+ // :induction X where X is anything else
+ // -- treat the same as {:induction}, that is, apply induction to all
+ // bound variables
+
+ // Handle {:induction false}
if (a.Args.Count == 1) {
var arg = a.Args[0].E as LiteralExpr;
if (arg != null && arg.Value is bool && !(bool)arg.Value) {
if (CommandLineOptions.Clo.Trace) {
- Console.Write("Suppressing automatic induction on: ");
+ Console.Write("Suppressing automatic induction for: ");
new Printer(Console.Out).PrintExpression(e);
Console.WriteLine();
}
return new List<BoundVar>();
}
}
+
+ // Handle {:induction L}
+ if (a.Args.Count != 0) {
+ var L = new List<BoundVar>();
+ foreach (var arg in a.Args) {
+ var id = arg.E as IdentifierExpr;
+ var bv = id == null ? null : id.Var as BoundVar;
+ if (bv != null && e.BoundVars.Contains(bv)) {
+ // add to L, but don't add duplicates
+ if (!L.Contains(bv)) {
+ L.Add(bv);
+ }
+ } else {
+ goto USE_DEFAULT_FORM;
+ }
+ }
+ if (CommandLineOptions.Clo.Trace) {
+ string sep = "Applying requested induction on ";
+ foreach (var bv in L) {
+ Console.Write("{0}{1}", sep, bv.Name);
+ sep = ", ";
+ }
+ Console.Write(" of: ");
+ new Printer(Console.Out).PrintExpression(e);
+ Console.WriteLine();
+ }
+ return L;
+ USE_DEFAULT_FORM: ;
+ }
+
+ // We have the {:induction} case, or something to be treated in the same way
if (CommandLineOptions.Clo.Trace) {
- Console.Write("Applying requested induction on: ");
+ Console.Write("Applying requested induction on all bound variables of: ");
new Printer(Console.Out).PrintExpression(e);
Console.WriteLine();
}
diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer index 50f20679..dc523fdf 100644 --- a/Test/VSComp2010/Answer +++ b/Test/VSComp2010/Answer @@ -16,7 +16,7 @@ Compiled program written to out.cs -------------------- Problem4-Queens.dfy --------------------
-Dafny program verifier finished with 11 verified, 0 errors
+Dafny program verifier finished with 9 verified, 0 errors
Compiled program written to out.cs
-------------------- Problem5-DoubleEndedQueue.dfy --------------------
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index e73c644f..ef084674 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -1,5 +1,5 @@ // VSComp 2010, problem 4, N queens
-// Rustan Leino, 31 August 2010.
+// Rustan Leino, 31 August 2010, updated 24 March 2011.
//
// In the version of this program that I wrote during the week of VSTTE 2010, I had
// an unproved assumption. In this version, I simply changed the existential quantifier
@@ -11,17 +11,7 @@ // The correctness of this program relies on some properties of Queens boards. These
// are stated and proved as lemmas, which here are given in assert statements.
//
-// There are two annoyances in this program:
-//
-// One has to do with Dafny's split between ''ghost'' variables/code and ''physical''
-// variables/code. The ''ghost'' things are used by the verifier, but are ignored by
-// the compiler. This is generally good, since any additional specifications are ghost
-// state that are needed to convince the verifier that a program is correct (let alone
-// express what it means for the program to be correct) are not required at run time.
-// However, Dafny currently considers *all* quantifiers to be ghost-only, which
-// necessitates some duplication of the 'IsConsistent' condition.
-//
-// The other annoyance is that Dafny's proof-term representation of the function
+// There is an annoyance in this program. Dafny's proof-term representation of the function
// 'IsConsistent' implicitly takes the heap as an argument, despite the fact that
// 'IsConsistent' does not depend on any part of the heap. Dafny ought to be able
// to figure that out from the fact that 'IsConsistent' has no 'reads' clause.
@@ -29,6 +19,10 @@ // below are specified with an (easy-to-prove) postcondition that 'IsConsistent(B,p)'
// does not change for any 'B' and 'p', even if the method may change the heap in
// some way.
+//
+// The March 2011 update of this program was to make use of Dafny's new heuristics for
+// compiling quantifiers. This makes it possible to call IsConsistent, whose body uses
+// a universal quantifier, from non-ghost code, which simplifies this program.
// The Search method returns whether or not there exists an N-queens solution for the
@@ -50,7 +44,7 @@ method Search(N: int) returns (success: bool, board: seq<int>) // Given a board, this function says whether or not the queen placed in column 'pos'
// is consistent with the queens placed in columns to its left.
-static function IsConsistent(board: seq<int>, pos: int): bool
+static function method IsConsistent(board: seq<int>, pos: int): bool
{
0 <= pos && pos < |board| &&
(forall q :: 0 <= q && q < pos ==>
@@ -59,37 +53,6 @@ static function IsConsistent(board: seq<int>, pos: int): bool board[pos] - board[q] != pos - q)
}
-method CheckConsistent(board: seq<int>, pos: int) returns (b: bool)
- ensures b <==> IsConsistent(board, pos);
- ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p)));
-{
- // The Dafny compiler won't compile a function with a 'forall' inside. (This seems reasonable
- // in general, since quantifiers could range over all the integers. Here, however, where the
- // range of the quantifier is bounded, it just seems stupid.) Therefore, we
- // have to provide a method that computes the same thing as the function defines.
- if (0 <= pos && pos < |board|) {
- var p := 0;
- while (p < pos)
- invariant p <= pos;
- invariant (forall q :: 0 <= q && q < p ==>
- board[q] != board[pos] &&
- board[q] - board[pos] != pos - q &&
- board[pos] - board[q] != pos - q);
- {
- if (!(board[p] != board[pos] &&
- board[p] - board[pos] != pos - p &&
- board[pos] - board[p] != pos - p)) {
- b := false;
- return;
- }
- p := p + 1;
- }
- b := true;
- return;
- }
- b := false;
-}
-
// Here comes the method where the real work is being done. With an ultimate board size of 'N'
// in mind and given the consistent placement 'boardSoFar' of '|boardSoFar|' columns, this method
// will search for a solution for the remaining columns. If 'success' returns as 'true',
@@ -135,8 +98,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: {
// Let's try to extend the board-so-far with a queen in column 'n':
var candidateBoard := boardSoFar + [n];
- call consistent := CheckConsistent(candidateBoard, pos);
- if (consistent) {
+ if (IsConsistent(candidateBoard, pos)) {
// The new queen is consistent. Thus, 'candidateBoard' is consistent in column 'pos'.
// The consistency of the queens in columns left of 'pos' follows from the
// consistency of those queens in 'boardSoFar' and the fact that 'candidateBoard' is
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c33cf851..b1e12099 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -295,7 +295,7 @@ Execution trace: Definedness.dfy(208,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(231,30): Error: possible violation of function postcondition
+Definedness.dfy(231,46): Error: possible violation of function postcondition
Execution trace:
(0,0): anon0
(0,0): anon5_Else
@@ -321,7 +321,7 @@ Execution trace: (0,0): anon13_Else
(0,0): anon7
(0,0): anon9
-FunctionSpecifications.dfy(40,18): Error: possible violation of function postcondition
+FunctionSpecifications.dfy(40,24): Error: possible violation of function postcondition
Execution trace:
(0,0): anon12_Else
(0,0): anon15_Else
@@ -399,6 +399,16 @@ Execution trace: Dafny program verifier finished with 8 verified, 2 errors
+-------------------- NonGhostQuantifiers.dfy --------------------
+NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(57,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(61,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(86,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(94,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+7 resolution/type errors detected in NonGhostQuantifiers.dfy
+
-------------------- Modules0.dfy --------------------
Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy new file mode 100644 index 00000000..dd730e90 --- /dev/null +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -0,0 +1,125 @@ +// This file contains various tests of resolving quantifiers in ghost and non-ghost positions
+
+class MyClass<T> {
+ // This function is in a ghost context, so all is cool.
+ function GhostF(): bool
+ {
+ (forall n :: 2 <= n ==> (exists d :: n < d && d < 2*n))
+ }
+ // But try to make it a non-ghost function, and Dafny will object because it cannot compile the
+ // body into code that will terminate.
+ function method NonGhostF(): bool
+ {
+ (forall n :: 2 <= n ==> (exists d :: n < d && d < 2*n)) // error: can't figure out how to compile
+ }
+ // Add an upper bound to n and things are cool again.
+ function method NonGhostF_Bounded(): bool
+ {
+ (forall n :: 2 <= n && n < 1000 ==> (exists d :: n < d && d < 2*n))
+ }
+ // Although the heuristics applied are syntactic, they do see through the structure of the boolean
+ // operators ==>, &&, ||, and !. Hence, the following three variations of the previous function can
+ // also be compiled.
+ function method NonGhostF_Or(): bool
+ {
+ (forall n :: !(2 <= n && n < 1000) || (exists d :: n < d && d < 2*n))
+ }
+ function method NonGhostF_ImpliesImplies(): bool
+ {
+ (forall n :: 2 <= n ==> n < 1000 ==> (exists d :: n < d && d < 2*n))
+ }
+ function method NonGhostF_Shunting(): bool
+ {
+ (forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))
+ }
+
+ // Here are more tests
+
+ function method F(a: array<T>): bool
+ requires a != null;
+ reads a;
+ {
+ (exists i :: 0 <= i && i < a.Length / 2 && (forall j :: i <= j && j < a.Length ==> a[i] == a[j]))
+ }
+
+ function method G0(a: seq<T>): bool
+ {
+ (exists t :: t in a && (forall u :: u in a ==> u == t))
+ }
+ function method G1(a: seq<T>): bool
+ {
+ (exists ti :: 0 <= ti && ti < |a| && (forall ui :: 0 <= ui && ui < |a| ==> a[ui] == a[ti]))
+ }
+
+ // Regrettably, the heuristics don't know about transitivity:
+ function method IsSorted0(s: seq<int>): bool
+ {
+ (forall i, j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
+ }
+ function method IsSorted1(s: seq<int>): bool
+ {
+ (forall j, i :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
+ }
+ // Add the redundant conjunct "i < |s|" and things are fine.
+ function method IsSorted2(s: seq<int>): bool
+ {
+ (forall i, j :: 0 <= i && i < |s| && i < j && j < |s| ==> s[i] <= s[j])
+ }
+ // But if you switch the order of i and j, you need a different redundant conjunct.
+ function method IsSorted3(s: seq<int>): bool
+ {
+ (forall j, i :: 0 <= i && i < |s| && i < j && j < |s| ==> s[i] <= s[j]) // error: can't figure out how to compile
+ }
+ function method IsSorted4(s: seq<int>): bool
+ {
+ (forall j, i :: 0 <= i && 0 < j && i < j && j < |s| ==> s[i] <= s[j])
+ }
+
+ // The heuristics look at bound variables in the order given, as is illustrated by the following
+ // two functions.
+ function method Order0(S: seq<set<int>>): bool
+ {
+ (forall i, j :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j)
+ }
+ function method Order1(S: seq<set<int>>): bool
+ {
+ (forall j, i :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j) // error: can't figure out how to compile
+ }
+
+ // Quantifiers can be used in other contexts, too.
+ // For example, in assert statements and assignment statements.
+ method M(s: seq<int>) returns (r: bool, q: bool) {
+ assert (forall x :: x in s ==> 0 <= x);
+ r := (forall x :: x in s ==> x < 100);
+ q := (exists y :: y*y in s); // error: can't figure out how to compile
+ }
+ // And if expressions.
+ function method Select_Good(S: set<int>, a: T, b: T): T
+ {
+ if (forall x :: x in S ==> 0 <= x && x < 100) then a else b
+ }
+ function method Select_Bad(S: set<int>, a: T, b: T): T
+ {
+ if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b // error: can't figure out how to compile
+ }
+ // (the same thing, but in a ghost function is fine, though)
+ function Select_Bad_Ghost(S: set<int>, a: T, b: T): T
+ {
+ if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b
+ }
+ // And if statements
+/****
+ method N(s: seq<int>) returns (ghost g: int, h: int)
+ {
+ if ( (forall x :: x in s ==> 0 <= x) ) {
+ h := 0; g := 0;
+ }
+ if ( (forall x :: x*x in s ==> x < 100) ) { // this is fine, since the whole statement is a ghost statement
+ g := 2;
+ }
+ if ( (forall x :: x*x in s ==> x < 50) ) { // error: cannot compile this guard of a non-ghost if statement
+ h := 6;
+ }
+ }
+****/
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 3e9507ef..2c55a6b9 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -12,7 +12,7 @@ for %%f in (Simple.dfy) do ( )
for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy
- Array.dfy MultiDimArray.dfy
+ Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 4bf200cd..d9b32305 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -73,7 +73,7 @@ Dafny program verifier finished with 6 verified, 0 errors -------------------- Induction.dfy --------------------
-Dafny program verifier finished with 22 verified, 0 errors
+Dafny program verifier finished with 23 verified, 0 errors
-------------------- Rippling.dfy --------------------
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 4bd1f35b..f31d79f8 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -107,6 +107,25 @@ class IntegerInduction { call Theorem4();
}
}
+
+ // The body of this function method gives a single quantifier, which leads to an efficient
+ // way to check sortedness at run time. However, an alternative, and ostensibly more general,
+ // way to express sortedness is given in the function's postcondition. The alternative
+ // formulation may be easier to understand for a human and may also be more readily applicable
+ // for the program verifier. Dafny will show that postcondition holds, which ensures the
+ // equivalence of the two formulations.
+ // The proof of the postcondition requires induction. It would have been nicer to state it
+ // as one formula of the form "IsSorted(s) <==> ...", but then Dafny would never consider the
+ // possibility of applying induction. Instead, the "==>" and "<==" cases are given separately.
+ // Proving the "<==" case is simple; it's the "==>" case that requires induction.
+ // The example uses an attribute that requests induction on just "j". However, the proof also
+ // goes through by applying induction just on "i" or applying induction on both bound variables.
+ function method IsSorted(s: seq<int>): bool
+ ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);
+ ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);
+ {
+ (forall i :: 0 <= i && i+1 < |s| ==> s[i] <= s[i+1])
+ }
}
datatype Tree<T> {
|