VDRD, chapter 10 (Feature adaptation), page 163

     Redeclaration rule

     Let `C' be a class and `g' a feature of `C'.   It  is
     valid  for `g' to be a redeclaration of a feature `f'
     inherited from a parent `B' of `C' if and only if the
     following conditions are satisfied.

        1 No effective feature of `C' other than  `f'  and
          `g' has the same final name.

        2 The signature of `g' conforms to  the  signature
          of `f'.

        3 If `g' is a routine, its Precondition,  if  any,
          begins with require else (not just require), and
          its Postcondition, if any,  begins  with  ensure
          then (not just ensure).

        4 If the redeclaration is a  redefinition  (rather
          than an effecting) the Redefine subclause of the
          Parent part for `B' lists the final name of  `f'
          in its Feature_list.

        5 If `f' is inherited as effective,  then  `g'  is
          also effective.

        6 If `f' is an attribute, `g' is an attribute, `f'
          and  `g'  are both variable, and their types are
          either both expanded or both non-expanded.

        8 (ISE Eiffel temporary limitation)  For  every 
          element  `a'  of the signature of `f', if `b' is
          the  corresponding  signature  element  in  `g', 
          the  types  of  `a'  and  `b'  are  either  both 
          expanded  or both non-expanded.