Eiffel

Eiffel was designed by Bertrand Meyer in 1985. Its key idea is design by contract: every method states what it requires from callers and what it guarantees in return, and the class states what is always true. The contract is part of the code, so it is checked, documented and inherited.

Paradigm: Object-Oriented Programming

What Makes Eiffel Special

  • Preconditions. A require clause states what must be true when a method is called. If it fails, the caller is at fault.
  • Postconditions. An ensure clause states what the method promises. old balance refers to the value before the call.
  • Class invariants. An invariant clause states what must hold for every object of the class between calls.
  • Contracts are inherited. A subclass may weaken preconditions and strengthen postconditions, which captures the Liskov substitution principle in the language.
  • Uniform access and multiple inheritance. Callers cannot tell a stored attribute from a computed one, and a class may inherit from several parents, with explicit renaming to resolve clashes.

Example: A bank account with a contract

class ACCOUNT
create make
feature
    balance: INTEGER

    make
        do
            balance := 0
        end

    deposit (amount: INTEGER)
        require
            positive_amount: amount > 0
        do
            balance := balance + amount
        ensure
            balance_increased: balance = old balance + amount
        end

    withdraw (amount: INTEGER)
        require
            positive_amount: amount > 0
            enough_funds: amount <= balance
        do
            balance := balance - amount
        ensure
            balance_decreased: balance = old balance - amount
        end

invariant
    never_negative: balance >= 0
end

How It Works

  • create make declares make as the constructor, and the feature section holds the attribute balance and the methods.
  • Each assertion has a tag such as enough_funds. When a contract is violated at runtime, the tag appears in the error message.
  • If code calls withdraw (500) on an account holding 100, the enough_funds precondition fails and points to the caller as the culprit.
  • The invariant must hold after every call, so a balance can never be negative.

History and Where It Is Used

Eiffel is used in finance, aerospace and the design of software with strict correctness needs, and EiffelStudio is the main environment. Its influence is broader than its adoption: contracts appear in Ada 2012, C++ contracts, Kotlin's require, and Python and Java tools such as icontract and JML.

Learn More