From 343f29bee9cad726c2de33d4ef6cdb49caa965d2 Mon Sep 17 00:00:00 2001 From: Unknown Date: Tue, 5 Apr 2011 17:03:28 -0700 Subject: Dafny: Allow field selections and array-element selection as LHSs of assignments where RHS is not just an expression --- Test/VSComp2010/Problem5-DoubleEndedQueue.dfy | 12 ++---- Test/VSI-Benchmarks/b8.dfy | 2 +- Test/dafny0/AdvancedLHS.dfy | 59 +++++++++++++++++++++++++++ Test/dafny0/Answer | 12 +++++- Test/dafny0/Array.dfy | 4 +- Test/dafny0/TypeTests.dfy | 9 ++++ Test/dafny0/runtest.bat | 2 +- Test/dafny1/ExtensibleArray.dfy | 9 ++-- Test/dafny1/PriorityQueue.dfy | 6 +-- Test/dafny1/UnboundedStack.dfy | 3 +- Test/vacid0/LazyInitArray.dfy | 6 +-- 11 files changed, 97 insertions(+), 27 deletions(-) create mode 100644 Test/dafny0/AdvancedLHS.dfy (limited to 'Test') diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy index cf109c1a..df8cb1b7 100644 --- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy +++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy @@ -30,10 +30,8 @@ class AmortizedQueue { modifies this; ensures Valid() && List == []; { - var tmp := new LinkedList.Init(); - front := tmp; - tmp := new LinkedList.Init(); - rear := tmp; + front := new LinkedList.Init(); + rear := new LinkedList.Init(); Repr := {this}; Repr := Repr + front.Repr + rear.Repr; List := []; @@ -52,8 +50,7 @@ class AmortizedQueue { call ff := f.Concat(rr); front := ff; - var tmp := new LinkedList.Init(); - rear := tmp; + rear := new LinkedList.Init(); } Repr := {this}; Repr := Repr + front.Repr + rear.Repr; @@ -79,8 +76,7 @@ class AmortizedQueue { ensures r != null && r.Valid() && r.List == List + [item]; { call rr := rear.Cons(item); - var tmp := new AmortizedQueue.InitFromPieces(front, rr); - r := tmp; + r := new AmortizedQueue.InitFromPieces(front, rr); } } diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 02c1a63a..3438d6e0 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -48,7 +48,7 @@ class Glossary { var rs:= new ReaderStream; call rs.Open(); var glossary := new Map>.Init(); - var q:= new Queue.Init(); + var q := new Queue.Init(); while (true) invariant rs.Valid() && fresh(rs.footprint); diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy new file mode 100644 index 00000000..b73af758 --- /dev/null +++ b/Test/dafny0/AdvancedLHS.dfy @@ -0,0 +1,59 @@ +class C { + var x: C; + + method M(S: set, a: array, b: array2) + requires S != {}; + modifies this, a, b; + { + x := new C; + x := new C.Init(); + havoc x; + x := choose(S); + + // test evaluation order + var c := x; + x := null; + x := new C.InitOther(x); // since the parameter is evaluated before the LHS is set, the precondition is met + assert x != c; + + // test evaluation order and modification + if (*) { + var k := this.x; + var kx := this.x.x; + this.x.x := new C.InitAndMutate(this); + assert this.x == null; + assert this.x != k; + assert k.x != kx; // because it was set to a new object + assert fresh(k.x); + } else { + var k := this.x; + var kx := this.x.x; + this.x.x := new C.InitAndMutate(this); + var t := this.x.x; // error: null dereference (because InitAndMutate set this.x to null) + } + + if (a != null && 10 <= a.Length) { + a[2] := new C; + a[4..8] := null; + havoc a[3]; + } + if (b != null && 10 <= b.Length0 && 20 <= b.Length1) { + b[2,14] := new C; + havoc b[3,11]; + } + } + + method Init() { } + method InitOther(c: C) + requires c == null; + { + var d := new int[if c == null then 10 else -3]; // run-time error if c were non-null, but it ain't + } + method InitAndMutate(c: C) + requires c != null; + modifies c; + ensures c.x == null; + { + c.x := null; + } +} diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index f57c6ead..eb85403e 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -81,7 +81,9 @@ TypeTests.dfy(69,8): Error: Duplicate local-variable name: x TypeTests.dfy(72,6): Error: Duplicate local-variable name: y TypeTests.dfy(79,17): Error: member F in class C does not refer to a method TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments -16 resolution/type errors detected in TypeTests.dfy +TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable +TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable +18 resolution/type errors detected in TypeTests.dfy -------------------- SmallTests.dfy -------------------- SmallTests.dfy(30,11): Error: index out of range @@ -418,6 +420,14 @@ NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be NonGhostQuantifiers.dfy(120,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) 8 resolution/type errors detected in NonGhostQuantifiers.dfy +-------------------- AdvancedLHS.dfy -------------------- +AdvancedLHS.dfy(32,23): Error: target object may be null +Execution trace: + (0,0): anon0 + (0,0): anon15_Else + +Dafny program verifier finished with 7 verified, 1 error + -------------------- 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/Array.dfy b/Test/dafny0/Array.dfy index 048ecd7a..60854f63 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -37,10 +37,10 @@ class A { method O() { var zz2 := new A[25]; assert zz2 != zz0; // holds because zz2 is newly allocated - /****** These would be good things to be able to verify, but the current encoding is not up to the task var o: object := zz0; assert this != o; // holds because zz0 has a different type - if (zz0 != null && zz1 != null && 2 <= |zz0| && |zz0| == |zz1|) { + /****** This would be a good thing to be able to verify, but the current encoding is not up to the task + if (zz0 != null && zz1 != null && 2 <= zz0.Length && zz0.Length == zz1.Length) { o := zz1[1]; assert zz0[1] == o ==> o == null; // holds because zz0 and zz1 have different element types } diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index cbab53bf..93c4aec4 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -80,3 +80,12 @@ method InitCalls() { var d := new C.M(8); // error: M has out parameters var e := new C.Caller(); } + +// --------------------- + +method ArrayRangeAssignments(a: array) + requires a != null && 10 <= a.Length; +{ + a[0..5] := new C; // this is not allowed + havoc a[1..4]; // this is not allowed +} diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 2c55a6b9..6a2f2cb5 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 NonGhostQuantifiers.dfy + Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.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/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index b790eea5..4ceca552 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -39,7 +39,7 @@ class ExtensibleArray { ensures Valid() && fresh(Repr - {this}); ensures Contents == []; { - var arr := new T[256]; elements := arr; + elements := new T[256]; more := null; length := 0; M := 0; @@ -90,15 +90,14 @@ class ExtensibleArray { elements[length - M] := t; } else { if (more == null) { - var mr := new ExtensibleArray>.Init(); - more := mr; - Repr := Repr + {mr} + mr.Repr; + more := new ExtensibleArray>.Init(); + Repr := Repr + {more} + more.Repr; } // "elements" is full, so move it into "more" and allocate a new array call more.Append(elements); Repr := Repr + more.Repr; M := M + 256; - var arr := new T[256]; elements := arr; + elements := new T[256]; Repr := Repr + {elements}; elements[0] := t; } diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy index 957eb7cb..db1c60fa 100644 --- a/Test/dafny1/PriorityQueue.dfy +++ b/Test/dafny1/PriorityQueue.dfy @@ -27,8 +27,7 @@ class PriorityQueue { ensures N == capacity; { N := capacity; - var arr := new int[N+1]; - a := arr; + a := new int[N+1]; n := 0; Repr := {this}; Repr := Repr + {a}; @@ -143,8 +142,7 @@ class PriorityQueue_Alternative { ensures N == capacity; { N := capacity; - var arr := new int[N+1]; - a := arr; + a := new int[N+1]; n := 0; Repr := {this}; Repr := Repr + {a}; diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy index 940e1a0a..dfc10327 100644 --- a/Test/dafny1/UnboundedStack.dfy +++ b/Test/dafny1/UnboundedStack.dfy @@ -31,8 +31,7 @@ class UnboundedStack { ensures IsUnboundedStack(); ensures content == [val] + old(content); { - var tmp := new Node.InitNode(val,top); - top := tmp; + top := new Node.InitNode(val,top); representation := representation + top.footprint; content := [val] + content; } diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy index fc4d687d..e56a8317 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -41,9 +41,9 @@ class LazyInitArray { ensures |Contents| == N && Zero == zero; ensures (forall x :: x in Contents ==> x == zero); { - var aa := new T[N+1]; a := aa; - var ii := new int[N]; b := ii; - ii := new int[N]; c := ii; + a := new T[N+1]; + b := new int[N]; + c := new int[N]; n := 0; // initialize ghost variable Contents to a sequence of length N containing only zero's, -- cgit v1.2.3