Fibonacci:::OBJECT
Fibonacci.a <= Fibonacci.c
Fibonacci.b <= Fibonacci.c
Fibonacci.c == Fibonacci.a + Fibonacci.b
===========================================================================
Fibonacci.compute():::ENTER
===========================================================================
Fibonacci.compute():::EXIT
Fibonacci.a == orig(Fibonacci.b)
Fibonacci.b == orig(Fibonacci.c)
Fibonacci.a <= Fibonacci.b
Fibonacci.a < Fibonacci.c
Fibonacci.b >= orig(Fibonacci.a)
Fibonacci.c >= orig(Fibonacci.a)
orig(Fibonacci.a) == - Fibonacci.a + Fibonacci.b
orig(Fibonacci.a) == - 2 * Fibonacci.a + Fibonacci.c
orig(Fibonacci.a) == 2 * Fibonacci.b - Fibonacci.c