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 | 7ca1c590659d2c11a67b138b8251cf5dffc03b38 (patch) | |
| tree | 0c7f17bef9ca346312468d1901729026923995c9 /Test | |
| parent | 03b24df6c2fa4217f74d3cc76785ab6babbe6f2f (diff) | |
Dafny: added alternative statement and alternative-loop statement
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 72 |
2 files changed, 77 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 28f438af..e0874a66 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -573,8 +573,12 @@ Execution trace: (0,0): anon10_Else
(0,0): anon11_Else
(0,0): anon12_Then
+ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibilties
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
-Dafny program verifier finished with 8 verified, 5 errors
+Dafny program verifier finished with 15 verified, 6 errors
-------------------- Termination.dfy --------------------
Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
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;
+ }
+}
|