note description: "[ Detect Integer Overflow debug ToDo: Pre/Post-conditions end ToDo: multiply and divide ]" author: "" date: "$Date$" revision: "$Revision$" class interface INTEGER_OVERFLOW create default_create feature Max_int: INTEGER_64 Min_int: INTEGER_64 safe_plus (left, right: INTEGER_64): BOOLEAN ensure right >= 0 implies Result = (left <= Max_int - right) right <= 0 implies Result = (left >= Min_int - right) safe_minus (left, right: INTEGER_64): BOOLEAN ensure right >= 0 implies Result = (left >= Min_int + right) right <= 0 implies Result = (left <= Max_int + right) end -- class INTEGER_OVERFLOW
Generated by ISE EiffelStudio