This commit use array with a purely functional styles to process them.
In particular, it uses recursive function instead of while loop.
Those benchmarks are easier to debug than the equivalent ones relying
on imperative features, because they do not go through any code
transformations.

Note that they still have the same limitation as the imperative ones
(cannot prove inductive properties), which shows that the imperative
transformation are not responsible for the limitation in proving
validity of program over arrays.