Dear group members,
I am sorry for the long silence, new project starting, you know how it
Nonetheless, we are still in our "short" visit to ANY with the focus
on looking at comparison. I read through the old postings and hope I
got all the main points. To get the discussion going again, let me sum
We where working on COMPARABLE and discovered the problem that
argument order inversion for operators does not work when the 'like
Current' argument is actually of a proper child type. This induced
catcalls in the postcondition. One approach to this we discussed was
replacing 'like Current' in the arguments of the equality tests by
'ANY', however we found out that while this may be desirable, it does
not remove the catcalls.
Franck told us in message 2745 that 'like Current' may now be
redefined to a specific type (ECMA). This removes the reason for
changing the second argument in the comparison features to 'ANY'.
The fundamental reason for the catcalls is that an operator is
selected from the first argument (i.e. is a method of the first
argument), while mathematically it should rather be something like a
method of the least common ancestor of both arguments. (This might
lead to other problems, e.g. that the least common ancestor need not
be unique, but we do not have it anyway so no need to think about it.)
As a consequence everything involving a change of argument order (like
symmetry properties, order in reverse,...) is not implementable when
the arguments are not of the same type.
As a consequence we do not need to specify properties like "symmetry"
for these cases, since they do not arise anyway!
Cyril made the point that requiring that equality can only happen for
objects of the same type, is too strong (posting 2740). I agree with
The idea would now be that rather than to forbid different argument
types, make sure anybody sees that the case is not covered in the
specification. This would get rid of the catcalls as well, I think.
(Incidentally that is what SE does currently.)
For 'is_equal' this would look as follows:
is_equal (other: like Current): BOOLEAN
-- Is `other' attached to an object considered equal
-- to current object?
other_not_void: other /= Void
limited_symmetry: same_type(other) implies
(Result implies other.is_equal (Current))
Dominique made some good points in posting 2750 which would result in
a different treatment for the 'standard_'-features.
'standard'-equality should still require 'same_type'. (One reason
somebody may want to have 'standard_equal' true for two instances but
'equal' untrue would be when memory address also has an impact on the
equality relation.) With this 'standard_is_equal' would just stay as
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?
other_not_void: other /= Void
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
A problem is that 'is_equal' is in the postcondition of 'copy'
(mentioned by several people). Maybe add a 'same_type' postcondition
to 'copy' to ensure intuitive semantics?
P.S.: I deleted messages 2760, 2762 and 2763 because they where spam.
Arno Wagner, Communication Systems Group, ETH Zuerich, wagner@...
GnuPG: ID: 1E25338F FP: 0C30 5782 9D93 F785 E79C 0296 797F 6B50 1E25 338F
For every complex problem there is an answer that is clear, simple,
and wrong. -- H L Mencken