Re: Is this OK?

From: Jean-Christophe Filliatre (Jean-Christophe.Filliatre@lri.fr)
Date: Mon May 18 1998 - 10:03:53 MET DST


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