IntegerList

AddIntegerAt AddIntegerLast FindInteger IntegerAt ReplaceIntegerAt

Attributes

InitialListWordFormat

Fields

instance IntegerList tag;
end instance;

Define Class IntegerList;
    inherits from FixedList;
    uses extra list: Signed;
    
    // getting
    operation IntegerAt(index: Unsigned): Unsigned, noFail;
        // get the value of a single integer in the list
    
    // adding and removing
    operation ReplaceIntegerAt(index: Unsigned; integer: Unsigned);
        // overwrite the integer at position <index>, leaving the list the same length
    operation AddIntegerAt(index: Unsigned; integer: Unsigned);
        // insert an integer into the list at position <index>
    operation AddIntegerLast(integer: Unsigned);
        // insert an integer at the end of the list
    
    // finding
    operation FindInteger(integer: Unsigned): Unsigned, noFail;
        // returns the index of the integer if found, zero if not

    overrides InitialListWordFormat;
        // returns integerWord to express the fact that integer lists
        // hold integers
end class;