NICE-ESG-Libs Digest        Fri, 23 Feb 96       Volume 2 : Issue  19 

Today's Topics:
            fwd: [zenger@ira.uka.de] 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: Fri, 23 Feb 96 06:53:48 EST
From: tynor (Steve Tynor)
Subject: fwd: [zenger@ira.uka.de] strip and ARRAY [ANY]
To: nice-esg-libs

------- start of forwarded message (RFC 934 encapsulation) -------
From: zenger@ira.uka.de (Christoph Zenger)
To: Steve.Tynor@atlanta.twr.com
Subject: strip and ARRAY [ANY]
Date: Fri, 23 Feb 96 11:09:29 +0100


Hi Steve,

> 	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

> Then we can rewrite the example postcondition as:
> 
> 	   ...
> 	ensure
> 	   strip(x).items_are_equal(old strip(x))
> 	end
> 
> and it "does the right thing".

The intuitive semantics of equal (o1.strip (x), o2.strip (x))
is that o1 and o2 are almost equal, they differ only on the
attribute x. This is informal for what IMHO the semantics of strip
should try to formalize.
You realized, that this is not the case for expanded attributes and
suggested to use items_are_equal instead of equal.

With your proposal of items_are_equal, there might be
s := clone (s) in the middle of foo's body, which isn't prohibited
by your new ensure clause, though it is prohibited by the old.
 
In general there are expanded attributes, that should be compared
with equal and unexpanded attributes, which should be compared
with =. We cannot come up with a special ..._equal feature for
every combination. IMO strip should be subject to discussion,
but this is rather a language issue.

items_are_equal seems to me a good addition to the standard,
because it is a practical solution to the strip problem, the
s := clone (s) being a minor nuisance.

Regards,
Christoph

[You may forward this or parts of it to the list, if you think it
appropriate]
- -------------------------------------------------------
Christoph Zenger              e-mail: zenger@ira.uka.de
IAKS, Informatik Uni Karlsruhe 
http://iaks-www.ira.uka.de/iaks-calmet/chris/chris.html


------- end -------