TableType(K, V): Category
|K||PrimitiveType||the type of the keys|
|V||Type||the type of the entries|
TableType(K, V) is the category of tables, i.e. discrete many-to-one mappings from keys to entries. More precisely, every element of a domain of this category is a table whose slots contain elements from V and such that every slot is given by a unique key from K.
BoundedFiniteDataStructureType Cross(K, V) : Tuple Cross(K, V) % creation of a table apply: (%, K) V extraction of an entry entries: % Generator V iterate through the entries find: (K, %) Partial V search for an entry keys: % Generator K iterate through the keys numberOfEntries: % MachineInteger number of entries set!: (%, K, V) V modification of an entry table: () % creation of a table MachineInteger %
if has InputType and has InputType then
if has OutputType and has OutputType then
if has SerializableType and has SerializableType then