note
	description: "Just utils"
	license: "[
				Copyright (C) 2021 Ilgiz Mustafin
		
				This program is free software; you can redistribute it and/or modify
				it under the terms of the GNU General Public License as published by
				the Free Software Foundation; either version 2 of the License, or
				(at your option) any later version.
		
				This program is distributed in the hope that it will be useful,
				but WITHOUT ANY WARRANTY; without even the implied warranty of
				MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
				GNU General Public License for more details.
		
				You should have received a copy of the GNU General Public License along
				with this program; if not, write to the Free Software Foundation, Inc.,
				51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
	]"

class 
	UTILS [G]

create 
	default_create

feature 

	first_index (ar: ARRAY [G]; v: G): INTEGER_32
			-- First index of item i = v in ar or ar.upper + 1 if not found
		do
			from
				Result := ar.lower
			until
				Result > ar.upper or else ar [Result] = v
			loop
				Result := Result + 1
			end
		ensure
				Result > ar.upper implies across
					ar as ari
				all
					ari.item /= v
				end
				Result /= ar.upper implies ar [Result] = v and across
					ar.subarray (ar.lower, Result - 1) as ari2
				all
					ari2.item /= v
				end
			instance_free: class
		end

	all_different (ar: ARRAY [G]): BOOLEAN
		local
			i: INTEGER_32
		do
			Result := True
			from
				i := ar.lower
			until
				not Result or i > ar.upper
			loop
				Result := across
					ar.subarray (i + 1, ar.upper) as it
				all
					it.item /= Void implies it.item /= ar [i]
				end
				i := i + 1
			end
		ensure
			instance_free: class
			true_for_empty: ar.count = 0 implies Result
		end

	invariant_ref_array (ar: ARRAY [G]; count: INTEGER_32): BOOLEAN
			-- Lower is 0, count is correct, all references are different
		local
			i: INTEGER_32
		do
			Result := ar.lower = 0 and ar.count = count and all_different (ar)
		ensure
			lower_not_zero_gives_false: ar.lower /= 0 implies Result = False
			incorrect_count_gives_false: ar.count /= count implies Result = False
			not_all_different_gives_false: not all_different (ar) implies Result = False
			instance_free: class
		end
	
end -- class UTILS

Generated by ISE EiffelStudio