NICE-ESG-Libs Digest        Thu, 22 Feb 96       Volume 2 : Issue  16 

Today's Topics:
                         strip and ARRAY[ANY]


  NICE Eiffel Standards Group -- Library Committee Mailing List

  To post to list:
     NICE-ESG-Libs@atlanta.twr.com
  To send mail to the Chairman of the committee:
     NICE-ESG-Libs-chair@atlanta.twr.com
  Administrative matters (sign up, unsubscribe, mail problems, etc):
     NICE-ESG-Libs-request@atlanta.twr.com

 
Date: Thu, 22 Feb 96 13:20:19 EST
From: tynor (Steve Tynor)
Subject: strip and ARRAY[ANY]
To: nice-esg-libs, eiffel@swissoft.h.provi.de (Michael Schweitzer)

Submitted for discussion.  Suppose I have the following class:

	class A 
	feature
	   s : STRING;
	   x, y : INTEGER;

	   foo is
		 -- This feature is not supposed to change anything but `x'
	      do
		...
	      ensure
		 -- all the fields of Current except `x' should be unchanged:
		 equal (strip(x), old strip(x));
	      end
	end

The postcondition can never succeed, even if Current is completely
unchanged! (yet this is the canonical way that strip is used in the
examples of ETL).

Why, you ask?  Because strip creates an ARRAY[ANY] (ETL pg. 397). 
Therefore instead of putting `y' into an array, `y's reference
equivalent (an INTEGER_REF) is put in the array. So, the array contains
a reference to a STRING and a reference to an INTEGER_REF.  But the 
"old strip" contains a different INTEGER_REF (one created by evaluating
Current before executing the body of the routine). Since `equal' is
defined in terms if `is_equal', it's the equivalent of saying: 

		 strip(x).is_equal (old strip(x))

But ARRAY's `is_equal' is defined (and correctly so, in my opinion) to
simply check whether "for all i, item(i) = other.item(i)".  That's
_reference_equality_ for ARRAY[ANY]. So, the two strip expressions will
never be equal. [Side note: as far as I'm aware, all existing
implementations implement ARRAY:is_equal in this manner, and it's in
fact spelled out to have these semantics in Jim McKim's recent touch-up
of the ARRAY class. I don't expect any argument that this is the correct
semantics for the feature (but you may suprise me...)].

The only solution that makes sense is to add a new feature to ARRAY
which checks `is_equal' on each element instead of using `='. That is, 

	items_are_equal (other : like Current) 
	      -- Is each item in Current `is_equal' to the corresponding
	      -- item in `other'?
           require
	       other_not_void: other /= Void;
	   ensure
	      -- for all i, 
	      --    ((item(i) = Void or other.item(i) = Void)
	      --      implies (item(i) = Void and other.item(i) = Void))
              --    or else item(i).is_equal(other.item(i))

Then we can rewrite the example postcondition as:

	   ...
	ensure
	   strip(x).items_are_equal(old strip(x))
	end

and it "does the right thing".

If you agree, then I will write up a proposal for adding a new
`items_are_equal' standard feature to ARRAY.  (Off the top of my head,
I can think of several alternative names: `items_are_equal',
`elements_are_equal', `is_equal_items', `is_equal_elements',
`equal_items' `same_items'.  I prefer `items_are_equal' or
`equal_items' since they are the most naturally English phrases.
`same_items' is not descriptive enough since it's not clear from the
name that `same_items' is any different than `is_equal'.

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Llamas are larger than frogs.

Steve Tynor		Internet: Steve.Tynor@atlanta.twr.com
Tower Technology 	WWW:      http://www.twr.com/