INTEGER (interface)
Revision as of 13:43, 26 April 2013 by Conaclos (Talk | contribs) (syntax and feature names updated)
Contents
Class Interface
note description: "Integer values" expanded class interface INTEGER inherit NUMERIC COMPARABLE HASHABLE feature -- Access hash_code: INTEGER -- 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 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 is_less alias "<" (other: like Current): BOOLEAN -- Is other greater than current integer? -- (From COMPARABLE.) require other_exists: other /= Void ensure asymmetric: Result implies not (other < Current) is_less_equal alias "<=" (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); is_greater_equal alias ">=" (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) is_greater alias ">" (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.) ensure then min_value_is_special: Result implies Current = min_value 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) product alias "*" (other: like Current): like Current -- Product by other -- (From NUMERIC.) require other_exists: other /= Void plus alias "+" (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 quotient alias "/" (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 integer_quotient alias "//" (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) integer_remainder alias "\\" (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 power alias "^" (other: NUMERIC): REAL_64 -- Integer power of Current by other -- (From NUMERIC.) require other_exists: other /= Void; good_exponent: exponentiable (other) ensure result_exists: Result /= Void identity alias "+": like Current -- Unary plus -- (From NUMERIC.) ensure result_exists: Result /= Void opposite alias "-": 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: sign * abs = item -- 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
Changes to ELKS 95
new features:
- is_special_case
- max_value
- min_value
changed feature contracts:
- abs
- infix "/"
changed invariants:
- sign_times_abs