Class GENERAL

5.1 Class GENERAL

indexing

description: "Platform-independent universal properties. %
    %This class is an ancestor to all developer-written classes."

class interface

GENERAL

feature -- Access

generating_type: STRING
        -- Name of current object's generating type
        -- (type of which it is a direct instance)

generator: STRING
        -- Name of current object's generating class
        -- (base class of the type of which it is a direct instance)

id_object (id: INTEGER): ANY
        -- Object for which object_id has returned id;
        -- void if none.

object_id: INTEGER
        -- Value identifying current object uniquely;
        -- meaningful only for reference types.

stripped (other: GENERAL): like other
        -- New object with fields copied from current object,
        -- but limited to attributes of type of other.
    require
        conformance: conforms_to (other)
    ensure
        stripped_to_other: Result.same_type (other)

feature -- Status report

frozen conforms_to (other: GENERAL): BOOLEAN
        -- Does type of current object conform to type
        -- of other (as per Eiffel: The Language, chapter13)?
    require
        other_not_void: other /= Void

frozen same_type (other: GENERAL): BOOLEAN
        -- Is type of current object identical to type of other?
    require
        other_not_void: other /= Void
    ensure
        definition: Result = (conforms_to (other) and 
            other.conforms_to (Current))

feature -- Comparison

frozen deep_equal (some: GENERAL; other: like some): BOOLEAN
        -- Are some and other either both void
        -- or attached to isomorphic object structures?
    ensure
        shallow_implies_deep: standard_equal (some, other) implies Result;
        same_type: Result implies some.same_type (other);
        symmetric: Result implies deep_equal (other, some)

frozen equal (some: GENERAL; other: like some): BOOLEAN
        -- Are some and other either both void or attached
        -- to objects considered equal?
    ensure
        definition: Result = (some = Void and other = Void) or else
            ((some /= Void and other /= Void) and then some.is_equal (other));

is_equal (other: like Current): BOOLEAN
        -- Is other attached to an object considered equal
        -- to current object?
    require
        other_not_void: other /= Void
    ensure
        consistent: standard_is_equal (other) implies Result;
        same_type: Result implies same_type (other);
        symmetric: Result implies other.is_equal (Current)

frozen standard_equal (some: GENERAL; other: like some): BOOLEAN
        -- Are some and other either both void or attached to
        -- field-by-field identical objects of the same type?
        -- Always uses the default object comparison criterion.
    ensure
        definition: Result = (some = Void and other = Void) or else
            ((some /= Void and other /= Void) and then
                some.standard_is_equal (other))

frozen standard_is_equal (other: like Current): BOOLEAN
        -- Is other attached to an object of the same type as
        -- current object, and field-by-field identical to it?
    require
        other_not_void: other /= Void
    ensure
        same_type: Result implies same_type (other);
        symmetric: Result implies other.standard_is_equal (Current)

feature -- Duplication

frozen clone (other: GENERAL): like other
        -- Void if other is void; otherwise new object
        -- equal to other.
    ensure
        equal: equal (Result, other)

copy (other: like Current)
        -- Update current object using fields of object attached
        -- to other, so as to yield equal objects.
    require
        other_not_void: other /= Void; 
        type_identity: same_type (other)
    ensure
        is_equal: is_equal (other)

frozen deep_clone (other: GENERAL): like other
        -- Void if other is void: otherwise, new object structure
        -- recursively duplicated from the one attached to other
    ensure
        deep_equal: deep_equal (other, Result)

frozen standard_clone (other: GENERAL): like other
        -- Void if other is void; otherwise new object
        -- field-by-field identical to other.
        -- Always uses the default copying semantics.
    ensure
        equal: standard_equal (Result, other)

frozen standard_copy (other: like Current)
        -- Copy every field of other onto corresponding field
        -- of current object.
    require
        other_not_void: other /= Void; 
        type_identity: same_type (other)
    ensure
        is_standard_equal: standard_is_equal (other)

feature -- Basic operations

frozen default: like Current
        -- Default value of current type

frozen default_pointer: POINTER
        -- Default value of type POINTER
        -- (Avoid the need to write p.default for some p
        -- of type POINTER.)
    ensure
        Result = Result.default

default_rescue
        -- Handle exception if no Rescue clause.
        -- (Default: do nothing.)

frozen do_nothing
        -- Execute a null action.

frozen Void: NONE
        -- Void reference

feature -- Output

io: STD_FILES
        -- Handle to standard file setup

out: STRING
        -- New string containing terse printable representation
        -- of current object

print (some: GENERAL)
        -- Write terse external representation of some on
        -- standard output.

frozen tagged_out: STRING
        -- New string containing printable representation of
        -- current object, each field preceded by its attribute
        -- name, a colon and a space.

invariant

reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
involutive_object_id: id_object (object_id) = Current

end