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

class interface
	PLUS_ONE

create 
	make

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
		ensure
				Result = {ITERABLE_ARITHMETIC [INTEGER_32]}.sum_array (a, agent term (?, ?, ?))
-- Unable to show all postconditions!

			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
			
		end -- class PLUS_ONE

Generated by ISE EiffelStudio