Bugs Catalog
AI/BL_Tokenizing_Machine/Get.h
Copyright © 2011, Reusable Software Research Group, The Ohio State University

//  /*----------------------------------------------------------------------*\
//  |   Abstract Instance : BL_Tokenizing_Machine_Get
//  \*----------------------------------------------------------------------*/

#ifndef AI_BL_TOKENIZING_MACHINE_GET
#define AI_BL_TOKENIZING_MACHINE_GET 1

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

#include "AI/BL_Tokenizing_Machine/Kernel.h"
	
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

abstract_instance
class BL_Tokenizing_Machine_Get :
    extends
	abstract_instance BL_Tokenizing_Machine_Kernel
{
public:
    
    /*!
	math definition IS_NEXT_TOKEN_AND_REMAINDER (
                in_str: string of character
                token_text: string of character
                c: character
                out_str: string of character
            ): boolean satisfies
	    IS_NEXT_TOKEN_AND_REMAINDER (in_str, token_text, c, out_str) =
	    (in_str = token_text * <c> * out_str and
	     IS_COMPLETE_TOKEN_TEXT (token_text, c) and
	     for all t2, out_str2: string of character, c2: character
		 (if IS_NEXT_TOKEN_AND_REMAINDER (in_str, t2, c2, out_str2)
		  then |token_text| <= |t2|))

        math definition IS_NEXT_NON_SEPARATOR_TOKEN_AND_REMAINDER (
                in_str: string of character
                token_text: string of character
                c: character
                out_str: string of character
            ): boolean satisfies
	    (IS_NEXT_TOKEN_AND_REMAINDER (in_str, token_text, c, out_str) and
	     WHICH_KIND (token_text) /= WHITE_SPACE and
	     WHICH_KIND (token_text) /= COMMENT) or
	    (there exists t1, out_str1: string of character,
			  c1: character
		 (IS_NEXT_TOKEN_AND_REMAINDER (in_str, t1, c1, out_str1) and
		  IS_NEXT_NON_SEPARATOR_TOKEN_AND_REMAINDER (
			       <c1> * out_str1, token_text, c, out_str) and
		  (WHICH_KIND (t1) = WHITE_SPACE or
		   WHICH_KIND (t1) = COMMENT)))
		       
        math definition IS_REMAINDER_AFTER_LEADING_SEPARATORS (
                in_str: string of character
                out_str: string of character
            ): boolean satisfies
	    if there exists t, o: string of character, c: character
		(IS_NEXT_TOKEN_AND_REMAINDER (in_str, t, c, o)  and
		 (WHICH_KIND (t) = WHITE_SPACE  or
		  WHICH_KIND (t) = COMMENT))
	    then
		there exists t, o: string of character, c: character
		(IS_NEXT_TOKEN_AND_REMAINDER (in_str, t, c, o)  and
		 (WHICH_KIND (t) = WHITE_SPACE  or
		  WHICH_KIND (t) = COMMENT) and
		  IS_REMAINDER_AFTER_LEADING_SEPARATORS (in_str, out_str) =
		      IS_REMAINDER_AFTER_LEADING_SEPARATORS
			  (<c> * o, out_str))
	    else
		IS_REMAINDER_AFTER_LEADING_SEPARATORS (in_str, out_str) =
		    (in_str = out_str)
		    
    !*/

    procedure Get_Next_Token (
            alters   Character_IStream& str,
            produces Text& token_text,
            produces Integer& token_kind
        ) is_abstract;
    /*!
	requires
	    str.is_open = true
	ensures
	    str.is_open = true and
	    str.ext_name = #str.ext_name and
	    (if there exists t, x: string of character, c: character
		(IS_NEXT_TOKEN_AND_REMAINDER (
		     #self.buffer * #str.content, t, c, x))
	     then
		 there exists c: character
		     (self.buffer = <c> and
		      IS_NEXT_TOKEN_AND_REMAINDER (
			  #self.buffer * #str.content,
			  token_text, c, str.content))
	     else
		 token_text = #self.buffer * #str.content and
		 str.content = empty_string and
		 self.buffer = empty_string) and
	    self.ready_to_dispense = false and
	    token_kind = WHICH_KIND (token_text)
    !*/

    procedure Get_Next_Non_Separator_Token (
            alters   Character_IStream& str,
            produces Text& token_text,
            produces Integer& token_kind
        ) is_abstract;
    /*!
	requires
	    str.is_open = true
	ensures
	    str.is_open = true and
	    str.ext_name = #str.ext_name and
	    (if there exists t, x: string of character, c: character 
		(IS_NEXT_NON_SEPARATOR_TOKEN_AND_REMAINDER (
		     #self.buffer * #str.content, t, c, x))
	     then
		 there exists c: character
		     (self.buffer = <c> and
		      IS_NEXT_NON_SEPARATOR_TOKEN_AND_REMAINDER (
			  #self.buffer * #str.content,
			  token_text, c, str.content))
	     else
		 self.buffer = empty_string  and
		 str.content = empty_string  and
		 IS_REMAINDER_AFTER_LEADING_SEPARATORS
		     (#self.buffer * #str.content, token_text))
	    self.ready_to_dispense = false  and
	    token_kind = WHICH_KIND (token_text)
    !*/

};

#endif // AI_BL_TOKENIZING_MACHINE_GET