Insufficient Contract for text_substring in YY_SCANNER

The contract for text_substring in class YY_SCANNER is insufficient. 
Here is the current contract for reference:

text_substring (s, e: INTEGER): STRING is
    -- Substring of last token read
    -- (Create a new string at each call.)
    -- (For efficiency reason, this function can bypass the
    -- call to `text' and create the substring directly from
    -- the input buffer.)
  require
    meaningful_start: 1 <= s
    meaningful_interval: s <= e + 1
    meaningful_end: e <= text_count
  deferred
  ensure
    text_substring_not_void: Result /= Void
    text_substring_empty: (s > e) implies (Result.count = 0)
    definition: s <= e implies Result.is_equal (text.substring (s, e))
  end

In particular the precondition `meaningful_interval' is too strong. 
It does not allow empty strings or single character strings. A better 
precondition would be:

meaningful_interval: s <= e - 1

Then the postcondition text_substring_empty is meaningful (it was 
previously impossible to have s > e). Furthermore we can replace 
`meaningful_interval' with a postcondition that would make the 
semantics of e and s clearer (e.g. is e one past the last item, or is 
it the last item?)

text_substring_count: Result.count = e - s + 1

You could then eliminate text_substring_empty.

Here is my proposed contract in full:

text_substring (s, e: INTEGER): STRING is
    -- Substring of last token read
    -- (Create a new string at each call.)
    -- (For efficiency reason, this function can bypass the
    -- call to `text' and create the substring directly from
    -- the input buffer.)
  require
    meaningful_start: 1 <= s
    meaningful_interval: s <= e - 1
    meaningful_end: e <= text_count
  deferred
  ensure
    text_substring_not_void: Result /= Void
    text_substring_count: Result.count = e - s + 1
    definition: s <= e implies Result.is_equal (text.substring (s, e))
  end

I don't know if this will affect the implementation. I haven't tested 
this in any way.

Thanks,
Brian






To Post a message, send it to:   [email protected]
To Unsubscribe, send a blank message to: [email protected] 
Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/gobo-eiffel/

<*> To unsubscribe from this group, send an email to:
    [email protected]

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/