Class ANY

Latest draft of the ELKS2003 proposal incorporating ELKS95 GENERAL plus all motions accepted to date.

(Text that appears in gray has not yet been considered in detail.)

indexing

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

class interface

   ANY

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'

   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", chapter 13)?
      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_identify: 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 of `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