diff options
author | Dietrich <dgeisler50@gmail.com> | 2015-04-20 04:19:48 -0600 |
---|---|---|
committer | Dietrich <dgeisler50@gmail.com> | 2015-04-20 04:19:48 -0600 |
commit | bdb6a7db94de0310fb6535facb33782fe231c013 (patch) | |
tree | 7917a67d2a9e60c35651bd740c6d02ca464fd23d /float_test.bpl | |
parent | 50ea5ab6baf31da6fa3be4f1420d683fd54013cd (diff) |
added a file for float type testing
Diffstat (limited to 'float_test.bpl')
-rw-r--r-- | float_test.bpl | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/float_test.bpl b/float_test.bpl new file mode 100644 index 00000000..22e436a1 --- /dev/null +++ b/float_test.bpl @@ -0,0 +1,11 @@ +procedure F(n: int) returns (r: int) + ensures 100 < n ==> r == n - 10; // This postcondition is easy to check by hand + ensures n <= 100 ==> r == 91; // Do you believe this one is true? +{ + if (100 < n) { + r := n - 10; + } else { + call r := F(n + 11); + call r := F(r); + } +}
\ No newline at end of file |