note
	description: "Summary description for {PLUSONE}."
	author: ""
	date: "$Date$"
	revision: "$Revision$"

class 
	PLUS_ONE

create 
	make

feature {NONE} 

	make (an_array: like a)
		do
			a := an_array
		end
	
feature 

	a: ARRAY [INTEGER_32]
			-- the array to be converted and incremented
			-- e.g. for <<8, 7, 4>> output 875

	val: INTEGER_32
			-- e.g. for array <<8, 7, 4>>,
			-- Result = (8*10^2 + 7*10^1 + 4*10^0) + 1
		require
				a.count >= 1
				across
					a as cr
				all
					0 <= cr.item and cr.item <= 9
				end
		local
			n, i, factor: INTEGER_32
		do
			from
				i := 1
				n := a.count
			until
				i > n
			loop
				check
						n - i >= 0
				end
				factor := (10 ^ (n - i).to_double).truncated_to_integer
				Result := Result + a [i] * factor
				i := i + 1
			end
			Result := Result + 1
		ensure
				Result = {ITERABLE_ARITHMETIC [INTEGER_32]}.sum_array (a, agent term (?, ?, ?))
-- Unable to show all postconditions!
end

			term (n: INTEGER_32; i: INTEGER_32; a_digit: INTEGER_32): INTEGER_32
					-- n: is the array count
					-- i: is the array index
					-- a_digit: is the array element
				do
					Result := a_digit * (10 ^ (n - i).to_double).truncated_to_integer
				end
			
		end -- class PLUS_ONE

Generated by ISE EiffelStudio