Re: Comparing DS_HASH_TABLE objects

Colin Paul Adams wrote:
>>>>>> "Helmut" == Helmut Brandl <[email protected]> writes:
> 
>     Helmut> For me an agent is an object which represents a feature
>     Helmut> and has some open and closed arguments. Two agents shall
>     Helmut> be equal if they represent the same feature, have the same
>     Helmut> open and closed argument positions and all closed
>     Helmut> arguments are equal (since they are contained in the
>     Helmut> agent).
> 
>     Helmut> Do your agents behave differently if you use "~" to
>     Helmut> compare two agents?
> 
> I don't know.
> 
>     >> Currently we have {FUNCTION}.is_equal defined which gives you a
>     >> sort of partial test for equality of functions. This strikes me
>     >> as a little odd.
>     >> 
>     >> I use {ROUTINE}.is_equal in postconditions for specifying the
>     >> semantics of Vision2 actions (such as pushing a button). But
>     >> this is a little overly restrictive (you ought to be able to
>     >> redefine an action to use any agent equivalent to the one
>     >> specified, but this requires a theorem prover, I think).
> 
>     Helmut> I don't understand what you mean by that?
> 
> Take these two functions as an example:
> 
>  double_1 (a_value: INTEGER): INTEGER is
>    -- Double `a_value'
>  do
>    Result := 2 * a_value
>  ensure
>   definition: Result = 2 * a_value
>  end
> 
>  double_2 (a_value: INTEGER): INTEGER is
>    -- Double `a_value'
>  do
>    Result := 2 * a_value
>  ensure
>   definition: Result = 2 * a_value
>  end
> 
> These represent the same mathematical function. But agent
> (double_1).is_equal (agent double_2) returns False (whereas agent
> (double_1).is_equal (agent double_1) returns True).
> 
> Take this third function:
> 
>  double_3 (a_value: INTEGER): INTEGER is
>    -- Double `a_value'
>  do
>    Result := a_value * a_value
>  ensure
>   definition: Result = a_value * a_value
>  end
> 
> this represents a mathematical function equivalent to the first
> two. Again, agent
> (double_1).is_equal (agent double_3) returns False.
> 
> It would require a (fairly simple, in this case) theorem prover to automatically
> determine the two agents as being equivalent (given the same input,
> they always return the same output).
> 
> So if I were to specify a postcondition that involved agent (double_1)
> somewhere, and a descendant class redefines the routine to use agent
> double_3 instead, the postcondition will fail (even though the
> semantics are actually preserved).

Ok, now I understand what you mean. But I guess that the agents
representing `double_1' and `double_3' cannot be equal, because they
represent different features. The postcondition alone does not guarantee
equal semantics (in that simple case yes, but generally no, since there
is no guarantee that the postcondition is complete).




------------------------------------

To Post a message, send it to:   [email protected]
To Unsubscribe, send a blank message to: [email protected]! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/gobo-eiffel/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/gobo-eiffel/join
    (Yahoo! ID required)

<*> To change settings via email:
    mailto:[email protected] 
    mailto:[email protected]

<*> To unsubscribe from this group, send an email to:
    [email protected]

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/