PR# 18947 [RJ] INTEGER_32_REF.plus - post condition commutative

Recently I turned on post-conditions in Eiffel Base and got a failure in INTEGER_32_REF.plus.  Although the argument is supposed to be 'like Current' I passed an INTEGER.  The post condition is inherited from NUMERIC:

	commutative: Result ~ (other + Current)

I believe this fails because 'Result' is an INTEGER_32_REF but "other + Current" is an INTEGER.  I suppose this is a CAT-call but it was pretty easy to do and it would be a shame to have to create a REF just to add 1.  As usual, I have some ideas.

Solution 1.  Introduce 'item' in NUMERIC (defaults to Current).  Redefine it in each of the *_REF classes (dang, it's built_in).  Change the post-condition to:
 
	commutative: Result.item ~ (other + Current).item

Solution 2.  Introduce 'to_ref' in NUMERIC (defaults to Current).  Redefine it in each of the *_REF classes.  Change the post-condition to:

	commutative: Result.to_ref ~ (other + Current).to_ref

Solution 3.  Introduce a safe comparison feature in NUMERIC instead of tilde.  It would essentially do what I'm trying to do in solutions 1 and 2.

Solution 4.  Introduce a feature in ANY that does what tilde does but will first attempt to 'convert'.

Randy

Approximate code (not actually tested):

local
   l_int_ref: INTEGER_32_REF
do
   create l_int_ref
   l_int_ref.plus(1).do_nothing
end

Below is the class which caused the initial problem (since fixed).  I suppose we could use CELL[INTEGER] instead of INTEGER_REF.

I'm not sure that this is extremely important.  I merely brought it up because it seems like a wart on the language.

   Randy

class
	ELOG_THREAD_SAFE_AUTO_INCREMENTER

feature -- Basic operations

	next_integer: INTEGER
			--|
		do
			auto_incrementer_mutex.lock
			Result := next_int
			next_int.set_item (next_int.item + 1)
--	next_int.set_item (next_int + 1)     -- Old code.
			auto_incrementer_mutex.unlock
		end

feature {NONE} -- Implementation

	auto_incrementer_mutex: ELOG_MUTEX
			-- Protects next_int
		indexing
			once_status: global
		once
			create Result.make
		end

	next_int: INTEGER_REF
			--|
		indexing
			once_status: global
		once
			create Result
		end

end

Another solution for the time being would be to have `plus (other: INTEGER): INTEGER' in INTEGER_32_REF. Turns out that today, the _REF classes are useless because one can pass an INTEGER to ANY and keep the type INTEGER. It is quite unlike the old days when passing an INTEGER to ANY would magically create an INTEGER_REF.

What is the scenario where you are still using INTEGER_32_REF?