/[eiffelstudio]/FreeELKS/trunk/library/kernel/special.e
ViewVC logotype

Diff of /FreeELKS/trunk/library/kernel/special.e

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 91476 by ericb, Fri Mar 3 10:19:32 2006 UTC revision 91477 by ericb, Sun Jan 14 09:47:13 2007 UTC
# Line 1  Line 1 
1  indexing  indexing
2          description: "[          description: "[
3                  Special objects: homogeneous sequences of values,                  Special objects: homogeneous sequences of values,
4                  used to represent arrays and strings                  used to represent arrays and strings
5                  ]"                  ]"
6          library: "Free implementation of ELKS library"          library: "Free implementation of ELKS library"
# Line 113  feature -- Access Line 113  feature -- Access
113                          is_dotnet: {PLATFORM}.is_dotnet                          is_dotnet: {PLATFORM}.is_dotnet
114                  do                  do
115                  end                  end
116                    
117  feature -- Measurement  feature -- Measurement
118    
119          lower: INTEGER is 0          lower: INTEGER is 0
# Line 125  feature -- Measurement Line 125  feature -- Measurement
125                          Result := count - 1                          Result := count - 1
126                  end                  end
127    
128          frozen count: INTEGER is          frozen count: INTEGER is
129                          -- Count of the special area                          -- Count of the special area
130                  external                  external
131                          "built_in"                          "built_in"
# Line 222  feature -- Element change Line 222  feature -- Element change
222                          end                          end
223                  end                  end
224    
225          frozen copy_data (other: like Current; source_index, destination_index, n: INTEGER) is          frozen copy_data (other: SPECIAL [T]; source_index, destination_index, n: INTEGER) is
226                          -- Copy `n' elements of `other' from `source_index' position to Current at                          -- Copy `n' elements of `other' from `source_index' position to Current at
227                          -- `destination_index'. Other elements of Current remain unchanged.                          -- `destination_index'. Other elements of Current remain unchanged.
228                  require                  require
# Line 232  feature -- Element change Line 232  feature -- Element change
232                          n_non_negative: n >= 0                          n_non_negative: n >= 0
233                          n_is_small_enough_for_source: source_index + n <= other.count                          n_is_small_enough_for_source: source_index + n <= other.count
234                          n_is_small_enough_for_destination: destination_index + n <= count                          n_is_small_enough_for_destination: destination_index + n <= count
235                            same_type: same_type (other)
236                  local                  local
237                          i, j, nb: INTEGER                          i, j, nb: INTEGER
238                  do                  do
# Line 361  feature -- Resizing Line 362  feature -- Resizing
362                          -- Create a copy of Current with a count of `n'.                          -- Create a copy of Current with a count of `n'.
363                  require                  require
364                          valid_new_count: n > count                          valid_new_count: n > count
                 local  
                         i, nb: INTEGER  
365                  do                  do
366                          create Result.make (n)                          create Result.make (n)
367                          from                          Result.copy_data (Current, 0, 0, count)
                                 nb := count  
                         invariant  
                                 i >= 0 and i <= nb  
                         variant  
                                 nb - i  
                         until  
                                 i = nb  
                         loop  
                                 Result.put (item (i), i)  
                                 i := i + 1  
                         end  
368                  ensure                  ensure
369                          Result_not_void: Result /= Void                          Result_not_void: Result /= Void
370                          Result_different_from_current: Result /= Current                          Result_different_from_current: Result /= Current

Legend:
Removed from v.91476  
changed lines
  Added in v.91477

  ViewVC Help
Powered by ViewVC 1.1.23