API Reference

type Binary_File_Type

 
   type Binary_File_Type is limited private; 

data type representing binary files This type controls the access mode for a file the type representing a single binary digit a bit sequence of arbitrary length

procedure Create_Binary_File

   procedure Create_Binary_File(  
      File : in out Binary_File_Type; 
      Mode : in Binary_File_Mode; 
      File_Name : String); 

Description

Creates a new binary file with the given file name

Preconditions

P.1 - File is not already open

P.2 - Given file name has to be valid e.g. not empty

Postconditions

C.1 - File is created and available for operations as

specified in the Mode parameter.

Exceptions

P.1 violated - exception Status_Error is raised

Notes

Mode In_Mode should not be supplied as this is nonsensical, why would a new (empty) file be created for reading only?

procedure Open_Binary_File

   procedure Open_Binary_File(  
      File : out Binary_File_Type; 
      Mode : in Binary_File_Mode; 
      File_Name : in String); 

Description

Opens an already existing binary file with the given file name

Preconditions

P.1 - File is not already open

P.2 - the given file with name File_Name exists P.3 - Given file name has to be valid e.g. not empty

Postconditions

C.1 - File is opened and available for operations as

specified in the Mode parameter.

Exceptions

P.1 violated - exception Status_Error is raised P.2 violated - exception Name_Error is raised

Notes

If mode In_File is supplied, then the file will be read-only. If mode Out_File is supplied, the file that exists will be erased and a new file created for writing.

If mode Append_File is supplied, the file cursor will be set to the end for append writing.

procedure Close_Binary_File

   procedure Close_Binary_File(  
      File : in out Binary_File_Type); 

Description

Opens an already existing binary file with the given file name

Preconditions

P.1 - File is open

Postconditions

C.1 - File is opened with the specified mode for manipulation.

Exceptions

P.1 violated - exception Status_Error is raised

Notes

procedure Delete_Binary_File

   procedure Delete_Binary_File(  
      File : in out Binary_File_Type); 

Description

Deletes the opened binary file

Preconditions

P.1 - File is open

P.2 - the external environment (Operating system et al) supports

the deletion of this file.

Postconditions

C.1 - File is deleted and the access closed.

Exceptions

P.1 violated - exception Status_Error is raised P.2 violated - exception Use_Error is raised

Notes

function Is_Open

   function Is_Open(  
      File : in Binary_File_Type) return Boolean; 

Description

Checks to see if the given file handle is open.

Preconditions

None.

Postconditions

C.1 - a boolean value is returned, True if and only if the file is

open.

Exceptions

None.

Notes

procedure Read_Bit

   procedure Read_Bit(  
      File : in out Binary_File_Type; 
      Bit  : out Binary_Digit_Type); 

Description

Reads a single bit from a file.

Preconditions

P.1 - The file is open.

P.2 - The file is of mode In_File.

P.3 - The file has not been depleted, i.e. there are still bits

to be read.

Postconditions

C.1 - Bit is read from the file, and the file cursor advanced

to the next bit.

Exceptions

P.1 violated - exception Status_Error is raised. P.2 violated - exception Mode_Error is raised. P.3 violated - exception End_Error is raised.

Notes

procedure Write_Bit

   procedure Write_Bit(  
      File : in out Binary_File_Type; 
      Bit  : in Binary_Digit_Type); 

Description

Writes a single bit to a file.

Preconditions

P.1 - The file is open.

P.2 - The file is not of mode In_File.

P.3 - The external maximum capacity of the file has not been

exceeded.

Postconditions

C.1 - Bit is written to the end of the file.

Exceptions

P.1 violated - exception Status_Error is raised.

P.2 violated - exception Mode_Error is raised.

P.3 violated - exception Use_Error is raised.

Notes

bits should be written in blocks of 8 since the byte is the basic unit of most (if not all) file systems, so the bits are actually only written once a byte has been completed. If the file is closed in the middle of a byte, then the spare bits are set to 0 and written before the file is closed.

procedure Write_Bit_Sequence

   procedure Write_Bit_Sequence(  
      File : in out Binary_File_Type; 
      Bits : in Binary_Array_Type); 

Description

Writes a bit sequence to a file.

Preconditions

P.1 - The file is open.

P.2 - The file is not of mode In_File.

P.3 - The external maximum capacity of the file has not been

exceeded.

Postconditions

C.1 - Bit is written to the end of the file.

Exceptions

P.1 violated - exception Status_Error is raised. P.2 violated - exception Mode_Error is raised.

P.3 violated - exception Use_Error is raised.

Notes

The same problem arises as with Write_Bit, bits should be written so that there are no spare bits in a byte, or that your program is aware of the fact that spare bits may exist and handles this appropriately.

function End_Of_File

   function End_Of_File(  
      File : in Binary_File_Type) return Boolean; 

Description

Checks to see if the file has been depleted, i.e. there are no bits left to be read.

Preconditions

P.1 - The file is open.

Postconditions

C.1 - a boolean value is returned, True if and only if the file is

open.

Exceptions

P.1 violated - exception Status_Error is raised.

Notes

Currently this does give any real meaningful result (or exception) if an attempt is made to call this with a file of mode Out_File or Append_File. This will be resolved shortly.

function Make_Integer

   function Make_Integer(  
      Binary_Array : in Binary_Array_Type) return Integer; 

Description

Creates an integer from an 8-bit or less binary sequence.

Preconditions

None.

Postconditions

C.1 - an Integer is created from the bit contents, with the

left-most bit (i.e. lowest index) being the most significant bit.

Exceptions

None.

Notes

If the binary sequence is larger than 8, then the bits after the 8th bit in the sequence are ignored.