Eiffel

Eiffel is a programming language that changed how we think about software correctness. Created by Bertrand Meyer in 1986, Eiffel introduced Design by Contract (DbC) - an approach where the “contract” between software components is explicitly written into the code and verified at runtime.

History & Origins

In the mid-1980s, Bertrand Meyer was frustrated with the state of commercial software development. After experience with Ada, Simula, and formal specification methods like Z notation, he set out to create a language that would make software reliability a first-class concern.

The Vision

Meyer’s goal was ambitious: create a language where:

1. Correctness is provable - Demonstrated rather than hoped for
2. Contracts are explicit - What a routine expects and guarantees is documented in code
3. Reuse is safe - Inheritance and polymorphism work correctly by design
4. Development is efficient - Despite the rigor, productivity remains high

From Formal Methods to a Language

Meyer had studied formal specification methods, particularly Tony Hoare’s axiomatic semantics and Jean-Raymond Abrial’s Z notation (which Meyer contributed to around 1978-79), and believed their rigor could be embedded directly into a practical programming language rather than remaining in separate mathematical documents. In the software of the time, preconditions assumed by a routine’s callers were never written down, and class invariants drifted as systems evolved.

Eiffel was first introduced publicly at the inaugural OOPSLA conference in October 1986, with the first commercial release from Interactive Software Engineering (ISE) following later that year. ISE, later renamed Eiffel Software, produced the EiffelStudio IDE and maintained the reference implementation, with Meyer serving as chairman and chief technology officer.

The Name

Eiffel was named after the Eiffel Tower - a symbol of elegant engineering. Just as Gustave Eiffel’s tower represents structural integrity and aesthetic beauty, the language aims to combine software correctness with clean design.

Standardization

ECMA International approved the 1st edition of ECMA-367 on June 21, 2005, formally titled “Eiffel: Analysis, Design and Programming Language.” The 2nd edition was adopted in June 2006, and ISO published it as ISO/IEC 25436 in November of that year. The title reflects Meyer’s conviction that a single consistent notation should span the software development lifecycle, from requirements analysis through design to executable code.

Design by Contract

Eiffel’s defining contribution to computer science is Design by Contract, now adopted by many modern languages.

The Contract Metaphor

Just as business contracts specify:

• What each party must provide (preconditions)
• What each party will receive (postconditions)
• What both parties agree to maintain (invariants)

Software contracts specify:

deposit (amount: INTEGER)
    -- Add amount to balance
    require
        amount_positive: amount > 0
    do
        balance := balance + amount
    ensure
        balance_increased: balance = old balance + amount
    end

Contract Elements

1. Preconditions (require) - What must be true before calling a routine
2. Postconditions (ensure) - What will be true after the routine completes
3. Class Invariants (invariant) - What is always true for any instance of the class

Runtime Checking

Contracts are checked at runtime (in debug mode), catching bugs immediately:

*** PRECONDITION VIOLATION ***
Class: BANK_ACCOUNT
Routine: deposit
Precondition: amount_positive

This “fail fast” approach catches bugs at their source.

Three Roles of a Contract

Contracts are documentation, specifying intent precisely; tests, checked at runtime in debug builds; and formal specifications, amenable to static analysis and proof. Meyer’s broader philosophy, articulated in Object-Oriented Software Construction, is that software should be correct by construction rather than correct by testing.

Why Eiffel Still Matters

1. Influence on Modern Languages

Design by Contract influenced:

• Java - Assertions, though less integrated
• C# - Code Contracts library
• D - Built-in contract syntax
• Ruby - Contract-style assertions and design patterns
• Ada 2012 - Added contract-based programming
• Spec# - Microsoft Research extension of C#
• JML (Java Modeling Language) - Adapted Eiffel’s contract notation for annotation-based use
• Kotlin - Eiffel’s Design by Contract has reportedly been cited as an influence on Kotlin’s contracts feature

2. Multiple Inheritance Done Right

Eiffel solves the “diamond problem” that plagued C++ through:

• Renaming - Inherited features can be renamed to avoid conflicts
• Redefinition - Methods can be overridden with new implementations
• Selection - When features conflict, you explicitly choose which to use
• Export status - Fine-grained control over feature visibility

3. Void Safety

Before Kotlin’s “billion-dollar mistake” solution, Eiffel addressed null references:

feature {NONE} -- Creation
    make
        do
            -- Must initialize all attached attributes
            create name.make_empty
        end

feature -- Access
    name: STRING  -- Cannot be Void (null)

    optional_data: detachable STRING  -- Can be Void, must be checked

The ECMA-367 2nd edition introduced this distinction. The compiler statically verifies that attached references are always initialized before use and that detachable references are checked before dereferencing.

4. Command-Query Separation

Eiffel enforces a clean principle: functions return values but don’t change state; procedures change state but don’t return values.

-- Query: Returns count, no side effects
count: INTEGER
    do
        Result := internal_count
    end

-- Command: Modifies state, no return value
increment
    do
        internal_count := internal_count + 1
    end

5. Uniform Access Principle

Clients of a class cannot tell whether they are accessing a stored attribute or computing a result through a function, because the syntax is identical. bank.balance could be either, so the internal implementation can change from a stored value to a computed one without breaking client code.

The Eiffel Compilation System

Melting Ice Technology

EiffelStudio uses “Melting Ice” compilation:

1. Frozen code - Fully compiled to C, then machine code
2. Melted code - Interpreted for rapid development iteration

During development, only changed code is “melted” (interpreted), giving near-instant recompilation. For deployment, everything is “frozen” (compiled) for maximum performance.

Finalization

For production, Eiffel code is:

1. Translated to optimized C
2. Compiled with your platform’s C compiler
3. Linked into a native executable

No runtime environment needed - just like C or C++.

Compilation Targets

EiffelStudio can target native code on Linux, Windows, and macOS through a C backend, and .NET / .NET Core through Common Intermediate Language (CIL) generation.

Modern Eiffel Features

Generic Programming

class LIST [G]
feature
    extend (item: G)
        do
            -- Add item of type G to list
        end

    item: G
        -- Current item
end

Generic parameters can be constrained. G -> COMPARABLE requires that G supports comparison, enabling type-safe generic algorithms:

class SORTED_LIST [G -> COMPARABLE]
feature
    extend (item: G)
        do
            -- Insert item in sorted position
        end

    has (item: G): BOOLEAN
        do
            -- Binary search
        end
end

Agents (Closures)

feature
    apply_to_all (action: PROCEDURE [INTEGER])
        do
            across 1 |..| 10 as i loop
                action.call ([i.item])
            end
        end

    example
        do
            apply_to_all (agent print_number)
        end

    print_number (n: INTEGER)
        do
            print (n.out + "%N")
        end
end

SCOOP (Simple Concurrent Object-Oriented Programming)

Eiffel’s approach to concurrency:

class WORKER
feature
    process (data: separate DATA_SOURCE)
        -- Automatically handles synchronization
        do
            data.fetch
            data.transform
        end
end

The separate keyword indicates an object may be in another processor/thread, with automatic locking.

When a routine receives a separate argument, Eiffel guarantees exclusive access for the duration of the call, eliminating data races without manual mutex management.

The Standard Library: EiffelBase

The canonical Eiffel library, EiffelBase, provides foundational data structures and algorithms with full contract specifications. Every class specifies preconditions, postconditions, and invariants as part of its interface, so the library’s documentation is itself executable and verifiable.

EiffelStudio IDE

Eiffel comes with an IDE including:

• Graphical class browser - Navigate inheritance hierarchies visually
• Contract viewer - See all contracts for any class
• Automatic documentation - Generate HTML docs from contracts
• Debugging with contracts - Breakpoints on contract violations
• Metrics - Code quality measurements

The OOSC Books

Meyer’s Object-Oriented Software Construction set out the reasoning behind the language:

• 1st edition (1988): Introduced Design by Contract and justified Eiffel’s design
• 2nd edition (1997): Expanded to over 1,300 pages, won a Jolt Award, and separated general OOP principles from Eiffel-specific notation

The Eiffel Community

Resources

• eiffel.org - Official language site
• EiffelStudio - The main IDE (free Community Edition available)
• Eiffel Software - Commercial support and tools
• ECMA-367 - ECMA standard documentation

Open Source Implementations

• EiffelStudio GPL Edition - Full IDE, GPL licensed
• Liberty Eiffel - Alternative open-source compiler
• gobo.sourceforge.net - Open-source Eiffel libraries
• Gobo Eiffel - Portable MIT-licensed compiler committed to ECMA-367 compliance
• SmartEiffel - Dormant GPL compiler, the project Liberty Eiffel forked from; it diverged from the ECMA standard and can emit Java bytecode

Getting Started

Eiffel source files use:

• .e - Eiffel class files (one class per file)
• .ecf - Eiffel configuration files (project settings)

The convention is lowercase filename matching class name:

• bank_account.e contains class BANK_ACCOUNT

A Complete Example

Here’s a small but complete Eiffel class showing contracts:

note
    description: "A simple counter with bounds checking"

class
    BOUNDED_COUNTER

create
    make

feature {NONE} -- Initialization

    make (a_max: INTEGER)
            -- Initialize with maximum value
        require
            max_positive: a_max > 0
        do
            maximum := a_max
            value := 0
        ensure
            maximum_set: maximum = a_max
            value_zero: value = 0
        end

feature -- Access

    value: INTEGER
            -- Current counter value

    maximum: INTEGER
            -- Maximum allowed value

feature -- Basic operations

    increment
            -- Increase value by one
        require
            not_at_maximum: value < maximum
        do
            value := value + 1
        ensure
            incremented: value = old value + 1
        end

    reset
            -- Reset to zero
        do
            value := 0
        ensure
            reset_done: value = 0
        end

invariant
    value_in_bounds: value >= 0 and value <= maximum
    maximum_positive: maximum > 0

end

Every method documents what it requires, what it ensures, and the class maintains its invariant at all times.

Continue to the Hello World tutorial to write your first Eiffel program.