Re: Precursor, symmetry of is_equal

On Feb 16, 2:19 pm, Roger Browne <r...@[EMAIL PROTECTED]
> wrote:
> Daniel F Moisset wrote:
> > So, my question is:
> >  * Is this a language gotcha?
>
> It's just a common-or-garden catcall, isn't it? Within the 'symmetric'
> postcondition (during evaluation of the precursor call), the call to
> "other.is_equal(Current)" is passing a PARENT as 'Current', whereas
> 'other' is a CHILD and is wanting to be passed another CHILD.

No, it is not a catcall. There are no instances of PARENT in my code
(I will atach a sample), in fact PARENT can be deferred. So there is
no place where some routine is getting something it does not expect.

I don't think it is a case of feature replication (I am using simple
inheritance), unless usage of "Precursor" qualifies as a form of
replication...

> > If you look at Bertrand's ETL3 drafts, you'll see that 'is_equal' is
now
> in some places declared with signature "is_equal(other: ?like Current)".
> That might make it typesafe but it won't make it work for Daniel's
> example.

My problem will also happen in ETL3 if I get it correctly.

Just to clarify, let me post some code. It crashes at least in SE 2.x.
If you have other compilers handy (I do not right now), I would like
to know what the results are:

deferred class PARENT

inherit
    ANY redefine is_equal end

feature

    a,b: STRING

    is_equal (other: like Current): BOOLEAN is
        do
            Result := a.is_equal (other.a) and b.is_equal (other.b)
        end

invariant
    a /= Void
    b /= Void

end


class CHILD

inherit
    PARENT redefine is_equal end

create
    make

feature

    make (a_a, a_b, a_c: STRING) is
        require
            a_a /= Void
            a_b /= Void
            a_c /= Void
        do
            a := a_a
            b := a_b
            c := a_c
        end

    c: STRING

    is_equal (other: like Current): BOOLEAN is
        do
            Result := Precursor (other)
            Result := Result and c.is_equal (other.c)
        end

invariant
    c /= Void

end

class MAIN

create make

feature

    make is
        local
            o1, o2: CHILD
            x: BOOLEAN
        do
            create o1.make_2 ("x", "y", "z")
            create o2.make_2 ("x", "y", "not z")
            x := o1.is_equal (o2)
            if x then print ("Yay!") end
        end

end


Regards,
   Daniel