diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-19 17:29:04 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-19 17:29:04 -0700 |
| commit | 8d353c7dca06d1121a3751efbb4a85721d81b2dd (patch) | |
| tree | 8e012e0061ed05abdb1e4bde162c66b950fe8aab /Test/dafny0/ControlStructures.dfy | |
| parent | 7992533629faca61ea8a3761b2ee21fd6f27ac18 (diff) | |
Dafny: added alternative statement and alternative-loop statement
Diffstat (limited to 'Test/dafny0/ControlStructures.dfy')
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy index eed74634..35d939d3 100644 --- a/Test/dafny0/ControlStructures.dfy +++ b/Test/dafny0/ControlStructures.dfy @@ -63,3 +63,75 @@ function F1(d: D, x: int): int case Green => 0
case Blue => 2
}
+
+// --------------- alternative statements ---------------------
+
+method A0(x: int) returns (r: int)
+ ensures 0 <= r;
+{
+ if { // error: missing case (x == 0)
+ case x < 0 => r := 12;
+ case 0 < x => r := 13;
+ }
+}
+
+method A1(x: int) returns (r: int)
+ ensures 0 <= r;
+{
+ if {
+ case x <= 0 => r := 12;
+ case 0 <= x => r := 13;
+ }
+}
+
+method DutchFlag(A: array<int>, N: int, l: int, r: int) returns (result: int)
+ requires A != null && N == A.Length;
+ requires 0 <= l && l+2 <= r && r <= N;
+ modifies A;
+ ensures l <= result && result < r;
+ ensures forall k, j :: l <= k && k < result && result <= j && j < r ==> A[k] <= A[j];
+ ensures forall k :: l <= k && k < result ==> A[k] <= old(A[l]);
+ ensures forall k :: result <= k && k < r ==> old(A[l]) <= A[k];
+{
+ var pv := A[l];
+ var i := l;
+ var j := r-1;
+ // swap A[l] and A[j]
+ var tmp := A[l]; A[l] := A[j]; A[j] := tmp;
+
+ while (i < j)
+ invariant l <= i && i <= j && j < r;
+ invariant forall k :: l <= k && k < i ==> A[k] <= pv;
+ invariant forall k :: j <= k && k < r ==> pv <= A[k];
+ {
+ if {
+ case A[i] <= pv =>
+ i := i + 1;
+ case pv <= A[j-1] =>
+ j := j - 1;
+ case A[j-1] < pv && pv < A[i] =>
+ // swap A[j-1] and A[i]
+ tmp := A[i]; A[i] := A[j-1]; A[j-1] := tmp;
+ assert A[i] < pv && pv < A[j-1];
+ i := i + 1;
+ j := j - 1;
+ }
+ }
+ result := i;
+}
+
+// --------------- alternative loop statements ---------------
+
+method B(x: int) returns (r: int)
+ ensures r == 0;
+{
+ r := x;
+ while
+ decreases if 0 <= r then r else -r;
+ {
+ case r < 0 =>
+ r := r + 1;
+ case 0 < r =>
+ r := r - 1;
+ }
+}
|