Partial Correctness of a Fibonacci Algorithm

In this paper we introduce some notions to facilitate formulating and proving properties of iterative algorithms encoded in nominative data language [19] in the Mizar system [3], [1]. It is tested on verification of the partial correctness of an algorithm computing n-th Fibonacci number:

i := 0

s := 0

b := 1

c := 0

while (i <> n)

  c := s

  s := b

  b := c + s

  i := i + 1

return s