+
Point of view
All features
class LOOPS
Summary
top
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
Direct parents
Insert list: ANY
Overview
top
Creation features
{ANY}
Features
{ANY}
make
effective procedure
{ANY}
top
gcd (value_1: INTEGER_32, value_2: INTEGER_32): INTEGER_32
effective function
{ANY}
top
Greatest Common Divisor of value_1 and value_2.
require
  • value_1 > 0
  • value_2 > 0
ensure
  • Result = gcd(value_2, value_1)