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

Problem in DOUBLE.floor

Expand Messages
  • Berend de Boer
    Hello SmallEiffel, When flooring the DOUBLE -2147483648.0, an exception is raised due to an postcondition failing: floor: INTEGER is -- Greatest integral value
    Message 1 of 3 , Jul 1, 2000
    • 0 Attachment
      Hello SmallEiffel,

      When flooring the DOUBLE -2147483648.0, an exception is raised due to an
      postcondition failing:

      floor: INTEGER is
      -- Greatest integral value no greater than Current.
      local
      d: DOUBLE;
      do
      d := double_floor;
      Result := d.truncated_to_integer;
      ensure
      result_no_greater: Result <= Current;
      close_enough: Current - Result < one
      end;

      The value -2147483647.0 converts fine. I really don't care that much, but I
      post this message in case this postcondition is incorrect and the
      SmallEiffel team wants to change it a bit.

      Groetjes,

      Berend. (-:
    • Thomas Aglassinger
      ... Shouldn t this have a precondition like require (Current = 0) implies (Current =
      Message 2 of 3 , Jul 1, 2000
      • 0 Attachment
        On 01-Jul-00, Berend de Boer wrote:

        > When flooring the DOUBLE -2147483648.0, an exception is raised due to an
        > postcondition failing:
        >
        > floor: INTEGER is
        > -- Greatest integral value no greater than Current.

        Shouldn't this have a precondition like

        require
        (Current >= 0) implies (Current <= Maximum_integer.to_double)
        (Current < 0) implies (Current >= Minimum_integer.to_double)

        in other words: does the input result into something that can be expressed
        as INTEGER? (Probably a -1 is missing somewhere in my suggestion...)

        Interestingly, the various "other" short forms (ELKS95, ISE, OT) on the web
        don't have this precondition. That means, the also produce wrong
        results, or the raise some kind of overflow exception.

        Regards,

        Thomas.
      • David Broadfoot
        ... Simply require Current = Minimum_integer.to_double ... Just like C and most other languages. David
        Message 3 of 3 , Jul 1, 2000
        • 0 Attachment
          > From: Thomas Aglassinger [mailto:agi@...]
          > Shouldn't this have a precondition like
          >
          > require
          > (Current >= 0) implies (Current <= Maximum_integer.to_double)
          > (Current < 0) implies (Current >= Minimum_integer.to_double)

          Simply
          require
          Current <= Maximum_integer.to_double
          Current >= Minimum_integer.to_double

          > in other words: does the input result into something that can be expressed
          > as INTEGER? (Probably a -1 is missing somewhere in my suggestion...)
          >
          > Interestingly, the various "other" short forms (ELKS95, ISE, OT) on the web
          > don't have this precondition. That means, the also produce wrong
          > results, or the raise some kind of overflow exception.

          Just like C and most other languages.

          David
        Your message has been successfully submitted and would be delivered to recipients shortly.