- Roger Browne wrote:

> is_equal (result.out)

Yes, it will.

>

> ...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.

> My example only solves the problem for non-negative values. The first

The part for negative numbers looks like

> 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).

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

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:

> (1) - no leading plus and/or zeroes (including leading

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

> zeroes in negative numbers)

> (2) - leading plus or zero

> (3) - "-0"

> (4) - the number starts with "-0" as in (3) but has more digits

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

design into the vote.

Regards,

Roger

--

Roger Browne - roger@... - Everything Eiffel

19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428