Resolve/C++ Catalog
AI/Id_Name_Table/Kernel.h
Copyright © 2010, Reusable Software Research Group, The Ohio State University

//  /*-------------------------------------------------------------------*\
//  |   Abstract Instance : Id_Name_Table_Kernel
//  \*-------------------------------------------------------------------*/

#ifndef AI_ID_NAME_TABLE_KERNEL
#define AI_ID_NAME_TABLE_KERNEL 1

///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

abstract_instance 
class Id_Name_Table_Kernel
{
public:

    /*!
	math subtype ID_NAME_TABLE_MODEL is finite set of (
		id: integer,
		name: string of character
	    )
	    exemplar m
	    constraint
		for all id1, id2: integer,
	                name1, name2: string of character
			where ((id1, name1) is in m  and
			       (id2, name2) is in m)
		    (id1 = id2 iff name1 = name2)
		    
	math definition ID_IS_DEFINED_IN (
		m: ID_NAME_TABLE_MODEL,
		id: integer
	    ): boolean is
	    there exists name: string of character ((id, name) is in m)

        math definition NAME_IS_DEFINED_IN (
		m: ID_NAME_TABLE_MODEL,
		name: string of character
	    ): boolean is
	    there exists id: integer ((id, name) is in m)
    !*/

    standard_abstract_operations (Id_Name_Table_Kernel);
    /*!
        Id_Name_Table_Kernel is modeled by ID_NAME_TABLE_MODEL
        initialization ensures
	    self = empty_set
    !*/

    procedure Add_Id_Name_Pair (
	    preserves Integer id,
            consumes Text& name
	) is_abstract;
    /*!
	requires
	    not ID_IS_DEFINED_IN (self, id) and
	    not NAME_IS_DEFINED_IN (self, name)
	ensures
	    self = #self union {(id, #name)}
    !*/

    procedure Remove_Id_Name_Pair (
            preserves Integer id,
	    preserves Text name,
	    produces Integer& id_copy,
	    produces Text& name_copy
	) is_abstract;
    /*!
	requires
	    (id, name) is in self
	ensures
	    id_copy = id and
	    name_copy = name and
	    self = #self - {(id, name)}
    !*/

    procedure Remove_Any_Pair (
            produces Integer& id,
	    produces Text& name
	) is_abstract;
    /*!
	requires
	    self /= empty_set
	ensures
	    self = #self - {(id, name)}
    !*/

    procedure Look_Up_Name_Via_Id (
            preserves Integer id,
	    produces Text& name
	) is_abstract;
    /*!
	preserves self
	requires
	    ID_IS_DEFINED_IN (self, id)
	ensures
	    (id, name) is in self
    !*/
 
    procedure Look_Up_Id_Via_Name (
            produces Integer& id,
	    preserves Text name
	) is_abstract;
    /*!
	preserves self
	requires
	    NAME_IS_DEFINED_IN (self, name)
	ensures
	    (id,name) is in self
    !*/

    function Boolean Id_Is_In_Table (
	    preserves Integer id
	) is_abstract;
    /*!
	ensures
	    Id_Is_In_Table = ID_IS_DEFINED_IN (self, id)
    !*/

    function Boolean Name_Is_In_Table (
	    preserves Text name
	) is_abstract;
    /*!
	ensures
	    Name_Is_In_Table = NAME_IS_DEFINED_IN (self, name)
    !*/

    function Integer Size () is_abstract;
    /*!
	ensures
	    Size = |self|
    !*/

};

#endif // AI_ID_NAME_TABLE_KERNEL