NICE-ESG-Libs Digest        Fri,  9 Feb 96       Volume 1 : Issue 326 

Today's Topics:
                    Christine, let's start voting!
            Proposal RB-4: remove invariant 'valid_bounds'


  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, 9 Feb 1996 09:16:03 +0000
From: Roger Browne 
Subject: Christine, let's start voting!
To: nice-esg-libs@atlanta.twr.com

Christine,

It's now over a month since Steve Tynor requested a call for votes.

Let's at least have a vote on RB-1 (fix comment in HASHABLE), so
that we can then focus on finishing ARRAY.

Regards,
Roger
-- 
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK   | Ph 01772-687525
-- Everything Eiffel: compilers/libraries/publications | +44-1772-687525

 
Date: Fri, 9 Feb 1996 09:35:26 +0000
From: Roger Browne 
Subject: Proposal RB-4: remove invariant 'valid_bounds'
To: nice-esg-libs@atlanta.twr.com

This proposal aims to remove a redundant subclause from the invariant
of ARRAY, which currently reads:

   invariant
      consistent_size: count = upper - lower + 1; 
      nonnegative_count: count >= 0
      valid_bounds: lower <= upper + 1
      item_equals_at: -- for_all i, lower..upper (item( i ) = Current @ i)

The subclause 'valid_bounds' can readily be deduced from
'consistent_size' and 'nonnegative_count' (by substituting
'upper - lower + 1' for 'count' in 'nonnegative_count' and
rearranging). The subclause 'valid_bounds' adds no further
information to the invariant.

Regards,
Roger

=====

Tag:

  RB-4: remove invariant 'valid_bounds'

Class:

  ARRAY

Proposed Change:

  Amend proposal RB-2 (James McKim's ARRAY class) to remove the
  following line from the invariant:

      valid_bounds: lower <= upper + 1

Details:

  Amend proposal RB-2 to replace this invariant...

  invariant
    consistent_size: count = upper - lower + 1; 
    nonnegative_count: count >= 0
    valid_bounds: lower <= upper + 1
    item_equals_at: -- for_all i, lower..upper (item( i ) = Current @ i)

  ...by this invariant...

  invariant
    consistent_size: count = upper - lower + 1; 
    nonnegative_count: count >= 0
    item_equals_at: -- for_all i, lower..upper (item( i ) = Current @ i)

Rationale:

  I do not believe that it is desirable to have a redundant subclause
  in the invariant. It does nothing to aid clarity. (If redundant
  invariant subclauses are desirable, why stop at one? I can think
  of many more candidate redundant invariant subclauses :-)

  Also, although runtime assertion monitoring is not normally
  enabled for kernel classes, there is no reason to make
  it less efficient than it needs to be.

Migration strategy:

  There is no effect on existing code.

=====
-- 
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK   | Ph 01772-687525
-- Everything Eiffel: compilers/libraries/publications | +44-1772-687525