Have a look at feature gcd to have an example of assertions in a loop.
Also note that Liberty Eiffel handles recursivity in assertions.
(There is also a feature gcd in class INTEGER_GENERAL.)
compile the program with -loop_check to validate loop
assertions (variant and invariant) at runtime