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

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

#ifndef AT_GENERAL_READ_WRITE
#define AT_GENERAL_READ_WRITE 1

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

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

    /*!
	math definition READ_WRITE_REP (
		x: Base
	    ): string of character satisfies restriction
	    "\n" is suffix of READ_WRITE_REP (x)  and
	    for all y: Base where (y /= x)
		(READ_WRITE_REP (y) is not prefix of READ_WRITE_REP (x))
    !*/

    procedure Read (
	    alters Character_IStream& str
	) is_abstract;
    /*!
	produces self
	requires
	    str.is_open = true  and
	    there exists x: Base, s: string of character
		(s is prefix of str.content  and
		 s = READ_WRITE_REP (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
		 s = READ_WRITE_REP (self))
    !*/

    procedure Write (
	    alters Character_OStream& str
	) is_abstract;
    /*!
	preserves self
	requires
	    str.is_open = true
	ensures
	    str.is_open = true  and
	    str.ext_name = #str.ext_name  and
	    str.content = #str.content * READ_WRITE_REP (self)
    !*/

};

#endif // AT_GENERAL_READ_WRITE