diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 9 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 161 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 12 | ||||
| -rw-r--r-- | Test/dafny0/MultiSets.dfy | 64 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 38 |
5 files changed, 239 insertions, 45 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 8ca70bac..a605ba87 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -434,6 +434,15 @@ function $IsCanonicalBoolBox(BoxType): bool; axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));
axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);
+// The following function and axiom are used to obtain a $Box($Unbox(_)) wrapper around
+// certain expressions. Note that it assumes any booleans contained in the set are canonical
+// (which is the case for any set that occurs in an execution of a Dafny program).
+// The role of the parameter 'dummy' in the following is (an unfortunately clumsy construction
+// whose only purpose is) simply to tell Boogie how to instantiate the type parameter 'T'.
+function $IsGoodSet<T>(s: Set BoxType, dummy: T): bool;
+axiom (forall<T> ss: Set BoxType, dummy: T, bx: BoxType :: { $IsGoodSet(ss, dummy), ss[bx] }
+ $IsGoodSet(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx):T));
+
// ---------------------------------------------------------------
// -- Encoding of type names -------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 854b7b38..0130ebab 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3805,7 +3805,7 @@ namespace Microsoft.Dafny { if (includeInParams) {
foreach (Formal p in m.Ins) {
Bpl.Type varType = TrType(p.Type);
- Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
+ Bpl.Expr wh = GetExtendedWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);
inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));
}
}
@@ -5766,8 +5766,10 @@ namespace Microsoft.Dafny { return u.IsDatatype;
} else if (t.IsRefType) {
return u.IsRefType;
+ } else if (t is MultiSetType) {
+ return u is MultiSetType;
} else if (t is MapType) {
- return false;
+ return u is MapType;
} else {
Contract.Assert(t.IsTypeParameter);
return false; // don't consider any type parameters to be the same (since we have no comparison function for them anyway)
@@ -5791,39 +5793,60 @@ namespace Microsoft.Dafny { eq = Bpl.Expr.Iff(e0, e1);
less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);
atmost = Bpl.Expr.Imp(e0, e1);
- } else if (ty is IntType) {
- eq = Bpl.Expr.Eq(e0, e1);
- less = Bpl.Expr.Lt(e0, e1);
- atmost = Bpl.Expr.Le(e0, e1);
- if (includeLowerBound) {
- less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), e0), less);
- atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), e0), atmost);
+
+ } else if (ty is IntType || ty is SeqType || ty.IsDatatype) {
+ Bpl.Expr b0, b1;
+ if (ty is IntType) {
+ b0 = e0;
+ b1 = e1;
+ } else if (ty is SeqType) {
+ b0 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
+ b1 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
+ } else if (ty.IsDatatype) {
+ b0 = FunctionCall(tok, BuiltinFunction.DtRank, null, e0);
+ b1 = FunctionCall(tok, BuiltinFunction.DtRank, null, e1);
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException();
}
+ eq = Bpl.Expr.Eq(b0, b1);
+ less = Bpl.Expr.Lt(b0, b1);
+ atmost = Bpl.Expr.Le(b0, b1);
+ if (ty is IntType && includeLowerBound) {
+ less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), less);
+ atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), atmost);
+ }
+
} else if (ty is EverIncreasingType) {
eq = Bpl.Expr.Eq(e0, e1);
less = Bpl.Expr.Gt(e0, e1);
atmost = Bpl.Expr.Ge(e0, e1);
- } else if (ty is SetType) {
- eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, e0, e1);
- less = etran.ProperSubset(tok, e0, e1);
- atmost = FunctionCall(tok, BuiltinFunction.SetSubset, null, e0, e1);
- } else if (ty is SeqType) {
- Bpl.Expr b0 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);
- Bpl.Expr b1 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);
- eq = Bpl.Expr.Eq(b0, b1);
- less = Bpl.Expr.Lt(b0, b1);
- atmost = Bpl.Expr.Le(b0, b1);
- } else if (ty.IsDatatype) {
- Bpl.Expr b0 = FunctionCall(tok, BuiltinFunction.DtRank, null, e0);
- Bpl.Expr b1 = FunctionCall(tok, BuiltinFunction.DtRank, null, e1);
- eq = Bpl.Expr.Eq(b0, b1);
- less = Bpl.Expr.Lt(b0, b1);
- atmost = Bpl.Expr.Le(b0, b1);
+
+ } else if (ty is SetType || ty is MapType) {
+ Bpl.Expr b0, b1;
+ if (ty is SetType) {
+ b0 = e0;
+ b1 = e1;
+ } else if (ty is MapType) {
+ // for maps, compare their domains as sets
+ b0 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType(tok, predef.BoxType, predef.BoxType), e0);
+ b1 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType(tok, predef.BoxType, predef.BoxType), e1);
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException();
+ }
+ eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, b0, b1);
+ less = etran.ProperSubset(tok, b0, b1);
+ atmost = FunctionCall(tok, BuiltinFunction.SetSubset, null, b0, b1);
+
+ } else if (ty is MultiSetType) {
+ eq = FunctionCall(tok, BuiltinFunction.MultiSetEqual, null, e0, e1);
+ less = etran.ProperMultiset(tok, e0, e1);
+ atmost = FunctionCall(tok, BuiltinFunction.MultiSetSubset, null, e0, e1);
} else {
// reference type
- Bpl.Expr b0 = Bpl.Expr.Neq(e0, predef.Null);
- Bpl.Expr b1 = Bpl.Expr.Neq(e1, predef.Null);
+ Contract.Assert(ty.IsRefType); // otherwise, unexpected type
+ var b0 = Bpl.Expr.Neq(e0, predef.Null);
+ var b1 = Bpl.Expr.Neq(e1, predef.Null);
eq = Bpl.Expr.Iff(b0, b1);
less = Bpl.Expr.And(Bpl.Expr.Not(b0), b1);
atmost = Bpl.Expr.Imp(b0, b1);
@@ -5837,6 +5860,39 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));
}
+ /// <summary>
+ /// This method can give a strong 'where' condition than GetWhereClause. However, the additional properties
+ /// are such that they would take effort (both in prover time and time spent designing more axioms) in order
+ /// for the prover to be able to establish them. Hence, these properties are applied more selectively. Applying
+ /// properties selectively is dicey and can easily lead to soundness issues. Therefore, these properties are
+ /// applied to method in-parameters.
+ /// </summary>
+ Bpl.Expr GetExtendedWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran) {
+ Contract.Requires(tok != null);
+ Contract.Requires(x != null);
+ Contract.Requires(type != null);
+ Contract.Requires(etran != null);
+ Contract.Requires(predef != null);
+ var r = GetWhereClause(tok, x, type, etran);
+ type = type.Normalize();
+ if (type is SetType) {
+ var t = (SetType)type;
+ // $IsGoodSet(x, V), where V is a value whose type is the same as the element type of the set.
+ var ex = ExemplaryBoxValue(t.Arg);
+ if (ex != null) {
+ var p = FunctionCall(tok, "$IsGoodSet", Bpl.Type.Bool, x, ex);
+ r = r == null ? p : BplAnd(r, p);
+ }
+#if LATER_MAYBE
+ } else if (type.IsDatatype) {
+ UserDefinedType udt = (UserDefinedType)type;
+ var oneOfTheCases = FunctionCall(tok, "$IsA#" + udt.ResolvedClass.FullCompileName, Bpl.Type.Bool, x);
+ r = BplAnd(r, oneOfTheCases);
+#endif
+ }
+ return r;
+ }
+
Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran)
{
Contract.Requires(tok != null);
@@ -5887,17 +5943,18 @@ namespace Microsoft.Dafny { Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t#" + otherTmpVarCount, predef.BoxType));
otherTmpVarCount++;
Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);
- Bpl.Expr xSubT = Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, x, t), Bpl.Expr.Literal(0));
+ Bpl.Expr xSubT = Bpl.Expr.SelectTok(tok, x, t);
Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t);
Bpl.Expr isGoodMultiset = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);
Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);
if (wh != null) {
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
- var q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
+ var q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(Bpl.Expr.Lt(Bpl.Expr.Literal(0), xSubT), wh));
isGoodMultiset = Bpl.Expr.And(isGoodMultiset, q);
}
return isGoodMultiset;
+
} else if (type is SeqType) {
SeqType st = (SeqType)type;
// (forall i: int :: { Seq#Index(x,i) }
@@ -5975,6 +6032,26 @@ namespace Microsoft.Dafny { return null;
}
+ /// <summary>
+ /// Returns null or a Boogie expression whose type is the same as the translated, non-boxed
+ /// Dafny type "type". The method is always allowed to return null, if no such value is conveniently
+ /// available.
+ /// </summary>
+ Bpl.Expr ExemplaryBoxValue(Type type) {
+ Contract.Requires(type != null);
+ Contract.Requires(predef != null);
+ type = type.Normalize();
+ if (type is BoolType) {
+ return Bpl.Expr.Literal(false);
+ } else if (type is IntType) {
+ return Bpl.Expr.Literal(0);
+ } else if (type.IsRefType) {
+ return predef.Null;
+ } else {
+ return null;
+ }
+ }
+
Bpl.Expr GetBoolBoxCondition(Expr box, Type type) {
Contract.Requires(box != null);
Contract.Requires(type != null);
@@ -6959,17 +7036,13 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.SetNeq:
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1));
case BinaryExpr.ResolvedOpcode.ProperSubset:
- return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
- translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e0, e1),
- Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1)));
+ return ProperSubset(expr.tok, e0, e1);
case BinaryExpr.ResolvedOpcode.Subset:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e0, e1);
case BinaryExpr.ResolvedOpcode.Superset:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e1, e0);
case BinaryExpr.ResolvedOpcode.ProperSuperset:
- return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
- translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e1, e0),
- Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1)));
+ return ProperSubset(expr.tok, e1, e0);
case BinaryExpr.ResolvedOpcode.Disjoint:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetDisjoint, null, e0, e1);
case BinaryExpr.ResolvedOpcode.InSet:
@@ -6992,17 +7065,13 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.MapNeq:
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, translator.FunctionCall(expr.tok, BuiltinFunction.MapEqual, null, e0, e1));
case BinaryExpr.ResolvedOpcode.ProperMultiSubset:
- return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
- translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e0, e1),
- Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1)));
+ return ProperMultiset(expr.tok, e0, e1);
case BinaryExpr.ResolvedOpcode.MultiSubset:
return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e0, e1);
case BinaryExpr.ResolvedOpcode.MultiSuperset:
return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e1, e0);
case BinaryExpr.ResolvedOpcode.ProperMultiSuperset:
- return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
- translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e1, e0),
- Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1)));
+ return ProperMultiset(expr.tok, e1, e0);
case BinaryExpr.ResolvedOpcode.MultiSetDisjoint:
return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDisjoint, null, e0, e1);
case BinaryExpr.ResolvedOpcode.InMultiSet:
@@ -7331,10 +7400,18 @@ namespace Microsoft.Dafny { Contract.Requires(e1 != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
- return Bpl.Expr.And(
+ return Bpl.Expr.Binary(tok, BinaryOperator.Opcode.And,
translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e0, e1),
Bpl.Expr.Not(translator.FunctionCall(tok, BuiltinFunction.SetSubset, null, e1, e0)));
}
+ public Bpl.Expr ProperMultiset(IToken tok, Bpl.Expr e0, Bpl.Expr e1) {
+ Contract.Requires(tok != null);
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ return Bpl.Expr.Binary(tok, BinaryOperator.Opcode.And,
+ translator.FunctionCall(tok, BuiltinFunction.MultiSetSubset, null, e0, e1),
+ Bpl.Expr.Not(translator.FunctionCall(tok, BuiltinFunction.MultiSetEqual, null, e0, e1)));
+ }
public Bpl.Expr ProperPrefix(IToken tok, Bpl.Expr e0, Bpl.Expr e1) {
Contract.Requires(tok != null);
Contract.Requires(e0 != null);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index f99b0133..27d8032f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1066,7 +1066,7 @@ Execution trace: Termination.dfy(291,3): anon12_Else
(0,0): anon13_Else
-Dafny program verifier finished with 49 verified, 7 errors
+Dafny program verifier finished with 57 verified, 7 errors
-------------------- DTypes.dfy --------------------
DTypes.dfy(15,14): Error: assertion violation
@@ -1572,8 +1572,16 @@ CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost 2 resolution/type errors detected in CallStmtTests.dfy
-------------------- MultiSets.dfy --------------------
+MultiSets.dfy(157,3): Error BP5003: A postcondition might not hold on this return path.
+MultiSets.dfy(156,15): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+MultiSets.dfy(163,3): Error BP5003: A postcondition might not hold on this return path.
+MultiSets.dfy(162,15): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 22 verified, 0 errors
+Dafny program verifier finished with 38 verified, 2 errors
-------------------- PredExpr.dfy --------------------
PredExpr.dfy(4,12): Error: condition in assert expression might not hold
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index e74873e3..22b93442 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -100,4 +100,66 @@ method test11(a: array<int>, n: int, c: int) ensures multiset(a[c..n-1]) == multiset(a[c..n]) - multiset{a[n-1]};
{
-}
\ No newline at end of file +}
+
+// ----------- the following tests mostly have to do with sets -------------
+
+class BoxTests<G> {
+ // ---------- sets ----------
+ ghost method LemmaSet0<T>(a: set<T>, b: set<T>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method LemmaSet1(a: set<G>, b: set<G>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method LemmaSet2(a: set<int>, b: set<int>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method LemmaSet3(a: set<object>, b: set<object>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method LemmaSet4(a: set<bool>, b: set<bool>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b;
+ {
+ }
+
+ ghost method Lemma_NonEmpty(x : set<int>, y : set<int>)
+ requires x * y == {};
+ ensures x !! y;
+ {
+ assert forall k :: k !in (x*y);
+ }
+
+ // ---------- sequences (don't require any special tricks in the encoding) ----------
+ ghost method LemmaSeq(a: seq<int>, b: seq<int>)
+ requires |a| <= |b| && forall i :: 0 <= i < |a| ==> a[i] == b[i];
+ ensures a <= b;
+ {
+ }
+
+ // ---------- multisets ----------
+ ghost method LemmaMultiset0<T>(a: multiset<T>, b: multiset<T>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b; // error: this property does not hold for multisets
+ {
+ }
+
+ ghost method LemmaMultiset1(a: multiset<int>, b: multiset<int>)
+ requires forall x :: x in a ==> x in b;
+ ensures a <= b; // error: this property does not hold for multisets
+ {
+ }
+}
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index bc431450..83baade1 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -372,3 +372,41 @@ class DefaultDecreasesFunction { if x < 0 then -x else x
}
}
+
+// ----------------- multisets and maps ----------
+
+module MultisetTests {
+ function F(a: multiset<int>, n: nat): int
+ decreases a, n;
+ {
+ if n == 0 then 0 else F(a, n-1)
+ }
+
+ function F'(a: multiset<int>, n: nat): int // inferred decreases clause
+ {
+ if n == 0 then 0 else F'(a, n-1)
+ }
+
+ ghost method M(n: nat, b: multiset<int>)
+ ensures F(b, n) == 0; // proved via automatic induction
+ {
+ }
+}
+
+module MapTests {
+ function F(a: map<int,int>, n: nat): int
+ decreases a, n;
+ {
+ if n == 0 then 0 else F(a, n-1)
+ }
+
+ function F'(a: map<int,int>, n: nat): int // inferred decreases clause
+ {
+ if n == 0 then 0 else F'(a, n-1)
+ }
+
+ ghost method M(n: nat, b: map<int,int>)
+ ensures F(b, n) == 0; // proved via automatic induction
+ {
+ }
+}
|