Control Flow in Eiffel

Control flow decides what a program does and how many times it does it. Eiffel gives you a clean, readable set of constructs — if/elseif/else for branching, inspect for multi-way selection, and the from ... until ... loop form for iteration — all closed with the same end keyword that delimits every other Eiffel construct. If you’ve written control flow in Pascal or Ada, the spelling will feel familiar; the rigor underneath will not.

What makes control flow in Eiffel distinctive is its connection to Design by Contract. Eiffel’s loop is the only mainstream looping construct with built-in correctness clauses: a loop invariant states what must hold true on every iteration, and a loop variant is an integer expression that must strictly decrease, mathematically guaranteeing the loop terminates. These turn an ordinary loop into a small, checkable proof. Another thing newcomers notice quickly: Eiffel has no break and no continue. A loop exits exactly when its until condition becomes true, which keeps loops honest and easy to reason about.

In this tutorial you’ll branch with if/elseif/else, select among many cases with inspect, iterate with the from/until/loop form and the across cursor loop, exit a loop early the idiomatic Eiffel way, and add a variant/invariant contract to a loop. As you saw in Hello World, every program is a class with a creation procedure — here we’ll put each demonstration in its own feature and call them all from make.

Conditionals: if, elseif, else

The if construct evaluates a boolean condition and runs the matching branch. Chain further tests with elseif (one word), provide a fallback with else, and close the whole form with end. Eiffel has no separate ternary operator — you assign to a local in each branch instead, which keeps intent explicit.

Eiffel’s boolean operators are spelled as words: and, or, not, plus the short-circuit variants and then and or else. Comparison operators (<, <=, >, >=, =, /=) work as you’d expect, with /= meaning “not equal”.

show_conditionals (temperature: INTEGER)
        -- Classify `temperature` with if/elseif/else.
    local
        label: STRING
    do
        if temperature > 30 then
            print ("It is hot%N")
        elseif temperature >= 15 then
            print ("It is mild%N")
        else
            print ("It is cold%N")
        end
            -- Eiffel has no ternary; assign in each branch instead
        if temperature >= 15 then
            label := "comfortable"
        else
            label := "chilly"
        end
        print ("Today is " + label + "%N")
    end

Multi-way branching: inspect

When you are comparing a single integer or character against fixed values, inspect is clearer than a long if/elseif chain. Each when clause lists one or more candidate values (separated by commas) or a value interval, and the optional else handles everything not matched. Unlike C’s switch, there is no fall-through and no break is needed — exactly one branch runs.

show_inspect (day: INTEGER)
        -- Multi-way branch on an integer with inspect.
    do
        inspect day
        when 1, 2, 3, 4, 5 then
            print ("Weekday%N")
        when 6, 7 then
            print ("Weekend%N")
        else
            print ("Invalid day%N")
        end
    end

inspect only works on values that are constant at compile time — integers and characters — which is precisely what makes it fast and unambiguous. For branching on arbitrary boolean tests, reach for if/elseif instead.

Loops: from / until / loop and across

Eiffel’s primary loop is the from ... until ... loop ... end form. It reads top to bottom as four parts: from runs once to initialize, until gives the exit condition (the loop continues while it is false), loop holds the body, and end closes it. Note the inversion from C-style while: you write the condition under which the loop stops, not the one under which it continues.

For walking a range or collection, the across cursor loop is more concise. The |..| operator builds an integer interval, and as ic names a cursor whose current value is ic.item.

show_counting_loop
        -- Count from 1 to 5 with from/until/loop.
    local
        i: INTEGER
    do
        from
            i := 1
        until
            i > 5
        loop
            print ("Count: " + i.out + "%N")
            i := i + 1
        end
    end

show_across_loop
        -- Iterate over an integer interval, printing even numbers.
    do
        across 1 |..| 5 as ic loop
            if ic.item \\ 2 = 0 then
                print ("Even: " + ic.item.out + "%N")
            end
        end
    end

Two details from the operators tutorial carry over: assignment uses := (so i := i + 1 advances the counter, while = stays reserved for equality), and \\ is the integer remainder operator, so ic.item \\ 2 = 0 tests for an even number. The .out feature, inherited from ANY, converts any value to its STRING form for printing.

Exiting a loop early

Because Eiffel has no break statement, the idiomatic way to leave a loop before its range is exhausted is to fold an extra condition into the until clause — typically a boolean flag that the body sets when it finds what it is looking for. This keeps the exit condition visible in one place rather than buried in the body.

show_search
        -- Stop scanning as soon as the target is found.
    local
        i: INTEGER
        found: BOOLEAN
    do
        from
            i := 1
        until
            i > 10 or found
        loop
            if i = 4 then
                print ("Found at " + i.out + "%N")
                found := True
            end
            i := i + 1
        end
    end

When i reaches 4, the body sets found to True; on the next test the until condition i > 10 or found becomes true and the loop stops. Using or (or the short-circuit or else) to combine exit conditions is the standard Eiffel substitute for break. The boolean literals are capitalized: True and False.

Contract-aware loops: variant and invariant

Here is where Eiffel’s loop goes beyond every C-family language. A loop may carry an invariant — assertions that must hold before the loop starts and after every iteration — and a variant, an integer expression that must stay non-negative and strictly decrease each pass. Together they let the compiler (with assertions enabled) catch a loop that breaks its own logic or fails to terminate. The clause order is from, invariant, until, loop, variant, end.

Create a file named loop_variant.e:

note
    description: "A loop carrying a correctness contract"

class
    LOOP_VARIANT

create
    make

feature

    make
            -- Sum the integers 1..n, with the loop proving its own correctness.
        local
            i, sum, n: INTEGER
        do
            n := 5
            from
                i := 1
                sum := 0
            invariant
                i_in_range: i >= 1 and i <= n + 1
                sum_correct: sum = (i - 1) * i // 2
            until
                i > n
            loop
                sum := sum + i
                i := i + 1
            variant
                n - i + 1
            end
            print ("Sum 1.." + n.out + " = " + sum.out + "%N")
        end

end

The invariant sum_correct states the running sum always equals the sum of 1 through i - 1 (the closed form (i - 1) * i // 2), and i_in_range bounds the counter. The variant n - i + 1 starts at 5 and shrinks to 1 as i climbs — proving the loop must end. If a future edit broke either property, an assertion violation would point straight at the loop. Recall that // is integer division, so (i - 1) * i // 2 evaluates left to right as ((i - 1) * i) // 2.

The Complete Program

The four demonstration features above live together in one class. Create a file named control_flow.e:

note
    description: "Demonstrates control flow constructs in Eiffel"

class
    CONTROL_FLOW

create
    make

feature -- Initialization

    make
            -- Run every control flow demonstration in turn.
        do
            show_conditionals (18)
            show_inspect (6)
            show_counting_loop
            show_across_loop
            show_search
        end

feature -- Demonstrations

    show_conditionals (temperature: INTEGER)
            -- Classify `temperature` with if/elseif/else.
        local
            label: STRING
        do
            if temperature > 30 then
                print ("It is hot%N")
            elseif temperature >= 15 then
                print ("It is mild%N")
            else
                print ("It is cold%N")
            end
            if temperature >= 15 then
                label := "comfortable"
            else
                label := "chilly"
            end
            print ("Today is " + label + "%N")
        end

    show_inspect (day: INTEGER)
            -- Multi-way branch on an integer with inspect.
        do
            inspect day
            when 1, 2, 3, 4, 5 then
                print ("Weekday%N")
            when 6, 7 then
                print ("Weekend%N")
            else
                print ("Invalid day%N")
            end
        end

    show_counting_loop
            -- Count from 1 to 5 with from/until/loop.
        local
            i: INTEGER
        do
            from
                i := 1
            until
                i > 5
            loop
                print ("Count: " + i.out + "%N")
                i := i + 1
            end
        end

    show_across_loop
            -- Iterate over an integer interval, printing even numbers.
        do
            across 1 |..| 5 as ic loop
                if ic.item \\ 2 = 0 then
                    print ("Even: " + ic.item.out + "%N")
                end
            end
        end

    show_search
            -- Stop scanning as soon as the target is found.
        local
            i: INTEGER
            found: BOOLEAN
        do
            from
                i := 1
            until
                i > 10 or found
            loop
                if i = 4 then
                    print ("Found at " + i.out + "%N")
                    found := True
                end
                i := i + 1
            end
        end

end

The ECF Configuration File

As you saw in Hello World, each Eiffel system needs an .ecf file naming its root class and entry feature. Create a file named control_flow.ecf:

1
2
3
4
5
6
7
8
9

<?xml version="1.0" encoding="ISO-8859-1"?>
<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-22-0" name="control_flow" uuid="00000000-0000-0000-0000-000000000002">
    <target name="control_flow">
        <root class="CONTROL_FLOW" feature="make"/>
        <setting name="console_application" value="true"/>
        <library name="base" location="$ISE_LIBRARY/library/base/base.ecf"/>
        <cluster name="root_cluster" location="."/>
    </target>
</system>

For the contract loop example, create a file named loop_variant.ecf with the system and target renamed to loop_variant and the root class set to LOOP_VARIANT:

1
2
3
4
5
6
7
8
9

<?xml version="1.0" encoding="ISO-8859-1"?>
<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-22-0" name="loop_variant" uuid="00000000-0000-0000-0000-000000000003">
    <target name="loop_variant">
        <root class="LOOP_VARIANT" feature="make"/>
        <setting name="console_application" value="true"/>
        <library name="base" location="$ISE_LIBRARY/library/base/base.ecf"/>
        <cluster name="root_cluster" location="."/>
    </target>
</system>

Running with Docker

1
2
3
4
5
6
7
8

# Pull the official EiffelStudio image
docker pull eiffel/eiffel:latest

# Compile and run the main control flow program
docker run --rm -v $(pwd):/app -w /app eiffel/eiffel:latest sh -c 'ec -batch -config control_flow.ecf -c_compile && ./EIFGENs/control_flow/W_code/control_flow'

# Compile and run the contract-aware loop
docker run --rm -v $(pwd):/app -w /app eiffel/eiffel:latest sh -c 'ec -batch -config loop_variant.ecf -c_compile && ./EIFGENs/loop_variant/W_code/loop_variant'

The workbench (W_code) build used here enables contract checking by default, so the loop invariant and variant in loop_variant.e are actively verified at runtime.

Expected Output

Running control_flow:

It is mild
Today is comfortable
Weekend
Count: 1
Count: 2
Count: 3
Count: 4
Count: 5
Even: 2
Even: 4
Found at 4

Running loop_variant:

Sum 1..5 = 15

Key Concepts

• if/elseif/else/end — elseif is one word, every form closes with end, and there is no ternary operator; assign to a local in each branch when you need a conditional value.
• Word-spelled booleans — combine conditions with and, or, not, and the short-circuit and then / or else; inequality is /=.
• inspect for selection — a clean multi-way branch over integers or characters with comma-separated when values and an optional else; exactly one branch runs, with no fall-through and no break needed.
• from/until/loop — the until clause states when the loop stops, the inverse of a C-style while; initialization lives in from and the body in loop.
• across cursor loops — iterate an interval built with |..| (or any collection) using as ic and ic.item, the concise choice for range and collection traversal.
• No break or continue — exit early by folding a boolean flag into the until condition with or; loops always leave through a single, visible exit test.
• Contract-aware loops — a loop invariant must hold on every iteration and a variant integer expression must strictly decrease, turning a loop into a checkable proof of correctness and termination — a capability unique to Eiffel among mainstream languages.