Class FIBONACCI

I was somewhat surprised to see this class in FreeELKS.

WHY? It doesn't appear to be used by anything else.

Anyway, I was rather intrigued, and gave it a try (I was interested in timing the n_th number).

I soon spotted that it was giving errors, and it was immediately obvious why. Here is a copy of the code:

i_th (i: INTEGER_32): INTEGER_32 -- The `i'-th Fibonacci number require -- from COUNTABLE positive_argument: i > 0 local count: INTEGER_32 last, second_last: INTEGER_32 do if i = 1 then Result := first elseif i = 2 then Result := second else from last := second second_last := first count := 2 until count = i loop Result := last + second_last second_last := last last := Result count := count + 1 end end end

It's using 32-bit signed arithmetic, so wrap-around soon occurs.

Another interesting point about this code, is the lack of postconditions. My first thought was that it should give the classical recursive definitions in the postconditions. My second thought was that although that would be fine, they wouldn't catch the overflow error. So my next thought was that some properties would help - one property is that the result is greater than i_th (n - 1). This would at least catch the problem if you happened to choose the first overflowing number, and you can do that by looping up from 1. A more complete version of this property would catch it for any number that triggers incorrect behaviour, by calling an agent on the INTEGER_INTERVAL (1 |..| n - 1).

Anyway, there isn't much point in writing the correct postconditions on a routine that can't be corrected. So I tried using MA_DECIMAL instead (it's a pity we don't have a standard class for true integers - Haskell does this better than us, but MA_DECIMAL is a good stand-in). Although it prints (by default - I was too lazy to write a proper formatter) the large numbers in scientific notation, examining the mantissa is a good enough check on the accuracy for starters. And it is reasonably fast too. Using ISE 6.3, I get 29 milliseconds to print F(15000). Using GEC instead, this goes down to 12 milliseconds. In comparison, using GHC to compile a Haskell program, which prints all the digits, it takes 14 milliseconds.

Using GEC and the FIBONNACI class gets a result in about 1 millisecond (the time command on Linux has millisecond precision). But the result is wrong. I vote for removing this from FreeELKS - it's too embarrassing.