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