INTEGER (interface) - Revision history

Conaclos: syntax and feature names updated

2013-04-26T21:43:15Z

syntax and feature names updated

Conaclos: syntax updated

2013-04-26T21:27:25Z

syntax updated

Juliant: /* Changes to ELKS 95 */

2006-11-22T19:18:13Z

‎Changes to ELKS 95

Juliant at 18:57, 22 November 2006

2006-11-22T18:57:42Z

Juliant at 18:54, 22 November 2006

2006-11-22T18:54:23Z

Juliant at 18:47, 22 November 2006

2006-11-22T18:47:54Z

Juliant at 18:46, 22 November 2006

2006-11-22T18:46:16Z

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

@@ Line 57: / Line 57: @@
 feature -- Comparison
-   infix "<" (other: like Current): BOOLEAN
+   is_less alias "<" (other: like Current): BOOLEAN
        -- Is other greater than current integer?
        -- (From COMPARABLE.)
@@ Line 65: / Line 65: @@
        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?
        -- (From COMPARABLE.)
@@ Line 73: / Line 73: @@
        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?
        -- (From COMPARABLE.)
@@ Line 81: / Line 81: @@
        definition: Result = (other <= Current)
-   infix ">" (other: like Current): BOOLEAN
+   is_greater alias ">" (other: like Current): BOOLEAN
        -- Is current object greater than other?
        -- (From COMPARABLE.)
@@ Line 152: / Line 152: @@
        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
        -- (From NUMERIC.)
@@ Line 158: / Line 158: @@
        other_exists: other /= Void
-   infix "+" (other: like Current): like Current
+   plus alias "+" (other: like Current): like Current
        -- Sum with other
        -- (From NUMERIC.)
@@ Line 175: / Line 175: @@
        result_exists: Result /= Void
-   infix "/" (other: like Current): REAL_64
+   quotient alias "/" (other: like Current): REAL_64
        -- Division by other
      require
@@ Line 187: / Line 187: @@
        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
        -- (From "/" in NUMERIC.)
@@ Line 196: / Line 196: @@
        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
      require
@@ Line 204: / Line 204: @@
        result_exists: Result /= Void
-   infix "^" (other: NUMERIC): REAL_64
+   power alias "^" (other: NUMERIC): REAL_64
        -- Integer power of Current by other
        -- (From NUMERIC.)
@@ Line 213: / Line 213: @@
        result_exists: Result /= Void
-   prefix "+": like Current
+   identity alias "+": like Current
        -- Unary plus
        -- (From NUMERIC.)
@@ Line 219: / Line 219: @@
        result_exists: Result /= Void
-   prefix "-": like Current
+   opposite alias "-": like Current
        -- Unary minus
        -- (From NUMERIC.)
@@ Line 233: / Line 233: @@
 invariant
-   sign_times_abs: not is_special_case implies equal (sign * abs, Current)
+   sign_times_abs: sign * abs = item
      -- From COMPARABLE

@@ Line 5: / Line 5: @@
 <code>[eiffel,N]
-indexing
+note
    description: "Integer values"
@@ Line 20: / Line 20: @@
 feature -- Access
-   hash_code: INTEGER is
+   hash_code: INTEGER
        -- Hash code value
        -- (From HASHABLE.)

@@ Line 251: / Line 251: @@
 new features:
 * is_special_case
 changed feature contracts:

@@ Line 141: / Line 141: @@
        -- Is current object a special case regarding numeric operations?
        -- (From NUMERIC.)
-     ensure
+     ensure then
        min_value_is_special: Result implies Current = min_value

@@ Line 44: / Line 44: @@
        Result_exists: Result /= Void;
        value: Result = 0
 feature -- Comparison
@@ Line 131: / Line 141: @@
        -- Is current object a special case regarding numeric operations?
        -- (From NUMERIC.)
 feature -- Basic operations