## Re: [eiffel-nice-library] Postcondition for 'to_integer'

Expand Messages
• ... Yes, it will. ... The part for negative numbers looks like item (1) = - implies (substring(1, count - 1).is_equal((result // 10).out) and item (count) =
Message 1 of 6 , Feb 1, 2001
• 0 Attachment
Roger Browne wrote:

> is_equal (result.out)
>
> ...only needs to evaluate to 'true' for the recursive call in which
> 'current' is in its canonical form (no leading '+' or '0'). Could we
> rewrite it as follows?
>
> substring(1, count - 1).is_equal((result // 10).out)
> and substring(count, count).is_equal((result \\ 10).out)
>
> The recursion will terminate, because we are applying INTEGER.out to a
> smaller value every time.

Yes, it will.

> My example only solves the problem for non-negative values. The first
> part of your postcondition also needs to evaluate to 'true' for STRINGs
> having a single leading minus sign and no leading zeros. I guess this
> could be solved - but the result would not be pretty, and I don't even
> know that all compilers handle "//" and "\\" the same way for negative
> numbers (many compilers in many programming languages get this wrong).

The part for negative numbers looks like

item (1) = ''-' implies
(substring(1, count - 1).is_equal((result // 10).out)
and item (count) = (result \\ 10).out.item (2))

(I use the following relation: x = (x // 10) * 10 + x \\ 10)

So, the original

is_equal (result.out)

can be rewritten as

(item (1) /= '-' implies
(substring(1, count - 1).is_equal((result // 10).out)
and item (count) = (result \\ 10).out.item (1))) and
(item (1) = ''-' implies
(substring(1, count - 1).is_equal((result // 10).out)
and item (count) = (result \\ 10).out.item (2)))

Regards,
Alexander Kogtenkov
Object Tools, Moscow
• Thanks, Alexander for doing all the hard work to make this postcondition rigorous. Now we have two possibilities. Alexander s first design yields a simpler
Message 2 of 6 , Feb 1, 2001
• 0 Attachment
Thanks, Alexander for doing all the hard work to make this postcondition
rigorous.

Now we have two possibilities. Alexander's first design yields a simpler
postcondition for STRING.to_integer and a more complex postcondition for
INTEGER.out:

STRING.to_integer
ensure
is_equal (result.out) -- (1)
or else
(item (1) = '+' or else item (1) = '0') and then -- (2)
result = substring (2, count).to_integer
or else
is_equal ("-0") and result = 0 -- (3)
or else
item (1) = '-' and then item (2) = '0' and then -- (4)
result = (("-") + substring (3, count)).to_integer

INTEGER.out
ensure
(0 <= item and item <= 9) implies result.count = 1
and result.item (1).code - ('0').code = item
and
(- 9 <= item and item <= - 1) implies
result.is_equal ("-" + (- item).out)
and
item > 9 implies result.is_equal ((item // 10).out
+ (item \\ 10).out)
and
item < - 9 implies result.is_equal ((item // 10).out
+ ((- item) \\ 10).out)

Alexander's second design yields a more complex postcondition for
STRING.to_integer and a simpler postcondition for INTEGER.out:

STRING.to_integer
ensure
(item (1) /= '-' implies -- (1)
(substring(1, count - 1).is_equal((result // 10).out)
and item (count) = (result \\ 10).out.item (1))) and
(item (1) = '-' implies
(substring(1, count - 1).is_equal((result // 10).out)
and item (count) = (result \\ 10).out.item (2)))
or else
(item (1) = '+' or else item (1) = '0') and then -- (2)
result = substring (2, count).to_integer
or else
is_equal ("-0") and result = 0 -- (3)
or else
item (1) = '-' and then item (2) = '0' and then -- (4)
result = (("-") + substring (3, count)).to_integer

INTEGER.out
ensure
result.to_integer = current

The following comments apply to both designs:

> zeroes in negative numbers)
> (2) - leading plus or zero
> (3) - "-0"
> (4) - the number starts with "-0" as in (3) but has more digits

Both designs look good to me. Does anyone have a preference for one over
the other?

If all the preferences favour one design, I'll put that one in the vote.
If preferences favour both designs, I'll run a separate vote to choose
between the two. And if no preferences are expressed, I'll put the second