Difference between revisions of "NUMERIC (interface)"
m |
m (→Class Interface: typo in invariant) |
||
| Line 4: | Line 4: | ||
==Class Interface== | ==Class Interface== | ||
| − | <code> | + | <code> |
indexing | indexing | ||
description: "Objects to which numerical operations are applicable"; | description: "Objects to which numerical operations are applicable"; | ||
| Line 108: | Line 108: | ||
self_subtraction: not is_special_case implies equal (Current - Current, zero); | self_subtraction: not is_special_case implies equal (Current - Current, zero); | ||
neutral_multiplication: not is_special_case implies equal (Current * one, Current); | neutral_multiplication: not is_special_case implies equal (Current * one, Current); | ||
| − | self_division: divisible not is_special_case implies (Current) implies equal (Current / Current, one) | + | self_division: divisible not is_special_case implies divisible (Current) implies equal (Current / Current, one) |
</code> | </code> | ||
Revision as of 11:11, 28 November 2006
Contents
Class Interface
indexing
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
