Eiffel小抄

class

note
    description: "Simple bank accounts"
 
class
    ACCOUNT
 
feature -- Access
 
    balance: INTEGER
            -- Current balance
 
    deposit_count: INTEGER
            -- Number of deposits made since opening
        do
            if all_deposits /= Void then
                Result := all_deposits.count
            end
        end
 
feature -- Element change
 
    deposit (sum: INTEGER)
            -- Add `sum' to account.
        require
            non_negative: sum >= 0
        do
            if all_deposits = Void then
                create all_deposits
            end
 
            all_deposits.extend (sum)
            balance := balance + sum
        ensure
            one_more_deposit: deposit_count = old deposit_count + 1
            updated: balance = old balance + sum
        end
 
feature {NONE} -- Implementation
 
    all_deposits: DEPOSIT_LIST
            -- List of deposits since account's opening.
 
invariant
    consistent_balance:
        (all_deposits /= Void) implies (balance = all_deposits.total)
    zero_if_no_deposits:
        (all_deposits = Void) implies (balance = 0)
 
end -- class ACCOUNT

inheritance

note
    description: "Savings accounts"
 
class
    SAVINGS_ACCOUNT
 
inherit
    ACCOUNT
        redefine
            deposit
    end
 
feature -- Element change
 
    deposit (sum: INTEGER)
            -- Add sum to account.
        do
            ... New implementation (see below) ...
        end
 
    ... Other features ...
 
end -- class SAVINGS_ACCOUNT

class D
inherit
    A
        rename
            g as f
                -- g was effective in A
        undefine
            f
        export
            {NONE} all
            {ANY} capacity
        end
end

class TEACHING_ASSISTANT
 
inherit
    TEACHER
        rename
            computer_account as faculty_account
        select
            faculty_account
        end
 
    STUDENT
        rename
            computer_account as student_account
        end

end

deferred class

deferred class
    LIST [G]
 
feature -- Access
 
    count: INTEGER
            -- Number of items in list
        do
            ... See below; this feature can be effective ...
        end
 
feature -- Element change
 
    extend (x: G)
            -- Add `x' at end of list.
        require
            space_available: not full
        deferred
        ensure
            one_more: count = old count + 1
        end
 
    ... Other feature declarations and invariants ...
 
end -- class LIST

operator

    infix "<=" (other: like Current): BOOLEAN
            -- Is current object less than or equal to `other'?
        require
            other_exists: other /= Void
        do
            Result := (Current < other) or is_equal (other)
        ensure
            definition: Result = (Current < other) or is_equal (other)
        end

create

            create x.make (2000)
            create x

            create {SAVINGS_ACCOUNT} x.make (2000)
            some_routine (create {ACCOUNT}.make (2000))

if

            if ... then
                ... 
            elseif ... then 
                ... 
            else 
                ... 
            end

switch

            inspect
                exp
            when v1 then
                inst
            when v2 then
                inst2
            ...
            else
                inst0
            end

loop

            from
                initialization
            until
                exit
            invariant -- optional
                inv
            variant   -- optional
                var
            loop
                body
            end

assert

            check
                x_not_void: x /= Void end
                    -- Because x was obtained as a clone of y,
                    -- and y is not void because [etc.]
            end

exception

        local
            attempts: INTEGER
        do
            last_character := low_level_read_function (f)
        rescue
            attempts := attempts + 1
            if attempts < Max_attempts then
                retry
            end
        end