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

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

#ifndef CI_TEXT_ARE_IN_ORDER_3
#define CI_TEXT_ARE_IN_ORDER_3 1

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

#include "AT/General/Are_In_Order.h"

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

concrete_instance
utility_class Text_Are_In_Order_3 :
    implements
	abstract_instance General_Are_In_Order <Text>
{
public:

    /*!
	math definition ARE_IN_ORDER (
		x: string of character,
		y: string of character
	    ): boolean is
	    [x is alphabetically less than or equal to y]
    !*/

    utility_function_body Boolean Are_In_Order (
	    preserves Text& x,
	    preserves Text& y
	)
    {
	object Integer i;

	while (i < x.Length() and i < y.Length())
	/*!
	    preserves x, y
	    alters i
	    maintains
		0 <= i <= |x|  and
		0 <= i <= |y|  and
		there exists a, b: string of character
		    (|a| = |b| = i  and
		     a is prefix of x  and
		     b is prefix of y  and
		     [a is alphabetically equal to b, i.e.,
		      they are equal except for case])
	    decreases
		min (|x|,|y|) - i
	!*/
	{
	    if (To_Lower(x[i]) < To_Lower(y[i]))
	    {
		return true;
	    }
	    else if (To_Lower(x[i]) > To_Lower(y[i]))
	    {
		return false;
	    }
	    else // x[i] == y[i], where x[i] and y[i] are
		 // case-insensitive to alphabetic characters
	    {
		i++;
	    }
	}

	// x and y have maximal case-insensitive prefixes that are identical

	if (x.Length() != y.Length())
	{
	    return (x.Length() <= y.Length());
	}
	else
	{
	    return x <= y;
	}

    };

};

#endif // CI_TEXT_ARE_IN_ORDER_3