The System Library (SLIB)

The B-Toolkit is supplied with a set of reusable machines which encapsulate basic state and data-structures, and provide basic abstract types.

These library machines are described here. The text of the machines is presented separately.

The Role of the System Library

Static and persistent data of an implementation must be held by an imported machine. Ultimately, the bottom level implementation must import a Library machine if static or persistent data is required (i.e. if you are implementing a state-machine).

A library machine is used simply by importing or seeing the machine in the construct you are writing. When a predefined machine is imported into an implementation, actual parameters must be supplied. However when seeing an existing machine no parameters should be supplied.

Each library machine is formally specified, and the readable formal specification is available in the development environment after the machine has been committed.

The manipulation of an object can be performed outside the state-machine to which the object belongs, using the TYPE machines of the Library.

Simple i/o can be performed using the i/o machines.

Persistence of data can be achieved using the file i/o machines.

Naming of Library Machines and their Operations

The naming library machines and their operations follows a uniform scheme.

Library machines with state have to be renamed when they are imported into a development. These machines and their operations, therefore, all have names starting with Rename, which is automatically replaced by a new prefix supplied in the importing machine at the time that the library machine is committed from the library.

The TYPE machines in the library have no state, and need not be renamed. They can be cited in a SEES clause wherever they are required.

Operations in library machines are named according to a uniform pattern described in the text below.

Library Machines

Library Machines are organised into five groups as follows.

Multiple Objects Machines

Programming Concepts Machines

Mathematical Concepts Machines

Input Output Machines

Type Machines

Multiple Objects Machines

A Multiple Object Machine is a repository for structured objects. In this sub-library we have:

Rename_set_obj, a machine for collections of Sets
Rename_seq_obj, a machine for collections of Sequences.
Rename_str_obj, a machine for collections of Strings of Bytes.
Rename_fnc_obj, a machine for collections of Functions over Natural Numbers.
Rename_ffnc_obj, a machine for collections of Functions over Natural Numbers with multiple field operations.

In most applications of B to software development, the Multiple Objects Machines are used for representing the main part of the information which an application maintains. Composite object structures which are suitable for representing complex information structures can also be constructed.

For example, by using combinations of the Multiple Objects Machines we can construct a suitable representation for files of records with different field types. Types can be simple types ( SCALAR, BOOL, BITS) or more complex (Sets of Strings, Sequences of Sets of Strings, Sets of Sequences of BITS etc). Such constructions gives the formal B design language the equivalent power of a modern high level programming notation.

When importing a Multiple Object Machine it must be instantiated with respect to the size of store which will be pre-allocated for storing its objects, and with respect to the type of elements which actually will populate the structured objects. A multiple object machine can store a number of objects of the required type (e.g. sequences of BOOL, sets of SCALARS, sets of SEQOBJ).

Composite object structures can be constructed. For example a `Sequences of Sets of SCALARS' is constructed by using a Set Object machine instantiated with SCALAR in combination with a Sequence Object machine instantiated with SETOBJ.

When providing a design using a machine as a repository then elements of different types can be stored within the same machine; e.g. a sequence object machine instantiated with `BOOL or SCALAR' (written BOOL \/ SCALAR) can store Boolean values as well as scalar values (positive integers) within the same sequence.

All Multiple Objects Machines offer the following facilities:

Initialisation (INI): This operation resets the repository to its initial empty state.
Creation (CRE) and killing (KIL) of objects: On creation of a new object a unique token will be allocated to denote the created object (e.g SEQOBJ are the tokens allocated for Sequence Objects). If the creation has been successful this token will be returned on creation, and required as input for any operation concerning this object (e.g. killing).
Capacity Enquiries (MEM_FUL, OBJ_FUL): All these operations can be used to determine whether the capacity of the repository has been reached.
Token Enquiries (ANY, XST): ANY returns a token of proper type (e.g. the Sequence Machine's ANY operation returns a SEQOBJ token). The XST operation can be used to determine whether a token denotes an object which actually exists.
Persistent storage (SAV, RST): The save operation (SAV) saves the current state of the object machine onto permanent storage, while the restore operation (RST) restores the object machine to a previously saved state.
Note that when saving several structures on the same file then the restores must be performed in the same order as the saves were performed; different dump files can be used by using file_io operations.
Browsing facilities (FIRST, NEXT): A browse through all stored objects is initiated by using the FIRST operation, which will return an object (if any) and a cursor for continuing the browse by using NEXT. When the cursor reaches `1' the last object has been retrieved.

Machine Rename_set_obj

The general multiple object operations, which are described above, are provided:

Initialisation (INI).
Creation (CRE) and killing (KIL) of sets; on creation the created set will be empty.
Capacity Enquiries (MEM_FUL, OBJ_FUL)
Set token Enquiries (ANY, XST).
Persistent Set storage facilities (SAV, RST).
Sets Browsing facilities (FIRST, NEXT).

In addition, this machine offers special operations for set manipulation and enquiring about the stored sets:

Operations for changing existing sets: (CPY, CLR) CPY copies one set to another set; CLR removes all elements from a set.
Operations for enlarging sets: (ENT, UNION) ENT enters a new element into a set; UNION extends a set by all the members of another set.
Operations for reducing sets: (RMV, DIFF, INTER) RMV removes an element from a set; DIFF removes all elements which are also present in another set; INTER keeps only the elements which are present in another set.
Enquiring about size of sets: (EMP, CRD) EMP returns TRUE if the set interrogated is empty; CRD gives the cardinality of a set.
Facilities for inspecting a particular set: (XST_ORD, VAL) All elements in all sets can be accessed by using their ordinal number. XST_ORD will indicate whether a particular number is a valid ordinal number. VAL will return the value of an element in the set, given its ordinal number.
Operations for determining set properties: (MBR, INCL) MBR will indicate whether a particular element is a member of a set; INCL will indicate whether one set is included in another.

Machine Rename_seq_obj

The general multiple object operations, which are described above, are provided:

Initialisation (INI).
Creation (CRE) and killing (KIL) of sequences. On creation the created sequence will be empty.
Capacity Enquiries (MEM_FUL, OBJ_FUL)
Sequence token Enquiries (ANY, XST).
Persistent Set storage facilities (SAV, RST).
Sequence Browsing facilities (FIRST, NEXT).

In addition, this machine offers special operations for manipulation of sequences, and enquiring about stored sequences:

Operations for changing existing sequences: (CPY, CLR, OVR, STO) CPY copies one sequence to another sequence; CLR resets a sequence to the empty sequence; OVR over-writes a sequence with another sequence; STO over-writes a particular location in the sequence.
Operations for re-ordering an existing sequence: (SWA, REV) SWA swaps two elements in a sequence; REV reverses an entire sequence.
Operations for enlarging sequences: (PSH, APP) PSH pushes an element onto the end of a sequence; APP extends a sequence with another sequence.
Operations for reducing sequences: (KEP, CUT) KEP keeps an initial part of a sequence; CUT cuts an initial part of a sequence away.
Enquiring about a sequence: (EMP, LEN) EMP returns TRUE if a sequence is empty; LEN gives the length of a sequence.
Facilities for inspecting a particular sequence: (POP, XST_IDX, VAL) POP returns the most recently pushed element; an element in a sequence can be accessed by using its index in its sequence; XST_IDX will indicate whether a particular number is a valid index; VAL will return the value of an element in the sequence given its index.
Operations for determining sequence properties: (MBR, EQL) MBR will indicate whether a particular element is a member of a sequence. EQL will indicate whether two sequences are identical.

Machine Rename_str_obj

The String Machine is a repository for sequences of bytes (seq(0..255)). It is often used for storing text strings. The facilities for strings offered in the library and the the B translators enable strings to be treated as simple objects, which can be transferred from one machine to another using operation which will transfers the entire structured string object. (Also available in the form of a Fixed Function Machine)

The general multiple object operations, which are described above, are provided:

Initialisation (INI).
Creation (CRE) and killing (KIL) of strings; on creation the created string will be empty.
Capacity Enquiries (MEM_FUL, OBJ_FUL)
String token Enquiries (ANY, XST).
Persistent String storage facilities (SAV, RST).
String Browsing facilities (FIRST, NEXT).

In addition, this machine offers special operations for manipulation of strings, and enquiring about stored strings:

An additional operation for creating a particular string: (NEW) NEW will create a new string with a particular contents, which either literally occurs in the design text, or, is the contents of a string which is a result of an input operation, or, is the contents of a string extracted elsewhere.
An additional operation for extracting string contents: (XTR)
Operations for changing existing strings: (CPY, CLR, OVR, STO) CPY copies one string to another string; CLR sets a string to the empty string; OVR over-writes a string with another string; STO over-writes a particular location in the string.
Operations for re-ordering an existing string: (SWA, REV) SWA swaps two bytes in a string; REV reverses an entire string.
Operations for enlarging strings: (PSH, APP) PSH pushes a byte onto the end of a string; APP extends a string with another string.
Operations for reducing strings: (KEP, CUT) KEP keeps an initial part of a string; CUT cuts an initial part of a string away.
Enquiring about size of strings: (EMP, LEN) EMP returns TRUE if a string is empty; LEN gives the length of a string.
Facilities for inspecting a particular strings: (POP, XST_IDX, VAL) POP returns the most recently pushed byte; a byte in a string can be accessed by using its index in its string. XST_IDX will indicate whether a particular number is a valid index. VAL will return the value of a byte in the string, given its index.
Operations for determining string properties: (SMR, EQL, EQL_LIT) SMR will indicate whether one string is lexicographically smaller than another string. EQL will indicate whether two store strings are identical. EQL_LIT will indicate whether a stored string is identical to another literal string (not stored in by this machine).

Machine Rename_fnc_obj

This machine stores partial Functions over an initial interval of Natural Numbers. The interval (its fields) will be determined when the machine is instantiated.

The general multiple object operations, which are described above, are provided:

Initialisation (INI).
Creation (CRE) and killing (KIL) of objects. On creation the created object will be empty.
Capacity Enquiries (FUL)
Function token Enquiries (ANY, XST).
Persistent String storage facilities (SAV, RST).
Object Browsing facilities (FIRST, NEXT).

In addition, this machine offers special operations for manipulation of functions, and enquiring about stored functions:

Enquiry operations: (TST_FLD, DEF_FNC) TST_FLD will indicate whether a given number input is a field of the function. DEF_FNC will indicate whether a function has been given a value for a particular field number.
Operations for changing a function: (STO, RMV) STO assigns a value to a particular field of a particular function; RMV removes a field from a function - the function will then be undefined for this field.

Machine Rename_ffnc_obj

This machine stores partial Functions over an initial interval of Natural Numbers. The interval (its fields) will be determined when the machine is instantiated. The general multiple object operations, which are described above, are provided:

Initialisation (INI).
Creation (CRE) and killing (KIL) of objects. The created function will be empty.
Capacity Enquiries (FUL)
Function token Enquiries (ANY, XST).
Persistent Object storage facilities (SAV, RST).
Object Browsing facilities (FIRST, NEXT).

This machine also offers the operations for manipulation of functions, and enquiring about stored functions as are available for the standard Function Object Machine:

Enquiry operations: (TST_FLD, DEF_FNC) TST_FLD will indicate whether a given number is a field of a function. DEF_FNC will indicate whether a function has been given a value for a particular field number.
Operations for changing a function: (STO, RMV) STO assigns a value to a particular field of a particular function; RMV removes a field from a function - the function will then be undefined for this field.

In addition, special operations for multiple field manipulation are provided:

Moving several field values from one function to another: (MOV_FFNC) MOV_FFNC will over-write the field values of one function with field values from another function.
Overwriting several field values: (OVR_FFNC) OVR_FFNC will overwrite several fields in a function with the packed version of a sequence of bytes (String).
Extracting multiple field values: (XTR_FFNC) XTR_FFNC will extract several field values - converted into a sequence of bytes stored at a word boundary.
Testing multiple fields: (EQL_FFNC) This tests whether the contents of sequence of bytes is equal to the sequence of bytes stored in multiple fields of a function.

Programming Concepts Machines

These machine offer an extension of the basic data structures of variable and array which are available in most languages. We have:

Rename_Vvar, a Variable of any type.
Rename_Nvar, a Natural Number Variable.
Rename_Varr, an Array of any type.
Rename_Narr, an Array of Natural Numbers.

These machines are commonly used to record transitory information within an application, or used as `anchors' for information stored in the Multiple Object Machines.

Variables can be instantiated to any type, e.g a variable of type BOOL can hold a boolean value, and a variable of type SEQOBJ (an anchor) can hold an token denoting a sequence within the Sequence Object Machine.

When providing a design using a machine as a repository, then elements of different types can be stored within the same machine. For example instantiating a machine with BOOL \/ SCALAR will enable a machine to have both boolean values as well as scalar values within a single structure.

All Programming Concepts Machines offer the following facilities:

Getting a value (VAL) VAL will return the value of a variable, or in the case of an array the value of a particular location.
Storing a value (STO) STO will assign a new value to a variable or in the case of an array to a particular location within the array.
Testing for values (EQL, NEQ) EQL and NEQ will test the contents of a variable (or a particular location within an array~) against another value.
Persistent storage facilities (SAV, RES) SAV will save the current value of an object onto permanent storage; RES will restore the value of an object to a value previously saved.

Note that when saving several structures on the same file then the restores must be performed in the same order as the saves were performed; different dump files can be used by using file_io operations.

Also note that these primitive operations appear as `procedure calls' within the algorithms of a B implementation; however in the generated implementation (the C-Code) all the simple operations from the Programming Concepts Machines are `in-lined' (no procedure calls are involved).

Machine Rename_Vvar

This Variable machine offers all the facilities described above, and can be instantiated to any type (SCALAR, BOOL, BITS, SETOBJ, etc.) We have:

Getting a value (VAL)
Storing a value (STO)
Testing for values (EQL, NEQ)
Persistent storage facilities (SAV, RES)

Machine Rename_Nvar

This Variable machine, can hold only Numbers, and offers all the facilities available for a Programming Concepts Machine:

Getting a value (VAL)
Storing a value (STO)
Testing for values (EQL, NEQ)
Persistent storage facilities (SAV, RES)

In addition the following operations are provided:

Arithmetic operations (INC, DEC, ADD, MUL, SUB, DIV, MOD) A variable can be modified by: INCrementing it, DECrementing it, ADDing to it, MULtiplying it by a number, SUBtracting a value from it, DIViding it with a number, or replacing it with a MODulo value.
Ordering Queries (GTR, GEQ, SMR, LEQ) A variable can be tested to determine whether it is GreaTeR then a particular number, Greater or EQual to a number, SMalleR than a number, or, Less than or EQual to a number.
Conditional retrieval (MIN, MAX) MIN will retrieve the smaller of two values, while MAX will retrieve the larger of two values.

Machine Rename_Varr

This Array machine can be used to store several values of any type. The type is determined by instantiation.

This machine offers all the facilities available for a Programming Concepts Machine:

Getting a value (VAL) Getting the value under a particular index of the array.
Storing a value (STO) Storing a value in a particular location of the array.
Testing for values (EQL, NEQ) Testing the value stored under a particular index.
Persistent storage facilities (SAV, RES)

In addition the following operations are provided:

Index testing (TST_IDX) TST_IDX will indicate whether a particular index is a valid index.
Search operations (SCH_LO_EQL, SCH_LO_NEQ, SCH_HI_EQL, SCH_HI_NEQ) These operation will return the lowest (or highest) array index which is equal (or not equal) to a particular given value.
Array manipulations (REV, RHT, LFT, SWP) REV will reverse the array; RHT and LFT will shift the values in an array either to the right (to higher indices) or left (to lower indices); SWP will swap two values in an array.

Machine Rename_Narr

This Array machine can be used to store several Numbers.

This machine offers all the facilities available for a Programming Concepts Machine:

Getting a value (VAL) Getting the value under a particular index of the array.
Storing a value (STO) Storing a value in a particular location of the array.
Testing for values (EQL, NEQ) Testing the value stored under a particular index.
Persistent storage facilities (SAV, RES)

In addition the following operations are provided:

Arithmetic operations (ADD, MUL, SUB, DIV, MOD) An array location can be modified by: INCrementing it, DECrementing it, ADDing to it, MULtiplying it by a number, SUBtracting a value from it, DIViding it with a number, or replacing it with a MODulo value.
Ordering Queries (GTR, GEQ, SMR, LEQ) An array location can be tested to determine whether it is GreaTeR than a particular number, Greater or EQual to a number, SMalleR than a number or Less than or EQual to a number.
Conditional retrieval (MIN, MAX) MIN will retrieve an array index, for which the array holds a minimum value, while MAX will retrieve an an array index, for which the array holds a maximum value.

In addition the following operations are provided:

Index testing (TST_IDX) TST_IDX will indicate whether a particular index is a valid index.
Search operations (SCH_LO_EQL, SCH_LO_NEQ, SCH_HI_EQL, SCH_HI_NEQ) These operation will return the lowest (or highest) array index which is equal (or not equal) to a particular given value.
Additional Search operations (SCH_LO_GEQ, SCH_LO_GTR, SCH_LO_LEQ, SCH_LO_SMR, SCH_HI_GEQ, SCH_HI_GTR, SCH_HI_LEQ, SCH_HI_SMR) These operation will return the lowest (or highest) array index which is relates in a particular way (greater or equal, greater, less or equal, or, smaller) to a given value.
Array manipulations (REV, RHT, LFT, SWP) REW will reverse the array; RHT and LFT will shift the values in an array either to the right (to higher indices) or left (to lower indices); SWP will swap two values in an array.
Additional Array manipulations (SRT_ASC, SRT_DSC) Sort the array to contain either ascending values or descending values.

Client-Server Machines

Machine Rename_Client / Rename_Server

These two machines are used as a pair to establish a Socket (TCP/IP) Client-Server Connection.

For the Client machine:

An operation to initialise the socket: Rename_INIT
Operations on the socket: Rename_CONNECT, Rename_WRITE, Rename_READ and Rename_CLOSE
Operations to read from the input buffer: Rename_GET_TOK, Rename_GET_STR and Rename_GET_FIL
Operations to write from the output buffer: Rename_PUT_TOK and Rename_PUT_STR
Operations to get and set the buffer input pointer: Rename_SET_IN_PTR and Rename_GET_IN_PTR
Operations to get and set the buffer output pointer: Rename_SET_OUT_PTR and Rename_GET_OUT_PTR

For the Server machine:

An operation to initialise the socket: Rename_INIT
Operations on the socket: Rename_ACCEPT, Rename_WRITE, Rename_READ and Rename_CLOSE
Operations to read from the input buffer: Rename_GET_TOK, Rename_GET_STR and Rename_PUT_FIL
Operations to write from the output buffer: Rename_PUT_TOK and Rename_PUT_STR
Operations to get and set the buffer input pointer: Rename_SET_IN_PTR and Rename_GET_IN_PTR
Operations to get and set the buffer output pointer: Rename_SET_OUT_PTR and Rename_GET_OUT_PTR
Operations for buffer saving & restoring: Rename_SAV_BUF, Rename_RST_BUF, Rename_NXT_BUF and Rename_SAV_RMV

Mathematical Concepts Machines

The Mathematical Concepts Machines allow the programmer to design using higher level concepts, which are likely to match more closely the concepts used in a set theoretical specification, hence making the design step more reliable. We have:

Rename_set, a Set machine.
Rename_Vseq, a Sequence machine for a sequence of any type.
Rename_Nseq, a Sequence machine for a sequence of Numbers.
Rename_Vfnc, a Function machine of a particular range type.
Rename_Nfnc, a Function machine for a Natural Number function.
Rename_Vffnc, an Extended Function machine.

The Mathematical Concepts Machines are either used for storing transitory information or for `anchors' to information stored within a Multiple Object Machine. When importing Mathematical Concepts Machine its type and its capacity must be given by instantiation. When providing a design using a machine as a repository then elements of different types can be stored within the same machine. For example instantiating a machine with BOOL \/ SCALAR will enable a machine to have both boolean values as well as scalar values within a single structure. A Mathematical Concepts Machine offers the following common facilities:

Getting a value (VAL) The VAL operation returns a particular value within the structure.
Persistent Storage facilities (SAV, RES) For saving onto and restoring from permanent storage. NoteWhen saving several structures on the same file then the `restores' must be performed in the same order as the `saves' were performed; different dump files can be used by using file_io operations.

Machine Rename_set

A set machine provides access to a single set structure. It offers the common operation for Mathematical Concepts Machine:

Getting a value (VAL) with a particular ordinal number.
Persistent Storage facilities (SAV, RST)

In addition it offers:

Familiar Set Operations: (ENT, RMV, CLR) ENT enters a new element into the set; RMV removes an element from the set; CLR clears the set
Familiar Set Enquiries: (MBR, EMP, CRD) MBR is used for testing set membership; EMP tests whether a set is empty; CRD gives the cardinality of a set.
Additional Enquiries (FUL, XST_IDX) FUL indicates whether a set is full; XST_IDX indicates whether a particular number is a valid ordinal.

Machine Rename_Vseq

This sequence machine provides access to a single sequence. The type of the elements of the sequence can be determined through instantiation. It offers the common operations for Mathematical Concepts Machine:

Getting a value (VAL) with a particular ordinal number.
Persistent Storage facilities (SAV, RST)

In addition it offers:

Familiar Sequence Operations: (CLR, PSH, POP, FST, LST, TAL, ST0) CLR clears the sequence; PSH pushes an element onto the sequence; POP gets the element most recently pushed; FST gets the first element; LST gets the last element; TAL modifies the sequence by removing the most recently pushed element; STO stores an element into the sequence.
Some Sequence Enquiries: (EMP, LEN) EMP test whether the sequence is empty; LEN gives the length of the sequence.
Some Sequence Tests: (NEQ, NEQ) EQL tests whether a particular value is at a particular index; NEQ tests whether a particular value is not at a particular index.
Additional Enquiries: (FUL, XST_IDX) FUL indicates whether a sequence is full; XST_IDX indicates whether a particular number is a valid index.
Searching Operations: (SCH_LO_EQL, SCH_LO_NEQ, SCH_HI_EQL, SCH_HI_NEQ) The searching operation search for the lowest (or highest) index in the sequence which is equal (or not equal) to a particular value.
Sequence manipulation operations: (KEP, CUT, SWP, REV, RHT, LFT) KEP keeps the beginning of a sequence; CUT cuts the beginning of a sequence away; SWP swaps two values in the sequence; REV reverses the entire sequence; RHT shifts some elements in the sequence to the right (up); LFT shifts some elements in the sequence to the left (down).

Machine Rename_Nseq

This sequence machine provides access to a single sequence of numbers. It offers the common operations for Mathematical Concepts Machine:

Getting a value (VAL)(VAL) with a particular ordinal number.
Persistent Storage facilities (SAV, RST)

It offers the common sequence operation:

Familiar Sequence Operations: (CLR, PSH, POP, FST, LST, TAL, STO) CLR clears the sequence; PSH pushes an element onto the sequence; POP gets the element most recently pushed; FST gets the first element; LST gets the last element; TAL modifies the sequence by removing the most recently pushed element; STO stores an element into the sequence.
Some Sequence Enquiries: (EMP, LEN) EMP test whether the sequence is empty; LEN gives the length of the sequence.
Some Sequence Tests: (EQL, NEQ) EQL tests whether a particular value is at a particular index; NEQ tests whether a particular value is not at a particular index.
Additional Enquiries: (FUL, XST_IDX) FUL indicates whether a sequence is full; XST_IDX indicates whether a particular number is a valid index.
Searching Operations: (SCH_LO_EQL, SCH_LO_NEQ, SCH_HI_EQL, SCH_HI_NEQ) The searching operation search for the lowest (or highest) index in the sequence which is equal (or not equal) to a particular value.
Sequence manipulation operations: (KEP, CUT, SWP, REV, RHT, LFT) KEP keeps the beginning of a sequence; CUT cuts the beginning of a sequence away; SWP swaps two values in the sequence; REV reverses the entire sequence; RHT shifts some elements in the sequence to the right (up); LFT shifts some elements in the sequence to the left (down).

In addition the Number Sequence Machine offers:

Extracting Values: (MAX_IDX, MIN_IDX) These operation extract the maximum (or minimum) value within a particular range.
Arithmetic Operations: (ADD, MUL, SUB, DIV, MOD) These operations modify a particular location within the sequence.
Test Operations: (GTR, GEQ, SMR, LEQ) These operations test a particular location within the sequence against a given value.
Searching Operations: (SCH_LO_GEQ, SCH_LO_GTR, SCH_LO_LEQ, SCH_LO_SMR, CH_HI_GEQ, SCH_HI_GTR, SCH_HI_LEQ, SCH_HI_SMR) These operations search for the lowest index (or highest index) in which a value satisfying a particular condition can be found.
Sequence manipulations: (SRT_AS, SRT_DSC) Sort the sequence to contains either ascending or descending values.

Machine Rename_Vfnc

This function machine provides access to a single partial function over numbers (mapping). The type of elements which the function returns can be determined through instantiation. It offers the common operations for Mathematical Concepts Machine:

Getting a value by applying the function (VAL) .
Persistent Storage facilities (SAV RES)

In addition it offers:

Changing the function: (STO RMV) STO gives the function a new value for a particular field number; RMV removes a field number from the domain of the function.
Testing function values: (EQL NEQ) These tests for a particular value in a particular field. in the function.
Enquiries: (TST_FLD, DEF FREE) TST_FLD indicates whether a given number is a valid field number; DEF tests whether a given number is within the domain of the function; FREE return a field number for which no value has yet been given.

Machine Rename_Nfnc

This function machine provides access to a single partial function over numbers (mapping). The function will return numbers. It offers the common operations for Mathematical Concepts Machine:

Getting a value by applying the function (VAL).
Persistent Storage facilities (SAV, RES)

It offers:

Changing the function: (STO, RMV) STO gives the function a new value for a particular field number; RMV removes a number from the domain of the function.
Arithmetic operations: (ADD, MUL, SUB, DIV, MOD) These operation modifies the value of the function for a particular field number.
Testing function values: (EQL, NEQ, GTR, GEQ, SMR, LEQ) These tests for a given value in a particular field in the function.
Enquiries: (TST_FLD, DEF, FREE) TST_FLD indicates whether a particular number is a valid field number; DEF tests whether a particular number is within the domain of the function; FREE return a field number for which no value has yet been given.

Machine Rename_Vffnc

Getting a value by applying the function (VAL).
Persistent Storage facilities (SAV, RES)

It offers the additional operations:

Changing the function: (STO, RMV) STO gives the function a new value fro a particular field number; RMV removes a number from the domain of the function.
Testing function values: (EQL, NEQ) These tests for a given value in a particular field. in the function.
Enquiries: (TST_FLD, DEF FREE) TST_FLD indicates whether a particular number is a valid field number; DEF tests whether a particular number is within the domain of the function; FREE return a field number for which no value has yet been given.

Some special operation for manipulation of segments of fields:

Moving segments of values: (MOV) This operation moves the values stored in a seqment of fields to another segment of fields.
String Operations: (OVR, XTR) OVR over-writes a number of function fields with a packed string; XTR extracts a string from a number of function fields.
String Testing: (EQL) Tests whether a particular string is equal to a string packed in a number of fields.

Input Output Machines

The Input Output Machines offers an application some simple input and output facilities:

basic_io, for basic terminal IO.
Rename_token_io, for more terminal IO.
Rename_File_io, for general file IO.
file_dump, for persistent storage.

Machine basic_io

This machine provides operations for writing to the terminal display and reading from the keyboard:

Spacing operations: (NWL, BLK)
Writing and reading numbers: (GET_NBR, GET_PROMPT_NBR, PUT_NBR) An interval to which the numbers must belong is specified.
Writing and reading B numbers: (GET_NAT, GET_PROMPT_NAT, PUT_NAT)
Writing and reading boolean values: (GET_BOOL, GET_PROMPT_BOOL, PUT_BOOL)
Writing and reading binary values: (GET_BTS, GET_PROMPT_BTS, PUT_BTS)
Writing and reading strings: (GET_STR, GET_PROMPT_STR, PUT_STR)
Writing and reading characters: (GET_CHR, PUT_CHR)

Machine Rename_token_io

This IO facility allows for a value of any elementary type to be read from the keyboard and written to the screen. NoteThis includes SEQOBJ, SETOBJ etc., since all these are represented as a single machine word) We have: (Rename_GET_TOK, Rename_GET_PROMPT_TOK, Rename_PUT_TOK)

File Machines

Machine Rename_File_io

A new file can be introduced by importing an instance of the file_io machine. This new file can be opened for writing/appending by Rename_OPEN_READ/ Rename_OPEN_APPEND. All subsequent `saves' will now be written to that file. The file can be opened for reading by Rename_OPEN_WRITE. All subsequent `restores' will now be read from that file. Rename_CLOSE will close the file. A file should always be closed to ensure that all written information is properly recorded.

Machine file_dump

This machine provides the default dump file (TMP.file), which is known by all object machines. Unless otherwise specified this file can be used for `saving' and `restoring'. open_write_dump_file will open the dump file for saving. open_read_dump_file will open the dump file for restoring. close_dump_file will close the dumpfile. A file should always be closed to ensure that all written information is properly recorded.

Machine Rename_file_dump

This machine provides the renamble dump file (Rename.dump). Rename_open_write_dump_file will open the dump file for saving. Rename_open_read_dump_file will open the dump file for restoring. Rename_close_dump_file will close the dumpfile. A file should always be closed to ensure that all written information is properly recorded.

Type Machines

The following machines allow for the manipulation of local variables introduced in an algorithm within an implementation. A value might be retrieved from the state of an object machine into a local variable, and then modified using the operation provided by the Type Operation Machines before stored into an object machine.

Machine Bool_TYPE / Bool_TYPE_Ops

Introduce the type BOOL which consists only of the values TRUE and FALSE. The Bool machines provide the familiar boolean operations:

Conjunction (and): CNJ
Disjunction (or): DIS
Negation (not): NEG
Bit conversion: BTS_BOOL This operation returns 1 for input TRUE and 0 for FALSE input .

Machine String_TYPE / String_TYP_Ops

These machines introduce the types CHAR and STRING. The operation CPY_STR must be used for assigning a value of type string to a local variable; the operations ASSIGN_ANY_STR, EN_STR, VAL_ITH_CHAR and HAR_TO_NAT are also provided.

Machine Scalar_TYPE / Scalar_TYPE_Ops

This machines introduce the type of SCALAR (= 0..2147483646). The following operations are provided:

Assigning a Scalar SCL
Arithmetic Operations (INC, DEC, ADD, MUL, SUB, DIV, MOD, RND)
Testing operations: (EQL, NEQ, GTR, GEQ, SMR, LEQ, EQZ) EQZ tests for zero.

Note that the normal syntax available in programming languages can be used within an algorithm of a B implementation. e.g ` :=' for assignment, ` +' for ADD, ` =' for EQL. However, if this syntax is used then no checks will be made by the B-Toolkit for over-flow.

Machine Int_TYPE / Int_TYPE_Ops

This machines introduce the type of INT (=- 2147483647 to +2147483646). The following operations are provided:

Assigning an INT SCL
Arithmetic Operations (INCI, DECI, ADDI, MULI, SUBI, DIVI, MODI)
Testing operations: (EQLI, NEQI, GTRI, GEQI, SMRI, LEQI, EQZI) EQZI tests for zero.

Note that the normal syntax available in programming languages can be used within an algorithm of a B implementation. e.g ` :=' for assignment, ` +' for ADDI, ` =' for EQLI. However, if this syntax is used then no checks will be made by the B-Toolkit for over-flow.

Machine Bit_TYPE / Bit_TYPE_Ops

This machine introduces the type of BITS as a set of sequences of length 32. The most significant bit position is 1, the least significant position is 32. We have:

Bit operations: (VAL, STO) VAL returns the value of a bit; STO stores a new bit.
Shifts: (LFT, RHT) LFT shifts left; RHT shifts right (no wrap-around).
Bit-wise Logical Operations: (CPL, LND, LOR, LXR) CPL negates all bits; LND performs a bit-wise `and'; LOR performs bit-wise `or'; LXR performs bit-wise `exclusive or'.
Masking Operations: (MSK, VMS, MMS) MSK generates a mask of 1's; VMS performs a masking and returns the resulting value; MMS merges a pattern with another pattern using a mask.

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo