procedure UPDATE(FILE : in FILE_TYPE);

    Operates on a file of mode INOUT_FILE. Updates the current
    element of the given file with the contents of the file buffer.
    If the format of the associated external file record is fixed and
    the current position in the file buffer does not indicate the end
    of the buffer, the rest of the file buffer is filled with zero
    bits before being written to the file.

    The exception MODE_ERROR is raised if the current mode is not
    INOUT_FILE. The exception USE_ERROR is raised if the current
    element is undefined at the start of this operation or if some
    key specification in the file buffer violates the external file
    attributes defined for that key. The exception KEY_ERROR is
    raised if a key has been changed or duplicated and if changes
    or duplicates are not allowed by the external file.