diff options
| author |  leino <unknown> | 2014-10-30 15:12:31 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-30 15:12:31 -0700 |
| commit | 9f41b35b514eba87a037cbada83f0c294eafb936 (patch) | |
| tree | 06b875a433e0ca8ca80dc41cc7ed34bbef5514b8 /Test/dafny0/LhsDuplicates.dfy | |
| parent | c612305e78f057b9d1e91a0d154989cb866a7906 (diff) | |
Allow assignment LHSs in a forall statement to be the same, so long as the they are assigned the same RHS value.
Don't include havoc assignments in LHS-duplicate checks.
Diffstat (limited to 'Test/dafny0/LhsDuplicates.dfy')
| -rw-r--r-- | Test/dafny0/LhsDuplicates.dfy | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/Test/dafny0/LhsDuplicates.dfy b/Test/dafny0/LhsDuplicates.dfy new file mode 100644 index 00000000..6a84c5a5 --- /dev/null +++ b/Test/dafny0/LhsDuplicates.dfy @@ -0,0 +1,70 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class MyClass<T> {
+ var f: T;
+}
+
+method M<T>()
+{
+ var a, b := new T[100], new T[100];
+ forall i | 0 <= i < 100 {
+ a[3] := *; // RHS is * -- this is okay
+ }
+ forall i | 0 <= i < 100 {
+ a[0] := b[0]; // RHSs are the same -- this is okay
+ }
+ forall i | 0 <= i < 100 {
+ a[0] := b[i]; // error: LHS's may be the same (while RHSs are different)
+ }
+}
+
+method N<T>(a: MyClass<T>, b: MyClass<T>)
+ requires a != null && b != null;
+ modifies a, b;
+{
+ var q := [a, b];
+ forall i | 0 <= i < 2 {
+ q[0].f := *; // RHS is * -- this is okay
+ }
+ forall i | 0 <= i < 2 {
+ q[0].f := q[0].f; // RHSs are the same -- this is okay
+ }
+ forall i | 0 <= i < 2 {
+ q[0].f := q[i].f; // error: LHS's may be the same (while RHSs are different)
+ }
+}
+
+method P<T>(t0: T, t1: T, t2: T) {
+ var a: T, b: T;
+ a, a, a := *, t0, *; // only one non-* RHS per variable -- this is okay
+ a, a, b, a, b := *, t1, t2, *, *; // only one non-* RHS per variable -- this is okay
+ a, a, b, a, b := *, t1, t2, t0, *; // error: duplicate LHS -- t0 and t1 may be different
+}
+
+method Q<T>(c0: MyClass<T>, c1: MyClass<T>)
+ requires c0 != null && c1 != null;
+ modifies c0, c1;
+{
+ c0.f, c1.f := c0.f, c0.f; // okay -- RHSs are the same
+ c0.f, c0.f, c0.f, c0.f := *, *, c1.f, *; // okay -- only one RHS is non-*
+ c0.f, c0.f, c0.f, c0.f := c0.f, *, c1.f, *; // error -- duplicate LHR
+}
+
+method R<T>(i: nat, j: nat)
+ requires i < 10 && j < 10;
+{
+ var a := new T[10];
+ a[i], a[j] := a[5], a[5]; // okay -- RHSs are the same
+ a[i], a[i], a[i], a[i] := *, *, a[5], *; // okay -- only one RHS is non-*
+ a[i], a[i], a[i], a[j] := *, a[i], a[j], a[i]; // error -- possible duplicate LHS
+}
+
+method S<T>(i: nat, j: nat)
+ requires i < 10 && j < 20;
+{
+ var a := new T[10,20];
+ a[i,j], a[i,i] := a[5,7], a[5,7]; // okay -- RHSs are the same
+ a[i,j], a[i,j], a[i,j], a[i,j] := *, *, a[5,7], *; // okay -- only one RHS is non-*
+ a[i,j], a[i,j], a[i,j], a[i,i] := *, a[i,i], a[i,j], a[i,i]; // error -- possible duplicate LHS
+}
|