indexing description: "Objects to which numerical operations are applicable" note: "The model is that of a commutative ring." deferred class interface NUMERIC feature -- Access one: like Current -- Neutral element for "*" and "/" ensure result_exists: Result /= void zero: like Current -- Neutral element for "+" and "-" 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 exponentiable (other: NUMERIC): BOOLEAN -- May current object be elevated to the power other? require other_exists: other /= void feature -- Basic operations infix "*" (other: like Current): like Current -- Product by other require other_exists: other /= void ensure result_exists: Result /= void prefix "+ ": like Current -- Unary plus ensure result_exists: Result /= void infix "+" (other: like Current): like Current -- Sum with other (commutative). 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 require other_exists: other /= void ensure result_exists: Result /= void prefix "- ": like Current -- Unary minus ensure result_exists: Result /= void infix "/" (other: like Current): like Current -- Division by other require other_exists: other /= void; good_divisor: divisible (other) ensure result_exists: Result /= void infix "^" (other: NUMERIC): NUMERIC -- Current object to the power other require other_exists: other /= void; good_exponent: exponentiable (other) ensure result_exists: Result /= void invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); neutral_addition: equal (Current + zero, Current); self_subtraction: equal (Current - Current, zero); neutral_multiplication: equal (Current * one, Current); self_division: divisible (Current) implies equal (Current / Current, one); end -- class NUMERIC