diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 8 | ||||
| -rw-r--r-- | Dafny/Dafny.atg | 14 | ||||
| -rw-r--r-- | Dafny/DafnyAst.ssc | 14 | ||||
| -rw-r--r-- | Dafny/Parser.ssc | 26 | ||||
| -rw-r--r-- | Dafny/Printer.ssc | 16 | ||||
| -rw-r--r-- | Dafny/Resolver.ssc | 28 | ||||
| -rw-r--r-- | Dafny/Translator.ssc | 40 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 2 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 4 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b8.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/ListContents.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/Simple.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 19 |
14 files changed, 162 insertions, 24 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 9615586a..4eee233b 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -84,6 +84,14 @@ axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Bui (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&
(i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));
+function Seq#Update<T>(Seq T, int, T) returns (Seq T);
+axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) }
+ 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s));
+axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) }
+ 0 <= n && n < Seq#Length(s) ==>
+ (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) &&
+ (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n)));
+
function Seq#Contains<T>(Seq T, T) returns (bool);
axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
Seq#Contains(s,x) <==>
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 022dc912..5da2b44b 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -847,14 +847,20 @@ SelectOrCallSuffix<ref Expression! e> [ ".." (. anyDots = true; .)
[ Expression<out ee> (. e1 = ee; .)
]
+ | ":="
+ Expression<out ee> (. e1 = ee; .)
]
| ".." Expression<out ee> (. anyDots = true; e1 = ee; .)
- ) (. if (!anyDots) {
- assert e1 == null;
- e = new SeqSelectExpr(x, true, e, e0, null);
- } else {
+ ) (. assert !anyDots ==> e0 != null;
+ if (anyDots) {
assert e0 != null || e1 != null;
e = new SeqSelectExpr(x, false, e, e0, e1);
+ } else if (e1 == null) {
+ assert e0 != null;
+ e = new SeqSelectExpr(x, true, e, e0, null);
+ } else {
+ assert e0 != null;
+ e = new SeqUpdateExpr(x, e, e0, e1);
}
.)
"]"
diff --git a/Dafny/DafnyAst.ssc b/Dafny/DafnyAst.ssc index 4b97edbd..f50ded86 100644 --- a/Dafny/DafnyAst.ssc +++ b/Dafny/DafnyAst.ssc @@ -871,6 +871,20 @@ namespace Microsoft.Dafny }
}
+ public class SeqUpdateExpr : Expression {
+ public readonly Expression! Seq;
+ public readonly Expression! Index;
+ public readonly Expression! Value;
+
+ public SeqUpdateExpr(Token! tok, Expression! seq, Expression! index, Expression! val)
+ {
+ Seq = seq;
+ Index = index;
+ Value = val;
+ base(tok);
+ }
+ }
+
public class FunctionCallExpr : Expression {
public readonly string! Name;
[Peer] public readonly Expression! Receiver;
diff --git a/Dafny/Parser.ssc b/Dafny/Parser.ssc index 0fd3e612..6b12d796 100644 --- a/Dafny/Parser.ssc +++ b/Dafny/Parser.ssc @@ -1312,10 +1312,16 @@ public static int Parse (List<ClassDecl!>! classes) { if (StartOf(5)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 78) {
- Get();
- anyDots = true;
- if (StartOf(5)) {
+ if (t.kind == 35 || t.kind == 78) {
+ if (t.kind == 78) {
+ Get();
+ anyDots = true;
+ if (StartOf(5)) {
+ Expression(out ee);
+ e1 = ee;
+ }
+ } else {
+ Get();
Expression(out ee);
e1 = ee;
}
@@ -1325,12 +1331,16 @@ public static int Parse (List<ClassDecl!>! classes) { Expression(out ee);
anyDots = true; e1 = ee;
} else Error(118);
- if (!anyDots) {
- assert e1 == null;
- e = new SeqSelectExpr(x, true, e, e0, null);
- } else {
+ assert !anyDots ==> e0 != null;
+ if (anyDots) {
assert e0 != null || e1 != null;
e = new SeqSelectExpr(x, false, e, e0, e1);
+ } else if (e1 == null) {
+ assert e0 != null;
+ e = new SeqSelectExpr(x, true, e, e0, null);
+ } else {
+ assert e0 != null;
+ e = new SeqUpdateExpr(x, e, e0, e1);
}
Expect(76);
diff --git a/Dafny/Printer.ssc b/Dafny/Printer.ssc index ba44f9a9..68b9e132 100644 --- a/Dafny/Printer.ssc +++ b/Dafny/Printer.ssc @@ -495,6 +495,22 @@ namespace Microsoft.Dafny { wr.Write("]");
if (parensNeeded) { wr.Write(")"); }
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ // determine if parens are needed
+ int opBindingStrength = 0x70;
+ bool parensNeeded = opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
+
+ if (parensNeeded) { wr.Write("("); }
+ PrintExpr(e.Seq, 00, false, indent); // BOGUS: fix me
+ wr.Write("[");
+ PrintExpression(e.Index);
+ wr.Write(" := ");
+ PrintExpression(e.Value);
+ wr.Write("]");
+ if (parensNeeded) { wr.Write(")"); }
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
// determine if parens are needed
diff --git a/Dafny/Resolver.ssc b/Dafny/Resolver.ssc index 47727562..7f1342f1 100644 --- a/Dafny/Resolver.ssc +++ b/Dafny/Resolver.ssc @@ -1020,14 +1020,14 @@ namespace Microsoft.Dafny { ResolveExpression(e.E0, twoState);
assert e.E0.Type != null; // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E0.Type, Type.Int)) {
- Error(e.E0, "sequence selections requires integer indices (got {0})", e.E0.Type);
+ Error(e.E0, "sequence selection requires integer indices (got {0})", e.E0.Type);
}
}
if (e.E1 != null) {
ResolveExpression(e.E1, twoState);
assert e.E1.Type != null; // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E1.Type, Type.Int)) {
- Error(e.E1, "sequence selections requires integer indices (got {0})", e.E1.Type);
+ Error(e.E1, "sequence selection requires integer indices (got {0})", e.E1.Type);
}
}
if (!seqErr) {
@@ -1038,6 +1038,30 @@ namespace Microsoft.Dafny { }
}
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ bool seqErr = false;
+ ResolveExpression(e.Seq, twoState);
+ assert e.Seq.Type != null; // follows from postcondition of ResolveExpression
+ Type elementType = new InferredTypeProxy();
+ if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) {
+ Error(expr, "sequence update requires a sequence (got {0})", e.Seq.Type);
+ seqErr = true;
+ }
+ ResolveExpression(e.Index, twoState);
+ assert e.Index.Type != null; // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Index.Type, Type.Int)) {
+ Error(e.Index, "sequence update requires integer index (got {0})", e.Index.Type);
+ }
+ ResolveExpression(e.Value, twoState);
+ assert e.Value.Type != null; // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Value.Type, elementType)) {
+ Error(e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);
+ }
+ if (!seqErr) {
+ expr.Type = e.Seq.Type;
+ }
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
ResolveExpression(e.Receiver, twoState);
diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc index 33002065..ae8f03a5 100644 --- a/Dafny/Translator.ssc +++ b/Dafny/Translator.ssc @@ -695,6 +695,15 @@ namespace Microsoft.Dafny { total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true));
}
return total;
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ Bpl.Expr total = IsTotal(e.Seq, etran);
+ Bpl.Expr seq = etran.TrExpr(e.Seq);
+ Bpl.Expr index = etran.TrExpr(e.Index);
+ total = BplAnd(total, IsTotal(e.Index, etran));
+ total = BplAnd(total, InSeqRange(expr.tok, index, seq, null, false));
+ total = BplAnd(total, IsTotal(e.Value, etran));
+ return total;
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
Bpl.Expr r = IsTotal(e.Receiver, etran);
@@ -825,6 +834,14 @@ namespace Microsoft.Dafny { CheckWellformed(e.E1, func, Position.Neither, builder, etran);
builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true)));
}
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ CheckWellformed(e.Seq, func, Position.Neither, builder, etran);
+ Bpl.Expr seq = etran.TrExpr(e.Seq);
+ Bpl.Expr index = etran.TrExpr(e.Index);
+ CheckWellformed(e.Index, func, Position.Neither, builder, etran);
+ builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, index, seq, null, false)));
+ CheckWellformed(e.Value, func, Position.Neither, builder, etran);
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
CheckWellformed(e.Receiver, func, Position.Neither, builder, etran);
@@ -1891,6 +1908,15 @@ namespace Microsoft.Dafny { return seq;
}
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ Bpl.Expr seq = TrExpr(e.Seq);
+ Type elmtType = ((SeqType!)e.Seq.Type).Arg;
+ Bpl.Type elType = translator.TrType(elmtType);
+ Bpl.Expr index = TrExpr(e.Index);
+ Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
string nm = ((!)e.Function).FullName + (e is UseExpr ? "#use" : "");
@@ -2308,6 +2334,7 @@ namespace Microsoft.Dafny { SeqBuild,
SeqAppend,
SeqIndex,
+ SeqUpdate,
SeqContains,
SeqDrop,
SeqTake,
@@ -2395,6 +2422,10 @@ namespace Microsoft.Dafny { assert args.Length == 2;
assert typeInstantiation != null;
return FunctionCall(tok, "Seq#Index", typeInstantiation, args);
+ case BuiltinFunction.SeqUpdate:
+ assert args.Length == 3;
+ assert typeInstantiation != null;
+ return FunctionCall(tok, "Seq#Update", predef.SeqType(tok, typeInstantiation), args);
case BuiltinFunction.SeqContains:
assert args.Length == 2;
assert typeInstantiation == null;
@@ -2616,6 +2647,15 @@ namespace Microsoft.Dafny { newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);
}
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr sse = (SeqUpdateExpr)expr;
+ Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);
+ Expression index = Substitute(sse.Index, receiverReplacement, substMap);
+ Expression val = Substitute(sse.Value, receiverReplacement, substMap);
+ if (seq != sse.Seq || index != sse.Index || val != sse.Value) {
+ newExpr = new SeqUpdateExpr(sse.tok, seq, index, val);
+ }
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
Expression receiver = Substitute(e.Receiver, receiverReplacement, substMap);
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 4f44612d..ed121ba0 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -100,7 +100,7 @@ class Benchmark3 { call r.Enqueue(m);
pperm:= pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] +[pperm[k]];
}
- assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //needed to trigger axiom
+ assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //lemma needed to trigger axiom
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index e3a99884..3fa80b4c 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -52,10 +52,8 @@ class Map<Key,Value> { if (j == -1) {
keys := keys + [key];
values := values + [val];
- assert values[|keys|-1] == val; // lemma
} else {
- values := values[..j] + [val] + values[j+1..];
- assert values[j] == val; //lemma
+ values := values[j := val];
}
}
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index c3374605..bc26ee85 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -298,10 +298,8 @@ class Map<Key,Value> { if (j == -1) {
keys := keys + [key];
values := values + [val];
- assert values[|keys|-1] == val; // lemma
} else {
- values := values[..j] + [val] + values[j+1..];
- assert values[j] == val; //lemma
+ values := values[j := val];
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 78982f01..e7f7c4d6 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -27,6 +27,7 @@ class MyClass<T, U> { var to: MyClass<T,U>;
call to, u, v := M(true, lotsaObjects)
call to, u, v := to.M(true, lotsaObjects)
+ assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
}
}
@@ -38,8 +39,11 @@ Dafny program verifier finished with 0 verified, 0 errors Boogie program verifier finished with 8 verified, 0 errors
-------------------- SmallTests.dfy --------------------
+SmallTests.dfy(29,7): Error: RHS expression must be well defined
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 3 verified, 0 errors
+Dafny program verifier finished with 4 verified, 1 error
-------------------- Queue.dfy --------------------
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy index 01d8b63b..759c6afd 100644 --- a/Test/dafny0/ListContents.dfy +++ b/Test/dafny0/ListContents.dfy @@ -77,10 +77,10 @@ class Node<T> { (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
{
var nx := current.next;
- assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]);
+ assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma
// ..., reverse, current, nx, ...
- assert current.data == current.list[0];
+ assert current.data == current.list[0]; // lemma
current.next := reverse;
current.footprint := {current} + reverse.footprint;
current.list := [current.data] + reverse.list;
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index 9f89543c..5f0bee87 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -24,6 +24,7 @@ class MyClass<T,U> { var to: MyClass<T,U>;
call to, u, v := this.M(true, lotsaObjects);
call to, u, v := to.M(true, lotsaObjects);
+ assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10];
}
}
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index a2cfc741..01c9f1ea 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -23,4 +23,23 @@ class Node { tmp := new Node;
assert tmp != this; // was once a bug in the Dafny checker
}
+
+ method SequenceUpdateOutOfBounds(s: seq<set<int>>, j: int) returns (t: seq<set<int>>)
+ {
+ t := s[j := {}]; // error: j is possibly out of bounds
+ }
+
+ method Sequence(s: seq<bool>, j: int, b: bool, c: bool) returns (t: seq<bool>)
+ requires 10 <= |s|;
+ requires 8 <= j && j < |s|;
+ ensures |t| == |s|;
+ ensures t[8] == s[8] || t[9] == s[9];
+ ensures t[j] == b;
+ {
+ if (c) {
+ t := s[j := b];
+ } else {
+ t := s[..j] + [b] + s[j+1..];
+ }
+ }
}
|