Resolve/C++ Catalog
AT/General/Get_From.h
Copyright © 2010, Reusable Software Research Group, The Ohio State University

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

#ifndef AT_GENERAL_GET_FROM
#define AT_GENERAL_GET_FROM 1

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

abstract_template <
	concrete_instance class Base
    >
class General_Get_From :
    extends
        concrete_instance Base
{
public:

    /*!
	math definition IS_AN_INPUT_REP (
		s: string of character,
		x: Base
	    ): boolean

	math definition IS_TOO_SHORT_A_PREFIX (
                s: string of character,
		i: string of character
	    ): boolean is
	    there exists x: Base, t: string of character
		(s is proper prefix of t  and
		 t is prefix of i  and
		 IS_AN_INPUT_REP (t, x))
    !*/

    procedure Get_From (
	    alters Character_IStream& str
	) is_abstract;
    /*!
	produces self
	requires
	    str.is_open = true  and
	    str.content /= empty_string  and
	    there exists x: Base, s: string of character
		(s is prefix of str.content  and
		 IS_AN_INPUT_REP (s, x))
	ensures
	    str.is_open = true  and
	    str.ext_name = #str.ext_name  and
	    there exists s: string of character
		(#str.content = s * str.content  and
		 IS_AN_INPUT_REP (s, self)  and
		 not IS_TOO_SHORT_A_PREFIX (s, #str.content))
    !*/

};

#endif // AT_GENERAL_GET_FROM