Resolve/C++ Catalog
CI/Text/Hash_1.h
Copyright © 2010, Reusable Software Research Group, The Ohio State University

//  /*-------------------------------------------------------------------*\
//  |   Concrete Instance : Text_Hash_1
//  \*-------------------------------------------------------------------*/

#ifndef CI_TEXT_HASH_1
#define CI_TEXT_HASH_1 1

///------------------------------------------------------------------------
/// Global Context --------------------------------------------------------
///------------------------------------------------------------------------

#include "AT/General/Hash.h"

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

concrete_instance
utility_class Text_Hash_1 :
    implements
	abstract_instance General_Hash <Text>
{
public:

    /*!
	math definition HASH_FUNCTION (
		x: string of character
	    ): integer satisfies
	    if x = empty_string
	    then HASH_FUNCTION (x) = 0
	    else there exists c: character, s: string of character
		     (x = <c> * s  and
		      HASH_FUNCTION (x) = TO_INTEGER (c) +
			  HASH_FUNCTION (s))	    
    !*/

    utility_function_body Integer Hash (
	    preserves Text& x
	)
    {
	object Integer i, result;

	while (i < x.Length ())
	/*!
	    alters i, result
	    preserves x
	    maintains
		there exists a, b: string of character
		    (|a| = i  and
		     x = a * b  and
		     result = HASH_FUNCTION (a))
	    decreases
		|x| - i
	!*/
	{
	    result += To_Integer (x[i]);
	    i++;
	}
	return result;
    };

};

#endif // CI_TEXT_HASH_1