note
    description: "Summary description for {PERSON}."
    author: ""
    date: "$Date$"
    revision: "$Revision$"

class
    PERSON

create
    set_name

feature
    name: STRING

feature
    set_name(a_name: STRING)
        require
          no_void_and_name:
            a_name /= Void and then not a_name.is_empty
        do
            name := a_name
        end

invariant
    person_has_a_name: name /= Void implies not name.is_empty
end


note
    description : "new application root class"
    date        : "$Date$"
    revision    : "$Revision$"

class
    APPLICATION

inherit
    ARGUMENTS

create
    make

feature {NONE} -- Initialization

    make
            -- Run application.
    local
        p1, p2: PERSON
        do
            create p1.set_name ("person 1")
            create p2.set_name (p1.name)
            p1.set_name ("Another name")
            print(p2.name)
        end

end