Package components.naturalnumber
Interface NaturalNumberKernel
- All Superinterfaces:
Standard<NaturalNumber>
- All Known Subinterfaces:
NaturalNumber
- All Known Implementing Classes:
NaturalNumber1L
,NaturalNumber2
,NaturalNumber3
,NaturalNumber4
,NaturalNumberSecondary
Natural number kernel component with primary methods. (Note: by package-wide
convention, all references are non-null.)
- Mathematical Subtypes:
NATURAL is integer exemplar n constraint n >= 0
- Mathematical Model (abstract value and abstract invariant of this):
type NaturalNumberKernel is modeled by NATURAL
- Constructor(s) (initial abstract value(s) of this):
(): ensures this = 0 (int i): requires i >= 0 ensures this = i (String s): requires there exists n: NATURAL (s = TO_STRING(n)) ensures s = TO_STRING(this) (NaturalNumber n): ensures this = n
-
Field Summary
Modifier and TypeFieldDescriptionstatic final int
A constant, with value 10, holding the radix (or base) for NaturalNumber. -
Method Summary
Modifier and TypeMethodDescriptionint
Dividesthis
by 10 and reports the remainder.boolean
isZero()
Reports whetherthis
is zero.void
multiplyBy10
(int k) Multipliesthis
by 10 and addsk
.Methods inherited from interface components.standard.Standard
clear, newInstance, transferFrom
-
Field Details
-
RADIX
A constant, with value 10, holding the radix (or base) for NaturalNumber.- See Also:
-
-
Method Details
-
multiplyBy10
Multipliesthis
by 10 and addsk
.- Parameters:
k
- theint
to be added- Updates:
this
- Requires:
0 <= k < 10
- Ensures:
this = 10 * #this + k
-
divideBy10
int divideBy10()Dividesthis
by 10 and reports the remainder.- Returns:
- the remainder
- Updates:
this
- Ensures:
#this = 10 * this + divideBy10 and 0 <= divideBy10 < 10
-
isZero
boolean isZero()Reports whetherthis
is zero.- Returns:
- true iff
this
is zero - Ensures:
isZero = (this = 0)
-