001package components.naturalnumber;
002
003import components.sequence.Sequence;
004import components.sequence.Sequence1L;
005
006/**
007 * {@code NaturalNumber} represented as a {@link Sequence<Integer>} with
008 * implementations of primary methods.
009 *
010 * <p>
011 * Execution-time performance of all methods implemented in this class is O(1),
012 * except the constructors from {@code String} (which is O(|{@code s}|)) and
013 * from {@code NaturalNumber} (which is O(log {@code n})).
014 *
015 * @mathdefinitions {@code
016 * HAS_ONLY_DIGITS (
017 *   s: string of integer
018 *  ): boolean satisfies
019 *  if s = empty_string
020 *   then HAS_ONLY_DIGITS (s) = true
021 *   else for all a: string of integer, k: integer where (s = a * <k>)
022 *    (HAS_ONLY_DIGITS (s) = (HAS_ONLY_DIGITS (a)  and  0 <= k < 10))
023 *
024 * IS_WELL_FORMED_RADIX_REPRESENTATION (
025 *   s: string of integer
026 *  ): boolean is
027 *  s = empty_string  or
028 *      there exists k: integer, a: string of integer
029 *       (s = <k> * a  and
030 *        1 <= k < 10  and
031 *        HAS_ONLY_DIGITS (a))
032 *
033 * NUMERICAL_VALUE (
034 *   s: string of integer
035 *  ): integer satisfies
036 *  if s = empty_string
037 *   then NUMERICAL_VALUE (s) = 0
038 *   else for all a: string of integer, k: integer where (s = a * <k>)
039 *         (NUMERICAL_VALUE (s) = NUMERICAL_VALUE (a) * 10 + k)
040 *
041 * STRING_OF_DIGITS (
042 *   n: NATURAL
043 *  ): string of integer
044 *  if n = 0
045 *  then STRING_OF_DIGITS (n) = empty_string
046 *  else STRING_OF_DIGITS (n) = STRING_OF_DIGITS (n/10) * <n mod 10>
047 * }
048 * @convention IS_WELL_FORMED_RADIX_REPRESENTATION ($this.digits)
049 * @correspondence this = NUMERICAL_VALUE ($this.digits)
050 */
051public class NaturalNumber4 extends NaturalNumberSecondary {
052
053    /*
054     * 2221/2231 assignment code deleted.
055     */
056
057}