diff options
author | Dietrich <dgeisler50@gmail.com> | 2015-04-20 05:20:06 -0600 |
---|---|---|
committer | Dietrich <dgeisler50@gmail.com> | 2015-04-20 05:20:06 -0600 |
commit | 4f35766542c5735374b85f66006afea875f07b79 (patch) | |
tree | 76842d97212c417a28baf425e9b30fb2a6ecf3f7 /float_test.bpl | |
parent | bdb6a7db94de0310fb6535facb33782fe231c013 (diff) |
added a collection of console writes for debugging. These should be removed in a future commit
Diffstat (limited to 'float_test.bpl')
-rw-r--r-- | float_test.bpl | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/float_test.bpl b/float_test.bpl index 22e436a1..ebd0ab47 100644 --- a/float_test.bpl +++ b/float_test.bpl @@ -1,11 +1,5 @@ -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? +procedure F(n: float) returns(r: float) + ensures r == n; { - if (100 < n) { - r := n - 10; - } else { - call r := F(n + 11); - call r := F(r); - } + r := n; }
\ No newline at end of file |