Re: Comparing DS_HASH_TABLE objects

>>>>> "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).
-- 
Colin Adams
Preston Lancashire


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

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/