INTEGER (interface) - Revision history

Conaclos: syntax and feature names updated

2013-04-26T21:43:15Z

syntax and feature names updated

← Older revision		Revision as of 21:43, 26 April 2013
Line 57:		Line 57:
	feature -- Comparison		feature -- Comparison

	~~infix~~ "<" (other: like Current): BOOLEAN		is_less alias "<" (other: like Current): BOOLEAN
	-- Is other greater than current integer?		-- Is other greater than current integer?
	-- (From COMPARABLE.)		-- (From COMPARABLE.)
Line 65:		Line 65:
	asymmetric: Result implies not (other < Current)		asymmetric: Result implies not (other < Current)

	~~infix~~ "<=" (other: like Current): BOOLEAN		is_less_equal alias "<=" (other: like Current): BOOLEAN
	-- Is current object less than or equal to other?		-- Is current object less than or equal to other?
	-- (From COMPARABLE.)		-- (From COMPARABLE.)
Line 73:		Line 73:
	definition: Result = (Current < other) or is_equal (other);		definition: Result = (Current < other) or is_equal (other);

	~~infix~~ ">=" (other: like Current): BOOLEAN		is_greater_equal alias ">=" (other: like Current): BOOLEAN
	-- Is current object greater than or equal to other?		-- Is current object greater than or equal to other?
	-- (From COMPARABLE.)		-- (From COMPARABLE.)
Line 81:		Line 81:
	definition: Result = (other <= Current)		definition: Result = (other <= Current)

	~~infix~~ ">" (other: like Current): BOOLEAN		is_greater alias ">" (other: like Current): BOOLEAN
	-- Is current object greater than other?		-- Is current object greater than other?
	-- (From COMPARABLE.)		-- (From COMPARABLE.)
Line 152:		Line 152:
	same_absolute_value: not is_special_case implies (Result = Current) or (Result = - Current)		same_absolute_value: not is_special_case implies (Result = Current) or (Result = - Current)

	~~infix~~ "*" (other: like Current): like Current		product alias "*" (other: like Current): like Current
	-- Product by other		-- Product by other
	-- (From NUMERIC.)		-- (From NUMERIC.)
Line 158:		Line 158:
	other_exists: other /= Void		other_exists: other /= Void

	~~infix~~ "+" (other: like Current): like Current		plus alias "+" (other: like Current): like Current
	-- Sum with other		-- Sum with other
	-- (From NUMERIC.)		-- (From NUMERIC.)
Line 175:		Line 175:
	result_exists: Result /= Void		result_exists: Result /= Void

	~~infix~~ "/" (other: like Current): REAL_64		quotient alias "/" (other: like Current): REAL_64
	-- Division by other		-- Division by other
	require		require
Line 187:		Line 187:
	result_correct: not divisble (other) implies Result.is_special_case		result_correct: not divisble (other) implies Result.is_special_case

	~~infix~~ "//" (other: like Current): like Current		integer_quotient alias "//" (other: like Current): like Current
	-- Integer division of Current by other		-- Integer division of Current by other
	-- (From "/" in NUMERIC.)		-- (From "/" in NUMERIC.)
Line 196:		Line 196:
	result_exists: divisible (other)		result_exists: divisible (other)

	~~infix~~ "\\" (other: like Current): like Current		integer_remainder alias "\\" (other: like Current): like Current
	-- Remainder of the integer division of Current by other		-- Remainder of the integer division of Current by other
	require		require
Line 204:		Line 204:
	result_exists: Result /= Void		result_exists: Result /= Void

	~~infix~~ "^" (other: NUMERIC): REAL_64		power alias "^" (other: NUMERIC): REAL_64
	-- Integer power of Current by other		-- Integer power of Current by other
	-- (From NUMERIC.)		-- (From NUMERIC.)
Line 213:		Line 213:
	result_exists: Result /= Void		result_exists: Result /= Void

	~~prefix~~ "+": like Current		identity alias "+": like Current
	-- Unary plus		-- Unary plus
	-- (From NUMERIC.)		-- (From NUMERIC.)
Line 219:		Line 219:
	result_exists: Result /= Void		result_exists: Result /= Void

	~~prefix~~ "-": like Current		opposite alias "-": like Current
	-- Unary minus		-- Unary minus
	-- (From NUMERIC.)		-- (From NUMERIC.)
Line 233:		Line 233:
	invariant		invariant

	sign_times_abs: ~~not is_special_case implies equal (~~sign * abs~~, Current)~~		sign_times_abs: sign * abs = item

	-- From COMPARABLE		-- From COMPARABLE

Conaclos: syntax updated

2013-04-26T21:27:25Z

syntax updated

← Older revision		Revision as of 21:27, 26 April 2013
Line 5:		Line 5:

	<code>[eiffel,N]		<code>[eiffel,N]
	~~indexing~~		note
	description: "Integer values"		description: "Integer values"

Line 20:		Line 20:
	feature -- Access		feature -- Access

	hash_code: INTEGER is		hash_code: INTEGER
	-- Hash code value		-- Hash code value
	-- (From HASHABLE.)		-- (From HASHABLE.)

Juliant: /* Changes to ELKS 95 */

2006-11-22T19:18:13Z

Changes to ELKS 95

← Older revision		Revision as of 19:18, 22 November 2006
Line 251:		Line 251:
	new features:		new features:
	* is_special_case		* is_special_case
			* max_value
			* min_value

	changed feature contracts:		changed feature contracts:

Juliant at 18:57, 22 November 2006

2006-11-22T18:57:42Z

← Older revision		Revision as of 18:57, 22 November 2006
Line 204:		Line 204:
	result_exists: Result /= Void		result_exists: Result /= Void

	infix "^" (other: NUMERIC): ~~DOUBLE~~		infix "^" (other: NUMERIC): REAL_64
	-- Integer power of Current by other		-- Integer power of Current by other
	-- (From NUMERIC.)		-- (From NUMERIC.)
Line 233:		Line 233:
	invariant		invariant

	sign_times_abs: equal (sign * abs, Current)		sign_times_abs: not is_special_case implies equal (sign * abs, Current)

	-- From COMPARABLE		-- From COMPARABLE
Line 255:		Line 255:
	* abs		* abs
	* infix "/"		* infix "/"

			changed invariants:
			* sign_times_abs

Juliant at 18:54, 22 November 2006

2006-11-22T18:54:23Z

← Older revision		Revision as of 18:54, 22 November 2006
Line 252:		Line 252:
	* is_special_case		* is_special_case

	changed contracts:		changed feature contracts:
	* abs		* abs
			* infix "/"

Juliant at 18:47, 22 November 2006

2006-11-22T18:47:54Z

← Older revision		Revision as of 18:47, 22 November 2006
Line 141:		Line 141:
	-- Is current object a special case regarding numeric operations?		-- Is current object a special case regarding numeric operations?
	-- (From NUMERIC.)		-- (From NUMERIC.)
	ensure		ensure then
	min_value_is_special: Result implies Current = min_value		min_value_is_special: Result implies Current = min_value

Juliant at 18:46, 22 November 2006

2006-11-22T18:46:16Z

← Older revision		Revision as of 18:46, 22 November 2006
Line 44:		Line 44:
	Result_exists: Result /= Void;		Result_exists: Result /= Void;
	value: Result = 0		value: Result = 0

			max_value: like Current
			-- Maximal integer value
			ensure
			Result_exists: Result /= Void;

			min_value: like Current
			-- Minimal integer value
			ensure
			Result_exists: Result /= Void;

	feature -- Comparison		feature -- Comparison
Line 131:		Line 141:
	-- Is current object a special case regarding numeric operations?		-- Is current object a special case regarding numeric operations?
	-- (From NUMERIC.)		-- (From NUMERIC.)
			ensure
			min_value_is_special: Result implies Current = min_value

	feature -- Basic operations		feature -- Basic operations

Juliant at 18:44, 22 November 2006

2006-11-22T18:44:25Z

New page

[[Category:ELKS]]
__TOC__

==Class Interface==

<code>[eiffel,N]
indexing
description: "Integer values"

expanded class interface INTEGER

inherit

NUMERIC

COMPARABLE

HASHABLE

feature -- Access

hash_code: INTEGER is
-- Hash code value
-- (From HASHABLE.)
ensure
good_hash_value: Result >= 0

one: like Current
-- Neutral element for "*" and "/"
-- (From NUMERIC.)
ensure
Result_exists: Result /= Void;
value: Result = 1

sign: INTEGER
-- Sign value (0, -1 or 1)
ensure
three_way: Result = three_way_comparison (zero)

zero: like Current
-- Neutral element for "+" and "-"
-- (From NUMERIC.)
ensure
Result_exists: Result /= Void;
value: Result = 0

feature -- Comparison

infix "<" (other: like Current): BOOLEAN
-- Is other greater than current integer?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
asymmetric: Result implies not (other < Current)

infix "<=" (other: like Current): BOOLEAN
-- Is current object less than or equal to other?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
definition: Result = (Current < other) or is_equal (other);

infix ">=" (other: like Current): BOOLEAN
-- Is current object greater than or equal to other?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
definition: Result = (other <= Current)

infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
definition: Result = (other < Current)

max (other: like Current): like Current
-- The greater of current object and other
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
current_if_not_smaller: (Current >= other) implies (Result = Current)
other_if_smaller: (Current < other) implies (Result = other)

min (other: like Current): like Current
-- The smaller of current object and other
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
current_if_not_greater: (Current <= other) implies (Result = Current)
other_if_greater: (Current > other) implies (Result = other)

three_way_comparison (other: like Current): INTEGER
-- If current object equal to other, 0; if smaller,
-- -1; if greater, 1.
-- (From COMPARABLE.)
require
other_exists: other /= Void
ensure
equal_zero: (Result = 0) = is_equal (other);
smaller: (Result = 1) = Current < other;
greater_positive: (Result = -1) = Current > other

feature -- Status report

divisible (other: like Current): BOOLEAN
-- May current object be divided by other?
-- (From NUMERIC.)
require
other_exists: other /= Void
ensure
value: Result = (other /= 0)

exponentiable (other: NUMERIC): BOOLEAN
-- May current object be elevated to the power other?
-- (From NUMERIC.)
require
other_exists: other /= Void
ensure
safe_values: (other.conforms_to (Current) or
(other.conforms_to (0.0) and (Current >= 0)))
implies Result

is_special_case: BOOLEAN
-- Is current object a special case regarding numeric operations?
-- (From NUMERIC.)

feature -- Basic operations

abs: like Current
-- Absolute value
ensure
non_negative: not is_special_case implies Result >= 0;
same_absolute_value: not is_special_case implies (Result = Current) or (Result = - Current)

infix "*" (other: like Current): like Current
-- Product by other
-- (From NUMERIC.)
require
other_exists: other /= Void

infix "+" (other: like Current): like Current
-- Sum with other
-- (From NUMERIC.)
require
other_exists: other /= Void
ensure
result_exists: Result /= Void;
commutative: equal (Result, other + Current)

infix "-" (other: like Current): like Current
-- Result of subtracting other
-- (From NUMERIC.)
require
other_exists: other /= Void
ensure
result_exists: Result /= Void

infix "/" (other: like Current): REAL_64
-- Division by other
require
other_exists: other /= Void;
good_divisor: divisible (other)
require else
other_exists: other /= Void
ensure
result_exists: Result /= Void
ensure then
result_correct: not divisble (other) implies Result.is_special_case

infix "//" (other: like Current): like Current
-- Integer division of Current by other
-- (From "/" in NUMERIC.)
require
other_exists: other /= Void;
good_divisor: divisible (other)
ensure
result_exists: divisible (other)

infix "\\" (other: like Current): like Current
-- Remainder of the integer division of Current by other
require
other_exists: other /= Void;
good_divisor: divisible (other)
ensure
result_exists: Result /= Void

infix "^" (other: NUMERIC): DOUBLE
-- Integer power of Current by other
-- (From NUMERIC.)
require
other_exists: other /= Void;
good_exponent: exponentiable (other)
ensure
result_exists: Result /= Void

prefix "+": like Current
-- Unary plus
-- (From NUMERIC.)
ensure
result_exists: Result /= Void

prefix "-": like Current
-- Unary minus
-- (From NUMERIC.)
ensure
result_exists: Result /= Void

feature -- Output

out: STRING
-- Printable representation of current object
-- (From GENERAL.)

invariant

sign_times_abs: equal (sign * abs, Current)

-- From COMPARABLE
irreflexive_comparison: not (Current < Current);

-- From NUMERIC
neutral_addition: not is_special_case implies equal (Current + zero, Current);
self_subtraction: not is_special_case implies equal (Current - Current, zero);
neutral_multiplication: not is_special_case implies equal (Current * one, Current);
self_division: not is_special_case implies divisible (Current) implies equal (Current / Current, one)

end
</code>

==Changes to ELKS 95==

new features:
* is_special_case

changed contracts:
* abs