//  /*-------------------------------------------------------------------*\
//  |   Abstract Template : Word_Occurrence
//  \*-------------------------------------------------------------------*/

#ifndef AT_WORD_OCCURRENCE
#define AT_WORD_OCCURRENCE 1

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

abstract_template <
        concrete_instance class Item
    >
class Word_Occurrence_Kernel
{
public:

    /*!
	math subtype WORD_FUNCTION is finite set of (
		d: Item
		r: Integer
	    )
	    exemplar m
	    constraint
		for all d1, d2: Item, r1, r2: Integer
			where ((d1,r1) is in m  and
			       (d2,r2) is in m)
		    (if d1 = d2 then r1 = r2)

	math definition IS_DEFINED_IN (
		m: WORD_FUNCTION,
		d: Item
	    ): boolean is
	    there exists r: Integer
		((d,r) is in m)


    !*/
    
    standard_abstract_operations (Word_Occurrence_Kernel);
    /*!
	Word_Occurrence_Kernel is modeled by WORD_FUNCTION
	initialization ensures
            self = empty_set
    !*/

    // A procedure operation has zero or more explicit parameters,
    // with their modes and types (examples shown).  It also has an
    // implicit alters-mode receiver object of type XYZ_Kernel that
    // is referred to as "self" in the contract specification.

    procedure Add (
	    consumes Item& d
	) is_abstract;
    /*!
	ensures
	
	    Item TO_LOWER
	    total = #total + 1
	    if Item NOT_IS_DEFINED IN #self
		    self = #self union {(#d, 1)}
	    else
		    self = #self{(#d, Integer++)}
    !*/

    procedure Remove (
            preserves Item& d,
            produces Item& d_copy,
	    produces Integer& r
	) is_abstract;
    /*!
	requires
	    IS_DEFINED_IN (self, d)
	ensures
	    d_copy = d  and
	    (d_copy, r) is in #self and
	    self = #self - {(d_copy, r)}
    !*/

    procedure Remove_Any (
            produces Item& d,
	    produces Integer& r
	) is_abstract;
    /*!
	requires
	    self /= empty_set
	ensures
	    (d, r) is in #self and
	    self = #self - {(d, r)}
    !*/

    function Integer& operator [] (
	    preserves Item& d
	) is_abstract;
    /*!
	requires
	    IS_DEFINED_IN (self, d)
	ensures
	    (d, self[d]) is in self
    !*/

    function Boolean Is_Defined (
	    preserves Item& d
	) is_abstract;
    /*!
	ensures
	    Is_Defined = IS_DEFINED_IN (self, d)
    !*/
    
    function Integer Size () is_abstract;
    /*!
	ensures
	    Size = |self|
    !*/

    function Integer Total () is_abstract;
    /*!
	ensures
	    Total = total
    !*/

};

#endif // AT_WORD_OCCURRENCE_KERNEL