# NUMERIC (interface)

## Contents

## Class Interface

note description: "Objects to which numerical operations are applicable"; note: "The model is that of a ring with identity." deferred class interface NUMERIC feature -- Access one: like Current -- Neutral element for "*" and "/" deferred ensure Result_exists: Result /= Void zero: like Current -- Neutral element for "+" and "-" deferred ensure Result_exists: Result /= Void feature -- Status report divisible (other: like Current): BOOLEAN -- May current object be divided by other? require other_exists: other /= Void deferred exponentiable (other: NUMERIC): BOOLEAN -- May current object be elevated to the power other? require other_exists: other /= Void deferred is_special_case: BOOLEAN -- Is current object a special case regarding numeric operations? -- Special cases are cases where normal mathematical rules don't -- apply. Mostly this happens because of the binary represantation -- of the numeric. deferred feature -- Basic operations infix "+" (other: like Current): like Current -- Sum with other (commutative). require other_exists: other /= Void deferred ensure result_exists: Result /= Void; commutative: equal (Result, other + Current) infix "-" (other: like Current): like Current -- Result of subtracting other require other_exists: other /= Void deferred ensure result_exists: Result /= Void infix "*" (other: like Current): like Current -- Product by other require other_exists: other /= Void deferred ensure result_exists: Result /= Void infix "/" (other: like Current): like Current -- Division by other require other_exists: other /= Void; good_divisor: divisible (other) deferred ensure result_exists: Result /= Void infix "^" (other: NUMERIC): NUMERIC -- Current object to the power other require other_exists: other /= Void; good_exponent: exponentiable (other) deferred ensure result_exists: Result /= Void prefix "+": like Current -- Unary plus deferred ensure result_exists: Result /= Void prefix "-": like Current -- Unary minus deferred ensure result_exists: Result /= Void invariant 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: divisible not is_special_case implies divisible (Current) implies equal (Current / Current, one)

## Changes to ELKS 95

new features:

- is_special_case

changed invariants:

- all