diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test21/MapOutputTypeParams.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test21/MapOutputTypeParams.bpl')
| -rw-r--r-- | Test/test21/MapOutputTypeParams.bpl | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/Test/test21/MapOutputTypeParams.bpl b/Test/test21/MapOutputTypeParams.bpl new file mode 100644 index 00000000..f0ca307f --- /dev/null +++ b/Test/test21/MapOutputTypeParams.bpl @@ -0,0 +1,33 @@ +
+
+
+var p : <a>[int]a;
+
+procedure P() returns () modifies p; {
+ p[13] := 5;
+ p[17] := true;
+ p[13] := false;
+ p[17] := 8;
+
+ assert p[13] == 5 && !p[13] && p[17] == 8 && p[17];
+ assert p == p[28 := p]; // error
+}
+
+var q : <a, b>[int][a]b;
+
+procedure Q() returns () modifies q; {
+ q[17] := q[17][true := 13];
+ q[17] := q[17][true := false];
+ q[16] := q[17][true := 14];
+
+ assert q[17][true] == 13 && !q[17][true];
+ assert q[17][true] == 14; // error
+}
+
+procedure R() returns () modifies p; {
+ p[7] := 28;
+ p[5] := p[7];
+
+ assert p[7] == 28;
+ assert p[6] == 28; // error
+}
\ No newline at end of file |