summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl11
-rw-r--r--Source/Core/AbsyExpr.ssc2
-rw-r--r--Source/Dafny/Translator.ssc222
-rw-r--r--Test/VSI-Benchmarks/b3.dfy10
-rw-r--r--Test/VSI-Benchmarks/b4.dfy15
-rw-r--r--Test/VSI-Benchmarks/b6.dfy22
-rw-r--r--Test/VSI-Benchmarks/b7.dfy10
-rw-r--r--Test/VSI-Benchmarks/b8.dfy53
-rw-r--r--Test/dafny0/Answer8
-rw-r--r--Test/dafny0/TypeParameters.dfy44
-rw-r--r--Test/inline/Answer4
11 files changed, 243 insertions, 158 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 75c5777e..9615586a 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -148,10 +148,17 @@ axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }
// -- Boxing and unboxing ----------------------------------------
// ---------------------------------------------------------------
-function $Box<T>(T) returns (ref);
-function $Unbox<T>(ref) returns (T);
+type BoxType;
+
+function $Box<T>(T) returns (BoxType);
+function $Unbox<T>(BoxType) returns (T);
axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
+axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);
+axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
+axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
+axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);
+// note: an axiom like this for bool would not be sound
// ---------------------------------------------------------------
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index 78a796c2..c07db23b 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -1527,7 +1527,7 @@ namespace Microsoft.Boogie
stream.Write("(");
((!)args[0]).Emit(stream, opBindingStrength, false);
- stream.Write(FunctionName);
+ stream.Write("{0} ", FunctionName);
Type.Emit(stream, 0);
if (parensNeeded)
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 1028058f..33002065 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -89,9 +89,14 @@ namespace Microsoft.Dafny {
readonly PredefinedDecls predef;
internal class PredefinedDecls {
public readonly Bpl.Type! RefType;
+ public readonly Bpl.Type! BoxType;
public readonly Bpl.Type! CevTokenType;
public readonly Bpl.Type! CevVariableKind;
public readonly Bpl.Type! CevEventType;
+ private readonly Bpl.TypeSynonymDecl! setTypeCtor;
+ public Bpl.Type! SetType(Token! tok, Bpl.Type! ty) {
+ return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
+ }
private readonly Bpl.TypeCtorDecl! seqTypeCtor;
public Bpl.Type! SeqType(Token! tok, Bpl.Type! ty) {
return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));
@@ -110,14 +115,16 @@ namespace Microsoft.Dafny {
return new Bpl.IdentifierExpr(tok, allocField);
}
- public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! cevTokenType, Bpl.TypeCtorDecl! cevVariableKind, Bpl.TypeCtorDecl! cevEventType,
- Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
+ public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! boxType, Bpl.TypeCtorDecl! cevTokenType, Bpl.TypeCtorDecl! cevVariableKind, Bpl.TypeCtorDecl! cevEventType,
+ Bpl.TypeSynonymDecl! setTypeCtor, Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.Constant! allocField, Bpl.Constant! cevHeapNameConst) {
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
+ this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new Bpl.TypeSeq());
this.CevTokenType = new Bpl.CtorType(Token.NoToken, cevTokenType, new Bpl.TypeSeq());
this.CevVariableKind = new Bpl.CtorType(Token.NoToken, cevVariableKind, new Bpl.TypeSeq());
this.CevEventType = new Bpl.CtorType(Token.NoToken, cevEventType, new Bpl.TypeSeq());
+ this.setTypeCtor = setTypeCtor;
this.seqTypeCtor = seqTypeCtor;
this.fieldName = fieldNameType;
this.HeapType = heap.TypedIdent.Type;
@@ -139,9 +146,11 @@ namespace Microsoft.Dafny {
Bpl.TypeCtorDecl cevTokenType = null;
Bpl.TypeCtorDecl cevVariableKind = null;
Bpl.TypeCtorDecl cevEventType = null;
+ Bpl.TypeSynonymDecl setTypeCtor = null;
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
+ Bpl.TypeCtorDecl boxType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
Bpl.Constant cevHeapNameConst = null;
@@ -156,6 +165,8 @@ namespace Microsoft.Dafny {
classNameType = dt;
} else if (dt.Name == "ref") {
refType = dt;
+ } else if (dt.Name == "BoxType") {
+ boxType = dt;
} else if (dt.Name == "$token") {
cevTokenType = dt;
} else if (dt.Name == "var_locglob") {
@@ -163,6 +174,11 @@ namespace Microsoft.Dafny {
} else if (dt.Name == "cf_event") {
cevEventType = dt;
}
+ } else if (d is Bpl.TypeSynonymDecl) {
+ Bpl.TypeSynonymDecl dt = (Bpl.TypeSynonymDecl)d;
+ if (dt.Name == "Set") {
+ setTypeCtor = dt;
+ }
} else if (d is Bpl.Constant) {
Bpl.Constant c = (Bpl.Constant)d;
if (c.Name == "alloc") {
@@ -179,12 +195,16 @@ namespace Microsoft.Dafny {
}
if (seqTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Seq");
+ } else if (setTypeCtor == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type Set");
} else if (fieldNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
} else if (refType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ref");
+ } else if (boxType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type BoxType");
} else if (cevTokenType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type $token");
} else if (cevVariableKind == null) {
@@ -198,7 +218,7 @@ namespace Microsoft.Dafny {
} else if (cevHeapNameConst == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant #loc.$Heap");
} else {
- return new PredefinedDecls(refType, cevTokenType, cevVariableKind, cevEventType, seqTypeCtor, fieldNameType, heap, classNameType, allocField, cevHeapNameConst);
+ return new PredefinedDecls(refType, boxType, cevTokenType, cevVariableKind, cevEventType, setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, allocField, cevHeapNameConst);
}
return null;
}
@@ -352,17 +372,18 @@ namespace Microsoft.Dafny {
if (f.Type is SetType) {
SetType st = (SetType)f.Type;
if (st.Arg.IsRefType) {
- // axiom (forall h: [ref, Field x]x, o: ref, t: ref ::
+ // axiom (forall h: [ref, Field x]x, o: ref, t: BoxType ::
// { h[o,f][t] }
- // $IsGoodHeap(h) && o != null && h[o,alloc] && h[o,f][t] ==> t == null || h[t, alloc]);
- Bpl.BoundVariable tVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$t", predef.RefType));
+ // $IsGoodHeap(h) && o != null && h[o,alloc] && h[o,f][t] ==> UnBox(t) == null || h[UnBox(t), alloc]);
+ Bpl.BoundVariable tVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$t", predef.BoxType));
Bpl.Expr t = new Bpl.IdentifierExpr(f.tok, tVar);
Bpl.Expr oDotFsubT = Bpl.Expr.SelectTok(f.tok, oDotF, t);
+ Bpl.Expr unboxT = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, t);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotFsubT));
- Bpl.Expr goodRef = etran.GoodRef(f.tok, t, st.Arg);
- Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(ante, oDotFsubT), Bpl.Expr.Or(Bpl.Expr.Eq(t, predef.Null), goodRef));
+ Bpl.Expr goodRef = etran.GoodRef(f.tok, unboxT, st.Arg);
+ Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(ante, oDotFsubT), Bpl.Expr.Or(Bpl.Expr.Eq(unboxT, predef.Null), goodRef));
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar, tVar), tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
} else {
@@ -374,17 +395,18 @@ namespace Microsoft.Dafny {
if (st.Arg.IsRefType) {
// axiom (forall h: [ref, Field x]x, o: ref, i: int ::
// { Seq#Index(h[o,f], i) }
- // $IsGoodHeap(h) && o != null && h[o,alloc] && 0 <= i && i < Seq#Length(h[o,f]) ==> Seq#Index(h[o,f], i) == null || h[Seq#Index(h[o,f], i), alloc]);
+ // $IsGoodHeap(h) && o != null && h[o,alloc] && 0 <= i && i < Seq#Length(h[o,f]) ==> Unbox(Seq#Index(h[o,f], i)) == null || h[Unbox(Seq#Index(h[o,f], i)), alloc]);
Bpl.BoundVariable iVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(f.tok, iVar);
- Bpl.Expr oDotFsubI = FunctionCall(f.tok, BuiltinFunction.SeqIndex, predef.RefType, oDotF, i);
+ Bpl.Expr oDotFsubI = FunctionCall(f.tok, BuiltinFunction.SeqIndex, predef.BoxType, oDotF, i);
+ Bpl.Expr unbox = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, oDotFsubI);
Bpl.Expr range = InSeqRange(f.tok, i, oDotF, null, false);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotFsubI));
- Bpl.Expr goodRef = etran.GoodRef(f.tok, oDotFsubI, st.Arg);
- Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(ante, range), Bpl.Expr.Or(Bpl.Expr.Eq(oDotFsubI, predef.Null), goodRef));
+ Bpl.Expr goodRef = etran.GoodRef(f.tok, unbox, st.Arg);
+ Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(ante, range), Bpl.Expr.Or(Bpl.Expr.Eq(unbox, predef.Null), goodRef));
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar, iVar), tr, body);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
} else {
@@ -563,21 +585,25 @@ namespace Microsoft.Dafny {
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, "frame axiom for " + f.FullName));
}
- Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, List<Expression!>! rw, ExpressionTranslator! etran) {
+ Bpl.Expr! InRWClause(Token! tok, Bpl.Expr! o, List<Expression!>! rw, ExpressionTranslator! etran)
+ requires predef != null;
+ // requires o to denote an expression of type RefType
+ {
Bpl.Expr disjunction = null;
foreach (Expression e in rw) {
Bpl.Expr disjunct;
if (e.Type is SetType) {
- // old(e)[o]
- disjunct = etran.TrInSet(tok, o, e, null);
+ // old(e)[Box(o)]
+ disjunct = etran.TrInSet(tok, o, e, ((SetType)e.Type).Arg);
} else if (e.Type is SeqType) {
- // (exists i: int :: 0 <= i && i < Seq#Length(old(e)) ==> Seq#Index(old(e),i) == o)
+ // (exists i: int :: 0 <= i && i < Seq#Length(old(e)) ==> Seq#Index(old(e),i) == Box(o))
+ Bpl.Expr boxO = FunctionCall(tok, BuiltinFunction.Box, null, o);
Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);
Bpl.Expr iBounds = InSeqRange(tok, i, etran.TrExpr(e), null, false);
- Bpl.Expr XsubI = FunctionCall(tok, BuiltinFunction.SeqIndex, TrType(((SeqType)e.Type).Arg), etran.TrExpr(e), i);
+ Bpl.Expr XsubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, etran.TrExpr(e), i);
// TODO: the equality in the next line should be changed to one that understands extensionality
- disjunct = new Bpl.ExistsExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(iBounds, Bpl.Expr.Eq(XsubI, o)));
+ disjunct = new Bpl.ExistsExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(iBounds, Bpl.Expr.Eq(XsubI, boxO)));
} else {
// o == old(e)
disjunct = Bpl.Expr.Eq(o, etran.TrExpr(e));
@@ -768,7 +794,9 @@ namespace Microsoft.Dafny {
}
}
- void CheckWellformed(Expression! expr, Function func, Position pos, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran) {
+ void CheckWellformed(Expression! expr, Function func, Position pos, Bpl.StmtListBuilder! builder, ExpressionTranslator! etran)
+ requires predef != null;
+ {
if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr) {
// always allowed
} else if (expr is DisplayExpression) {
@@ -1168,14 +1196,14 @@ namespace Microsoft.Dafny {
} else if (type is IntType) {
return Bpl.Type.Int;
} else if (type.IsTypeParameter) {
- return predef.RefType;
+ return predef.BoxType;
} else if (type.IsRefType) {
// object and class types translate to ref
return predef.RefType;
} else if (type is SetType) {
- return new Bpl.MapType(Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(TrType(((SetType)type).Arg)), Bpl.Type.Bool);
+ return predef.SetType(Token.NoToken, predef.BoxType);
} else if (type is SeqType) {
- return predef.SeqType(Token.NoToken, TrType(((SeqType)type).Arg));
+ return predef.SeqType(Token.NoToken, predef.BoxType);
} else {
assert false; // unexpected type
}
@@ -1318,12 +1346,12 @@ namespace Microsoft.Dafny {
List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>(s.Lhs.Count);
for (int i = 0; i < s.Lhs.Count; i++) {
Expression e = s.Lhs[i];
- if (ExpressionTranslator.ModeledAsRef(((!)s.Method).Outs[i].Type) && !ExpressionTranslator.ModeledAsRef((!)e.Type)) {
+ if (ExpressionTranslator.ModeledAsBoxType(((!)s.Method).Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType((!)e.Type)) {
// we need an Unbox
- Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$tmp#" + otherTmpVarCount, predef.RefType));
+ Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$tmp#" + otherTmpVarCount, predef.BoxType));
otherTmpVarCount++;
locals.Add(var);
- Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(stmt.Tok, var.Name, predef.RefType);
+ Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(stmt.Tok, var.Name, predef.BoxType);
tmpOuts.Add(varIdE);
outs.Add(varIdE);
} else {
@@ -1340,7 +1368,7 @@ namespace Microsoft.Dafny {
Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e); // TODO: is this cast always justified?
if (tmpVarIdE != null) {
// e := UnBox(tmpVar);
- Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(stmt.Tok, lhs, FunctionSpecial(stmt.Tok, BuiltinFunction.Unbox, TrType((!)e.Type), tmpVarIdE));
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(stmt.Tok, lhs, FunctionCall(stmt.Tok, BuiltinFunction.Unbox, TrType((!)e.Type), tmpVarIdE));
builder.Add(cmd);
}
builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHere",
@@ -1574,13 +1602,13 @@ namespace Microsoft.Dafny {
Bpl.Expr oInS;
if (s.Collection.Type is SetType) {
- oInS = etran.TrInSet(stmt.Tok, o, s.Collection, null);
+ oInS = etran.TrInSet(stmt.Tok, o, s.Collection, ((SetType)s.Collection.Type).Arg);
} else {
Bpl.BoundVariable iVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$i", Bpl.Type.Int));
Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(stmt.Tok, iVar);
Bpl.Expr S = etran.TrExpr(s.Collection);
Bpl.Expr range = InSeqRange(stmt.Tok, i, S, null, false);
- Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, TrType(((SeqType!)s.Collection.Type).Arg), S, i);
+ Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);
Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));
// 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)));
@@ -1665,15 +1693,16 @@ namespace Microsoft.Dafny {
} else if (type is SetType) {
SetType st = (SetType)type;
if (st.Arg.IsRefType) {
- // (forall t: ref :: { x[t] } x[t] ==> t == null || $Heap[t,alloc])
- Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t", predef.RefType));
+ // (forall t: BoxType :: { x[t] } x[t] ==> Unbox(t) == null || $Heap[Unbox(t),alloc])
+ Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t", predef.BoxType));
Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);
Bpl.Expr xSubT = Bpl.Expr.SelectTok(tok, x, t);
+ Bpl.Expr unboxT = FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, t);
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
- Bpl.Expr goodRef = etran.GoodRef(tok, t, st.Arg);
- Bpl.Expr body = Bpl.Expr.Imp(xSubT, Bpl.Expr.Or(Bpl.Expr.Eq(t, predef.Null), goodRef));
+ Bpl.Expr goodRef = etran.GoodRef(tok, unboxT, st.Arg);
+ Bpl.Expr body = Bpl.Expr.Imp(xSubT, Bpl.Expr.Or(Bpl.Expr.Eq(unboxT, predef.Null), goodRef));
return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, body);
} else {
// TODO: should also handle sets of sets, etc.
@@ -1684,17 +1713,18 @@ namespace Microsoft.Dafny {
SeqType st = (SeqType)type;
if (st.Arg.IsRefType) {
// (forall i: int :: { Seq#Index(x,i) }
- // 0 <= i && i < Seq#Length(x) ==> Seq#Index(x,i) == null || $Heap[Seq#Index(x,i), alloc])
+ // 0 <= i && i < Seq#Length(x) ==> Unbox(Seq#Index(x,i)) == null || $Heap[Unbox(Seq#Index(x,i)), alloc])
Bpl.BoundVariable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);
- Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.RefType, x, i);
+ Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i);
+ Bpl.Expr unbox = FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, xSubI);
Bpl.Expr range = InSeqRange(tok, i, x, null, false);
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubI));
- Bpl.Expr goodRef = etran.GoodRef(tok, xSubI, st.Arg);
- Bpl.Expr body = Bpl.Expr.Imp(range, Bpl.Expr.Or(Bpl.Expr.Eq(xSubI, predef.Null), goodRef));
+ Bpl.Expr goodRef = etran.GoodRef(tok, unbox, st.Arg);
+ Bpl.Expr body = Bpl.Expr.Imp(range, Bpl.Expr.Or(Bpl.Expr.Eq(unbox, predef.Null), goodRef));
return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, body);
} else {
// TODO: should also handle sequences or sequences, etc.
@@ -1815,20 +1845,20 @@ namespace Microsoft.Dafny {
} else if (expr is SetDisplayExpr) {
SetDisplayExpr e = (SetDisplayExpr)expr;
- Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SetEmpty, translator.TrType((!)expr.Type));
+ Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
foreach (Expression ee in e.Elements) {
- Bpl.Expr ss = TrExpr(ee);
- s = translator.FunctionCall(expr.tok, BuiltinFunction.SetUnionOne, translator.TrType(expr.Type), s, ss);
+ Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), (!)ee.Type);
+ s = translator.FunctionCall(expr.tok, BuiltinFunction.SetUnionOne, predef.BoxType, s, ss);
}
return s;
} else if (expr is SeqDisplayExpr) {
SeqDisplayExpr e = (SeqDisplayExpr)expr;
- Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, translator.TrType((!)expr.Type));
+ Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
int i = 0;
foreach (Expression ee in e.Elements) {
- Bpl.Expr ss = TrExpr(ee);
- s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, translator.TrType(expr.Type), s, Bpl.Expr.Literal(i), ss, Bpl.Expr.Literal(i+1));
+ Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), (!)ee.Type);
+ s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, Bpl.Expr.Literal(i), ss, Bpl.Expr.Literal(i+1));
i++;
}
return s;
@@ -1840,12 +1870,17 @@ namespace Microsoft.Dafny {
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
Bpl.Expr seq = TrExpr(e.Seq);
- Bpl.Type elType = translator.TrType(((SeqType!)e.Seq.Type).Arg);
+ Type elmtType = ((SeqType!)e.Seq.Type).Arg;
+ Bpl.Type elType = translator.TrType(elmtType);
Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0);
Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1);
if (e.SelectOne) {
assert e1 == null;
- return translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, elType, seq, e0);
+ Bpl.Expr x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);
+ if (!ModeledAsBoxType(elmtType)) {
+ x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
+ }
+ return x;
} else {
if (e1 != null) {
seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqTake, elType, seq, e1);
@@ -1879,24 +1914,25 @@ namespace Microsoft.Dafny {
FreshExpr e = (FreshExpr)expr;
Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr);
if (e.E.Type is SetType) {
- // generate: (forall $o: ref :: $o != null && X[$o] ==> !old($Heap)[$o,alloc])
+ // generate: (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc])
// TODO: trigger?
Bpl.Variable oVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$o", predef.RefType));
Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar);
Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);
- Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, null);
+ Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg);
Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, o, oldHeap));
Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh);
return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), body);
} else if (e.E.Type is SeqType) {
- // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Seq#Index(X,$i) != null ==> !old($Heap)[Seq#Index(X,$i),alloc])
+ // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) && Unbox(Seq#Index(X,$i)) != null ==> !old($Heap)[Seq#Index(X,$i),alloc])
// TODO: trigger?
Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);
Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), null, false);
Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);
Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, XsubI, oldHeap));
- Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, XsubI), oIsFresh);
+ Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null);
+ Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh);
return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body);
} else {
// generate: x == null || !old($Heap)[x]
@@ -1921,9 +1957,9 @@ namespace Microsoft.Dafny {
BinaryExpr e = (BinaryExpr)expr;
Bpl.Expr e0 = TrExpr(e.E0);
if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) {
- return TrInSet(expr.tok, e0, e.E1, e.E0.Type); // let TrInSet translate e.E1
+ return TrInSet(expr.tok, e0, e.E1, (!)e.E0.Type); // let TrInSet translate e.E1
} else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) {
- Bpl.Expr arg = TrInSet(expr.tok, e0, e.E1, e.E0.Type); // let TrInSet translate e.E1
+ Bpl.Expr arg = TrInSet(expr.tok, e0, e.E1, (!)e.E0.Type); // let TrInSet translate e.E1
return Bpl.Expr.Not(arg);
}
Bpl.Expr e1 = TrExpr(e.E1);
@@ -2003,9 +2039,11 @@ namespace Microsoft.Dafny {
case BinaryExpr.ResolvedOpcode.Concat:
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqAppend, translator.TrType(((SeqType!)expr.Type).Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.InSeq:
- return translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1, e0);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1,
+ BoxIfNecessary(expr.tok, e0, (!)e.E0.Type));
case BinaryExpr.ResolvedOpcode.NotInSeq:
- Bpl.Expr arg = translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1, e0);
+ Bpl.Expr arg = translator.FunctionCall(expr.tok, BuiltinFunction.SeqContains, null, e1,
+ BoxIfNecessary(expr.tok, e0, (!)e.E0.Type));
return Bpl.Expr.Not(arg);
default:
@@ -2075,7 +2113,15 @@ namespace Microsoft.Dafny {
}
public Bpl.Expr! CondApplyBox(Token! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
- if (!ModeledAsRef(fromType) && ModeledAsRef(toType)) {
+ if (!ModeledAsBoxType(fromType) && ModeledAsBoxType(toType)) {
+ return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);
+ } else {
+ return e;
+ }
+ }
+
+ public Bpl.Expr! BoxIfNecessary(Token! tok, Bpl.Expr! e, Type! fromType) {
+ if (!ModeledAsBoxType(fromType)) {
return translator.FunctionCall(tok, BuiltinFunction.Box, null, e);
} else {
return e;
@@ -2083,15 +2129,15 @@ namespace Microsoft.Dafny {
}
public Bpl.Expr! CondApplyUnbox(Token! tok, Bpl.Expr! e, Type! fromType, Type! toType) {
- if (ModeledAsRef(fromType) && !ModeledAsRef(toType)) {
- return translator.FunctionSpecial(tok, BuiltinFunction.Unbox, translator.TrType(toType), e);
+ if (ModeledAsBoxType(fromType) && !ModeledAsBoxType(toType)) {
+ return translator.FunctionCall(tok, BuiltinFunction.Unbox, translator.TrType(toType), e);
} else {
return e;
}
}
- public static bool ModeledAsRef(Type! t) {
- return !(t is BoolType || t is IntType || t is CollectionType);
+ public static bool ModeledAsBoxType(Type! t) {
+ return t.IsTypeParameter;
}
public Bpl.IdentifierExpr! TrVar(Token! tok, IVariable! var) {
@@ -2099,11 +2145,10 @@ namespace Microsoft.Dafny {
}
/// <summary>
- /// Translate like s[elmt], but try to avoid as many set functions as possible in the
+ /// Translate like s[Box(elmt)], but try to avoid as many set functions as possible in the
/// translation, because such functions can mess up triggering.
- /// If elmtType is non-null, boxing according to elmtType is applied as appropriate.
/// </summary>
- public Bpl.Expr! TrInSet(Token! tok, Bpl.Expr! elmt, Expression! s, Type elmtType) {
+ public Bpl.Expr! TrInSet(Token! tok, Bpl.Expr! elmt, Expression! s, Type! elmtType) {
if (s is BinaryExpr) {
BinaryExpr bin = (BinaryExpr)s;
switch (bin.ResolvedOp) {
@@ -2133,7 +2178,7 @@ namespace Microsoft.Dafny {
return disjunction;
}
}
- return Bpl.Expr.SelectTok(tok, TrExpr(s), elmt);
+ return Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType));
}
Bpl.QKeyValue TrAttributes(Attributes attrs) {
@@ -2221,16 +2266,17 @@ namespace Microsoft.Dafny {
// This is done below
} else if (type is SetType) {
- // (forall tp: ref :: e[tp] ==> tp == null || $Heap[tp, alloc])
- bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$tp", predef.RefType));
+ // (forall tp: BoxType :: e[tp] ==> Unbox(tp) == null || $Heap[Unbox(tp), alloc])
+ bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$tp", predef.BoxType));
Bpl.Expr tp = new Bpl.IdentifierExpr(tok, bv);
ante = Bpl.Expr.SelectTok(tok, e, tp); // note, this means the set-inclusion does not undergo the set-inclusion expansion optimization done by TrInSet
- e = tp;
+ e = translator.FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, tp);
} else if (type is SeqType) {
- // (forall i: int :: Seq#Index(e,i) == null || $Heap[Seq#Index(e,i), alloc])
+ // (forall i: int :: Unbox(Seq#Index(e,i)) == null || $Heap[Unbox(Seq#Index(e,i)), alloc])
bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
- e = translator.FunctionCall(tok, BuiltinFunction.SeqIndex, predef.RefType, e, new Bpl.IdentifierExpr(tok, bv));
+ e = translator.FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, e, new Bpl.IdentifierExpr(tok, bv));
+ e = translator.FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, e);
} else {
return null;
@@ -2287,35 +2333,33 @@ namespace Microsoft.Dafny {
CevProgramLocation,
}
+ // The "typeInstantiation" argument is passed in to help construct the result type of the function.
Bpl.NAryExpr! FunctionCall(Token! tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[]! args)
requires predef != null;
{
switch (f) {
- case BuiltinFunction.SetEmpty:
+ case BuiltinFunction.SetEmpty: {
assert args.Length == 0;
assert typeInstantiation != null;
- return FunctionCall(tok, "Set#Empty",
- new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(typeInstantiation), Bpl.Type.Bool), args);
+ Bpl.Type resultType = predef.SetType(tok, typeInstantiation);
+ return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Set#Empty", resultType, args), resultType);
+ }
case BuiltinFunction.SetUnionOne:
assert args.Length == 2;
assert typeInstantiation != null;
- return FunctionCall(tok, "Set#UnionOne",
- new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(typeInstantiation), Bpl.Type.Bool), args);
+ return FunctionCall(tok, "Set#UnionOne", predef.SetType(tok, typeInstantiation), args);
case BuiltinFunction.SetUnion:
assert args.Length == 2;
assert typeInstantiation != null;
- return FunctionCall(tok, "Set#Union",
- new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(typeInstantiation), Bpl.Type.Bool), args);
+ return FunctionCall(tok, "Set#Union", predef.SetType(tok, typeInstantiation), args);
case BuiltinFunction.SetIntersection:
assert args.Length == 2;
assert typeInstantiation != null;
- return FunctionCall(tok, "Set#Intersection",
- new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(typeInstantiation), Bpl.Type.Bool), args);
+ return FunctionCall(tok, "Set#Intersection", predef.SetType(tok, typeInstantiation), args);
case BuiltinFunction.SetDifference:
assert args.Length == 2;
assert typeInstantiation != null;
- return FunctionCall(tok, "Set#Difference",
- new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(typeInstantiation), Bpl.Type.Bool), args);
+ return FunctionCall(tok, "Set#Difference", predef.SetType(tok, typeInstantiation), args);
case BuiltinFunction.SetEqual:
assert args.Length == 2;
assert typeInstantiation == null;
@@ -2333,11 +2377,12 @@ namespace Microsoft.Dafny {
assert args.Length == 1;
assert typeInstantiation == null;
return FunctionCall(tok, "Seq#Length", Bpl.Type.Int, args);
- case BuiltinFunction.SeqEmpty:
+ case BuiltinFunction.SeqEmpty: {
assert args.Length == 0;
assert typeInstantiation != null;
- return FunctionCall(tok, "Seq#Empty",
- new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(typeInstantiation), Bpl.Type.Bool), args);
+ Bpl.Type resultType = predef.SeqType(tok, typeInstantiation);
+ return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Seq#Empty", resultType, args), resultType);
+ }
case BuiltinFunction.SeqBuild:
assert args.Length == 4;
assert typeInstantiation != null;
@@ -2374,9 +2419,11 @@ namespace Microsoft.Dafny {
case BuiltinFunction.Box:
assert args.Length == 1;
assert typeInstantiation == null;
- return FunctionCall(tok, "$Box", predef.RefType, args);
+ return FunctionCall(tok, "$Box", predef.BoxType, args);
case BuiltinFunction.Unbox:
- assert false; // Unbox should be handled by a call to FunctionSpecial
+ assert args.Length == 1;
+ assert typeInstantiation != null;
+ return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", typeInstantiation, args), typeInstantiation);
case BuiltinFunction.IsGoodHeap:
assert args.Length == 1;
@@ -2430,17 +2477,6 @@ namespace Microsoft.Dafny {
}
}
- Bpl.NAryExpr! FunctionSpecial(Token! tok, BuiltinFunction f, Bpl.Type! resultType, params Bpl.Expr[]! args)
- {
- switch (f) {
- case BuiltinFunction.Unbox:
- assert args.Length == 1;
- return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", resultType, args), resultType);
- default:
- assert false; // unexpected enum value
- }
- }
-
Bpl.NAryExpr! FunctionCall(Token! tok, string! function, Bpl.Type! returnType, params Bpl.Expr[]! args)
{
return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), new Bpl.ExprSeq(args));
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 4f717f48..4f44612d 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -13,22 +13,22 @@
//would be nice if we could mark pperm as a ghost variable
class Queue<T> {
- var contents: seq<int>;
+ var contents: seq<T>;
method Init();
modifies this;
ensures |contents| == 0;
- method Enqueue(x: int);
+ method Enqueue(x: T);
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: int);
+ method Dequeue() returns (x: T);
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
- function Head(): int
+ function Head(): T
requires 0 < |contents|;
reads this;
{ contents[0] }
- function Get(i: int): int
+ function Get(i: int): T
requires 0 <= i && i < |contents|;
reads this;
{ contents[i] }
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index 5a9d46c8..e3a99884 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -43,16 +43,10 @@ class Map<Key,Value> {
requires Valid();
modifies this;
ensures Valid();
- // no key is lost:
- ensures (forall k :: k in old(keys) ==> k in keys);
- // at most one key is introduced:
- ensures (forall k :: k in keys ==> k in old(keys) || k == key);
- // the given key has the given value:
- ensures (exists i :: 0 <= i && i < |keys| &&
- keys[i] == key && values[i] == val);
- // other values don't change:
- ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
- values[i] == old(values)[i]);
+ ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>
+ keys[i] == key && values[i] == val &&
+ (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
+ ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
{
call j := FindIndex(key);
if (j == -1) {
@@ -60,7 +54,6 @@ class Map<Key,Value> {
values := values + [val];
assert values[|keys|-1] == val; // lemma
} else {
- keys := keys[..j] + [key] + keys[j+1..];
values := values[..j] + [val] + values[j+1..];
assert values[j] == val; //lemma
}
diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index 48306e9b..d320f9e9 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -1,7 +1,7 @@
-class Collection {
+class Collection<T> {
var footprint:set<object>;
- var elements:seq<int>;
+ var elements:seq<T>;
function Valid():bool
reads this, footprint;
@@ -24,7 +24,7 @@ class Collection {
footprint := {this};
}
- method GetItem(i:int ) returns (x:int)
+ method GetItem(i:int ) returns (x:T)
requires Valid();
requires 0<=i && i<|elements|;
ensures elements[i] ==x;
@@ -32,7 +32,7 @@ class Collection {
x:=elements[i];
}
- method Add(x:int )
+ method Add(x:T )
requires Valid();
modifies footprint;
ensures Valid() && fresh(footprint - old(footprint));
@@ -41,21 +41,21 @@ class Collection {
elements:= elements + [x];
}
- method GetIterator() returns (iter:Iterator)
+ method GetIterator() returns (iter:Iterator<T>)
requires Valid();
ensures iter != null && iter.Valid();
ensures fresh(iter.footprint) && iter.pos == -1;
ensures iter.c == this;
{
- iter:= new Iterator;
+ iter:= new Iterator<T>;
call iter.Init(this);
}
}
-class Iterator {
+class Iterator<T> {
- var c:Collection;
+ var c:Collection<T>;
var pos:int;
var footprint:set<object>;
@@ -66,7 +66,7 @@ class Iterator {
this in footprint && c!= null && -1<= pos && null !in footprint
}
- method Init(coll:Collection)
+ method Init(coll:Collection<T>)
requires coll != null;
modifies this;
ensures Valid() && fresh(footprint -{this}) && pos ==-1;
@@ -94,7 +94,7 @@ class Iterator {
0<= pos && pos < |c.elements|
}
- method GetCurrent() returns (x:int)
+ method GetCurrent() returns (x:T)
requires Valid() && HasCurrent();
ensures c.elements[pos] == x;
{
@@ -108,7 +108,7 @@ class Client
method Main()
{
- var c:= new Collection;
+ var c:= new Collection<int>;
call c.Init();
call c.Add(33);
call c.Add(45);
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index f7d51058..ddad7599 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -7,22 +7,22 @@
class Queue<T> {
- var contents: seq<int>;
+ var contents: seq<T>;
method Init();
modifies this;
ensures |contents| == 0;
- method Enqueue(x: int);
+ method Enqueue(x: T);
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: int);
+ method Dequeue() returns (x: T);
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
- function Head(): int
+ function Head(): T
requires 0 < |contents|;
reads this;
{ contents[0] }
- function Get(i: int): int
+ function Get(i: int): T
requires 0 <= i && i < |contents|;
reads this;
{ contents[i] }
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 51172419..c3374605 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -5,22 +5,22 @@
// the following words (until we read null) form the terms definition. Then the stream provides the next term etc.
class Queue<T> {
- var contents: seq<Word>;
+ var contents: seq<T>;
method Init();
modifies this;
ensures |contents| == 0;
- method Enqueue(x: Word);
+ method Enqueue(x: T);
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: Word);
+ method Dequeue() returns (x: T);
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
- function Head(): Word
+ function Head(): T
requires 0 < |contents|;
reads this;
{ contents[0] }
- function Get(i: int): Word
+ function Get(i: int): T
requires 0 <= i && i < |contents|;
reads this;
{ contents[i] }
@@ -56,18 +56,20 @@ class Glossary {
invariant glossary.Valid();
invariant glossary !in rs.footprint;
invariant null !in glossary.keys;
- //to do add invariant invariant (forall d:: d in glossary.values ==>!(null in d)); ***
+ invariant (forall d :: d in glossary.values ==> null !in d);
invariant q !in rs.footprint;
- // ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)
+ invariant q.contents == glossary.keys;
// we leave out the decreases clause - unbounded stream
{
call term,definition := readDefinition(rs);
- if (term == null)
- {
+ if (term == null) {
break;
- }
- call glossary.Add(term,definition);
- call q.Enqueue(term);
+ }
+ call present, d := glossary.Find(term);
+ if (!present) {
+ call glossary.Add(term,definition);
+ call q.Enqueue(term);
+ }
}
call rs.Close();
@@ -79,12 +81,14 @@ class Glossary {
invariant wr.Valid() && fresh(wr.footprint);
invariant glossary.Valid();
invariant glossary !in wr.footprint && null !in glossary.keys;
+ invariant (forall d :: d in glossary.values ==> null !in d);
invariant q !in wr.footprint;
+ invariant (forall k :: k in q.contents ==> k in glossary.keys);
decreases |q.contents|;
{
- call term:= q.Dequeue();
- call present,definition:= glossary.Find(term);
- assume present; // to change this into an assert we need the loop invariant ** above that we commented out
+ call term := q.Dequeue();
+ call present,definition := glossary.Find(term);
+ assert present;
// write term with a html anchor
call wr.PutWordInsideTag(term, term);
@@ -95,12 +99,13 @@ class Glossary {
invariant wr.Valid() && fresh(wr.footprint);
invariant glossary.Valid();
invariant glossary !in wr.footprint && null !in glossary.keys;
+ invariant (forall d :: d in glossary.values ==> null !in d);
invariant q !in wr.footprint;
invariant qcon == q.contents;
+ invariant (forall k :: k in q.contents ==> k in glossary.keys);
decreases |definition| -i;
{
var w := definition[i];
- assume w != null; // to convert this into an assert we need invariant *** above
call present, d := glossary.Find(w);
if (present)
{
@@ -130,6 +135,7 @@ class Glossary {
while (true)
invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));
invariant null !in definition;
+ // we leave out the decreases clause - unbounded stream
{
call w := rs.GetWord();
if (w == null)
@@ -283,16 +289,10 @@ class Map<Key,Value> {
requires Valid();
modifies this;
ensures Valid();
- // no key is lost:
- ensures (forall k :: k in old(keys) ==> k in keys);
- // at most one key is introduced:
- ensures (forall k :: k in keys ==> k in old(keys) || k == key);
- // the given key has the given value:
- ensures (exists i :: 0 <= i && i < |keys| &&
- keys[i] == key && values[i] == val);
- // other values don't change:
- ensures (forall i :: 0 <= i && i < |keys| && keys[i] != key ==>
- values[i] == old(values)[i]);
+ ensures (forall i :: 0 <= i && i < |keys| && old(keys)[i] == key ==>
+ keys[i] == key && values[i] == val &&
+ (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j]));
+ ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val];
{
call j := FindIndex(key);
if (j == -1) {
@@ -300,7 +300,6 @@ class Map<Key,Value> {
values := values + [val];
assert values[|keys|-1] == val; // lemma
} else {
- keys := keys[..j] + [key] + keys[j+1..];
values := values[..j] + [val] + values[j+1..];
assert values[j] == val; //lemma
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 64c43c87..78982f01 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -96,5 +96,11 @@ Execution trace:
Dafny program verifier finished with 5 verified, 3 errors
-------------------- TypeParameters.dfy --------------------
+TypeParameters.dfy(41,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ (0,0): anon0
+TypeParameters.dfy(63,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 7 verified, 2 errors
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 3f57f369..794f2f95 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -19,3 +19,47 @@ class C<U> {
function G<Y>(): Y;
}
+
+class SetTest {
+ method Add<T>(s: set<T>, x: T) returns (t: set<T>)
+ ensures t == s + {x};
+ {
+ t := s + {x};
+ }
+
+ method Good()
+ {
+ var s := {2, 5, 3};
+ call t := Add(s, 7);
+ assert {5,7,2,3} == t;
+ }
+
+ method Bad()
+ {
+ var s := {2, 50, 3};
+ call t := Add(s, 7);
+ assert {5,7,2,3} == t; // error
+ }
+}
+
+class SequenceTest {
+ method Add<T>(s: seq<T>, x: T) returns (t: seq<T>)
+ ensures t == s + [x];
+ {
+ t := s + [x];
+ }
+
+ method Good()
+ {
+ var s := [2, 5, 3];
+ call t := Add(s, 7);
+ assert [2,5,3,7] == t;
+ }
+
+ method Bad()
+ {
+ var s := [2, 5, 3];
+ call t := Add(s, 7);
+ assert [2,5,7,3] == t || [2,5,3] == t;
+ }
+}
diff --git a/Test/inline/Answer b/Test/inline/Answer
index 43ec6740..8f2c34e4 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -961,12 +961,12 @@ function {:inline true} foo(x: int) returns (bool)
function {:inline false} foo2(x: int) returns (bool);
// autogenerated definition axiom
-axiom (forall x: int :: {:inline false} { foo2(x):bool } foo2(x):bool == (x > 0));
+axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));
function foo3(x: int) returns (bool);
// autogenerated definition axiom
-axiom (forall x: int :: { foo3(x):bool } foo3(x):bool == (x > 0));
+axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));
Boogie program verifier finished with 0 verified, 0 errors
fundef2.bpl(6,3): Error BP5001: This assertion might not hold.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 11:07:54 +0000