// /*-------------------------------------------------------------------*\// | 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