Loading ...
Sorry, an error occurred while loading the content.

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

Expand Messages
  • Alexander Kogtenkov
    ... 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
    • Roger Browne
      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:

        > (1) - no leading plus and/or zeroes (including leading
        > 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
        design into the vote.

        Regards,
        Roger
        --
        Roger Browne - roger@... - Everything Eiffel
        19 Eden Park Lancaster LA1 4SJ UK - Phone +44 1524 32428
      Your message has been successfully submitted and would be delivered to recipients shortly.