EiffelBase class
(HTML page generated by ISE Eiffel 4.2)
Eiffel Class
indexing
description: "Objects to which numerical operations are applicable";
note: "The model is that of a commutative ring.";
status: "See notice at end of class";
date: "$Date: 2007-03-30 11:10:11 -0800 (Fri, 30 Mar 2007) $";
revision: "$Revision: 95354 $"
deferred class NUMERIC
feature -- Access
one: like Current is
-- Neutral element for "*" and "/"
deferred
ensure
result_exists: Result /= void
end;
zero: like Current is
-- Neutral element for "+" and "-"
deferred
ensure
result_exists: Result /= void
end;
feature -- Status report
divisible (other: like Current): BOOLEAN is
-- May current object be divided by other?
require
other_exists: other /= void
deferred
end;
exponentiable (other: NUMERIC): BOOLEAN is
-- May current object be elevated to the power other?
require
other_exists: other /= void
deferred
end;
feature -- Basic operations
infix "+" (other: like Current): like Current is
-- Sum with other (commutative).
require
other_exists: other /= void
deferred
ensure
result_exists: Result /= void;
commutative: equal (Result, other + Current)
end;
infix "-" (other: like Current): like Current is
-- Result of subtracting other
require
other_exists: other /= void
deferred
ensure
result_exists: Result /= void
end;
infix "*" (other: like Current): like Current is
-- Product by other
require
other_exists: other /= void
deferred
ensure
result_exists: Result /= void
end;
infix "/" (other: like Current): like Current is
-- Division by other
require
other_exists: other /= void;
good_divisor: divisible (other)
deferred
ensure
result_exists: Result /= void
end;
infix "^" (other: NUMERIC): NUMERIC is
-- Current object to the power other
require
other_exists: other /= void;
good_exponent: exponentiable (other)
deferred
ensure
result_exists: Result /= void
end;
prefix "+": like Current is
-- Unary plus
deferred
ensure
result_exists: Result /= void
end;
prefix "-": like Current is
-- Unary minus
deferred
ensure
result_exists: Result /= void
end;
invariant
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
|
