Date: Mon, 18 May 1998 10:03:53 +0200
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
To: N Hur <firstname.lastname@example.org>
Subject: Re: Is this OK?
> (* a camllight session *)
> - : 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