diff options
Diffstat (limited to 'Test/aitest0/Intervals.bpl')
| -rw-r--r-- | Test/aitest0/Intervals.bpl | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl index 6a588bbe..c769645f 100644 --- a/Test/aitest0/Intervals.bpl +++ b/Test/aitest0/Intervals.bpl @@ -316,3 +316,17 @@ procedure Id17(n: int) assert 0 <= i; // fine: SometimesId2 claims to be an identity and the use of it is int->int
}
+// real numbers
+
+procedure W0(N: real)
+{
+ var i, bf0: real;
+ i := 0.0;
+ while (i < N) {
+ bf0 := N - i;
+ i := i + 1.0;
+ // check termination:
+ assert 0.0 <= bf0;
+ assert N - i <= bf0 - 1.0;
+ }
+}
|