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