diff options
Diffstat (limited to 'Test/aitest0')
| -rw-r--r-- | Test/aitest0/Answer | 2 | ||||
| -rw-r--r-- | Test/aitest0/Intervals.bpl | 14 |
2 files changed, 15 insertions, 1 deletions
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer index 961b3c33..cc518d1b 100644 --- a/Test/aitest0/Answer +++ b/Test/aitest0/Answer @@ -165,4 +165,4 @@ Execution trace: Intervals.bpl(301,3): anon3_LoopHead
Intervals.bpl(301,3): anon3_LoopDone
-Boogie program verifier finished with 15 verified, 11 errors
+Boogie program verifier finished with 16 verified, 11 errors
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;
+ }
+}
|