Re: Re: Insufficient Contract for text_substring in YY_SCANNER

Brian Heilig wrote:
> But I still think:
> 
>   text_substring_count: Result.count = e - s + 1
> 
> is a better postcondition.

I prefer the current postconditions where we clearly
see what we get in both cases:

     text_substring_empty: (s > e) implies (Result.count = 0)
     definition: s <= e implies Result.is_equal (text.substring (s, e))

In fact the first one should read:

     text_substring_empty: (s > e) implies Result.is_empty

but until recently STRING.is_empty was not supported by all
Eiffel compilers. So these postconditions are not about
the number of characters in Result (which can be implied
from the postconditions above), but what these characters
are (with a special case when there is no character).

-- 
Eric Bezault
mailto:ericb-D6Qt/9opevxWk0Htik3J/[email protected]
http://www.gobosoft.com



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/