diff options
| author |  leino <unknown> | 2014-11-13 17:40:18 -0800 |
|---|---|---|
| committer | leino <unknown> | 2014-11-13 17:40:18 -0800 |
| commit | f27cb29e16125a4132e67e826c13db46595a838e (patch) | |
| tree | 7cbbe9676548406d236dba73668dbd0eedd73539 /Test/dafny0/ForallCompilation.dfy | |
| parent | cce655873bcbddf737917b198e3e2d75a00213ae (diff) | |
Bug fixes in the compilation of forall statements.
Diffstat (limited to 'Test/dafny0/ForallCompilation.dfy')
| -rw-r--r-- | Test/dafny0/ForallCompilation.dfy | 104 |
1 files changed, 104 insertions, 0 deletions
diff --git a/Test/dafny0/ForallCompilation.dfy b/Test/dafny0/ForallCompilation.dfy new file mode 100644 index 00000000..c812983a --- /dev/null +++ b/Test/dafny0/ForallCompilation.dfy @@ -0,0 +1,104 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+ var c := new MyClass;
+ c.arr := new int[10,20];
+ c.K0(3, 12);
+ c.K1(3, 12);
+ c.K2(3, 12);
+ c.K3(3, 12);
+ c.K4(12);
+ c.M();
+ c.N();
+ c.P();
+ c.Q();
+}
+
+class MyClass
+{
+ var arr: array2<int>;
+
+ method K0(i: int, j: int)
+ requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;
+ modifies arr;
+ {
+ forall k | k in {-3, 4} {
+ arr[i,j] := 50;
+ }
+ }
+
+ method K1(i: int, j: int)
+ requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;
+ // note the absence of a modifies clause
+ {
+ forall k: int | k in {} {
+ arr[i,j] := k; // fine, since control will never reach here
+ }
+ }
+
+ method K2(i: int, j: int)
+ requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;
+ modifies arr;
+ {
+ forall k: int | k in {-3, 4} {
+ // The following would have been an error (since this test file tests
+ // compilation, we don't include the test here):
+ // arr[i,j] := k; // error: k can take on more than one value
+ }
+ }
+
+ method K3(i: int, j: int)
+ requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;
+ modifies arr;
+ {
+ forall k: nat | k in {-3, 4} && k <= i {
+ arr[k,j] := 50; // fine, since k:nat is at least 0
+ }
+ }
+
+ method K4(j: int)
+ requires arr != null && 0 <= j < arr.Length1;
+ modifies arr;
+ {
+ forall i, k: nat | 0 <= i < arr.Length0 && k in {-3, 4} {
+ arr[i,j] := k; // fine, since k can only take on one value
+ }
+ }
+
+ method M()
+ {
+ var ar := new int [3,3];
+ var S: set<int> := {2,0};
+ forall k | k in S {
+ ar[k,1]:= 0;
+ }
+ forall k, j | k in S && j in S {
+ ar[k,j]:= 0;
+ }
+ }
+
+ method N() {
+ var ar := new int[3, 3];
+ ar[2,2] := 0;
+ }
+
+ method P() {
+ var ar := new int[3];
+ var prev := ar[..];
+ var S: set<int> := {};
+ forall k | k in S {
+ ar[k] := 0;
+ }
+ assert ar[..] == prev;
+ }
+
+ method Q() {
+ var ar := new int[3,3];
+ var S: set<int> := {1,2};
+ forall k | k in S {
+ ar[0,0] := 0;
+ }
+ assert ar[0,0] == 0;
+ }
+}
|