diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 9 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 60 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 10 | ||||
| -rw-r--r-- | Test/dafny0/MultiSets.dfy | 64 |
4 files changed, 138 insertions, 5 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 c98b311d..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));
}
}
@@ -5860,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);
@@ -5910,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) }
@@ -5998,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);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c2574860..27d8032f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -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
+ {
+ }
+}
|