application.e

class
    APPLICATION

inherit
    ARGUMENTS

create
    make

feature {NONE} -- Initialization

    make
            -- Run application.
        do
            create my_account
        end

    my_account: BANK_ACCOUNT

end

bank_account.e

class
    BANK_ACCOUNT
inherit
    ANY
        redefine
            default_create
        end
feature
    default_create
        do
            balance := 0
        end

    balance: INTEGER

    deposit (an_amount: INTEGER)
            -- Deposit `an_amount'.
        require
            amount_large_enough: an_amount > 0
        do
        ensure
            balance_increased: balance > old balance
            deposited: balance = old balance + an_amount
        end

    withdraw (an_amount: INTEGER)
            -- Withdraw `an_amount'.
        require
            amount_large_enough: an_amount > 0
            amount_valid: balance >= an_amount
        do
            balance := balance - an_amount
        ensure
            balance_decreased: balance < old balance
            withdrawn: balance = old balance + an_amount
        end

invariant
    balance_not_negative: balance >= 0
end

test_bank_account.e

note
    description: "[
        Eiffel tests that can be executed by testing tool.
    ]"
    author: "EiffelStudio test wizard"
    date: "$Date$"
    revision: "$Revision$"
    testing: "type/manual"

class
    TEST_BANK_ACCOUNT

inherit
    EQA_TEST_SET

feature -- Test routines

    test_deposit_01
            -- New test routine
        note
            testing:  "covers/{BANK_ACCOUNT}.deposit"
        local
            l_ba: BANK_ACCOUNT
        do
            create l_ba
            l_ba.deposit (500)
        end
end

test_bank_account.ecf

<?xml version="1.0" encoding="ISO-8859-1"?>
<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-22-0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.eiffel.com/developers/xml/configuration-1-22-0 http://www.eiffel.com/developers/xml/configuration-1-22-0.xsd" name="test_bank_account" uuid="D0523DC1-EA64-4357-8063-C16AC4F30744">
	<target name="test_bank_account">
		<root class="TEST_BANK_ACCOUNT" feature="make"/>
		<setting name="console_application" value="true"/>
		<precompile name="base_pre" location="$ISE_PRECOMP\base-scoop-safe.ecf"/>
		<library name="base" location="$ISE_LIBRARY\library\base\base.ecf"/>
		<library name="testing" location="$ISE_LIBRARY\library\testing\testing.ecf"/>
		<cluster name="test_bank_account" location=".\"/>
	</target>
</system>