Date: Mon, 18 May 1998 10:03:53 +0200
Message-Id: <199805180803.KAA00738@pc85.lri.fr>
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
To: N Hur <mapnh@maths.bath.ac.uk>
Subject: Re: Is this OK?
In-Reply-To: <Pine.SUN.3.91.980515135653.27393A-100000@thor.maths.bath.ac.uk>
> (* a camllight session *)
>
> #(-234)/4
> ;;
> - : int = -58
>
>
> #div_big_int (big_int_of_string "-234") (big_int_of_string "4");;
> - : big_int = -59
There is OK. Indeed, when defining the quotient and the remainder you
must specify the range of the remainder. Usually, you specify that the
remainder of the division of a by b is between 0 and b-1, whatever is
the sign of a. That is the case in the big_in library.
But in the case of Caml division, the specification is different: the
remainder has the same sign that a, which is negative in your example.
But in both cases you always have
a = b * (a/b) + (a mod b)
which is the expected invariant.
-- Jean-Christophe FILLIATRE mailto:Jean-Christophe.Filliatre@lri.fr http://www.lri.fr/~filliatr
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:14 MET