Re: can Ada give run-time error or warning for integer division with non-zero remainder?

[Brad Moore <brad.moore@shaw.ca>]

Or you could simplify this further using some new Ada 2012 features, and 
eliminate the body.

package Integers is
    type Integer is new Standard.Integer;

    overriding function "/" (L : Integer; R  : Integer) return Integer is
      (Integer (Standard.Integer (L) / Standard.Integer (R)))
    with Post => "/"'Result * R = L;

    function "/" (L : Standard.Integer; R  : Integer) return Integer is
       (Integer (L / Standard.Integer (R)))
    with Post => "/"'Result * R = Integer (L);

    function "/" (L : Integer; R  : Standard.Integer) return Integer is
       (Integer (Standard.Integer (L) / R))
    with Post => "/"'Result * Integer (R) = L;

end Integers;

Brad


On 12/08/2012 1:16 AM, Per Sandberg wrote:
> If you want an new behaviour for "/" on an integer type you could always
> make a new integer type with the required properties:
> -------------------------------------------------------------------------
> package Integers is
>     type Integer is new Standard.Integer;
>     overriding function "/" (L : Integer; R  : Integer) return Integer;
>     function "/" (L : Standard.Integer; R  : Integer) return Integer;
>     function "/" (L : Integer; R  : Standard.Integer) return Integer;
> end Integers
> -------------------------------------------------------------------------
> package body Integers is
>
>     overriding function "/" (L : Integer; R  : Integer) return Integer is
>     begin
>        return Ret : Integer do
>           Ret := Integer (Standard.Integer (Standard.Integer (L) /
>     Standard.Integer (R))); if Ret * R /= L then
>              raise Constraint_Error with L'Img & "/" & R'Img & " gives
>     reminder."; end if;
>        end return;
>     end "/";
>
>     function "/" (L : Standard.Integer; R  : Integer) return Integer is
>     begin
>        return Ret : Integer do
>           Ret := Integer (L) / R;
>        end return;
>     end "/";
>
>     function "/" (L : Integer; R  : Standard.Integer) return Integer is
>     begin
>        return Ret : Integer do
>           Ret := L / Integer (R);
>        end return;
>     end "/";
>
> end Integers;