Re: Ada function sqrt(x)

[Roderick Chapman <rod@praxis.co.uk>]

Keith Thompson wrote:
> 
> In <51o7nh$5vl@cf01> pascal.obry@der.edfgdf.fr (Pascal Obry) writes:
> > "zeppelin" <zeppelin@access.mountain.net> wrote:
> >
> > >I want to find the sqrt of a interger... how can I do this and what package
> > >do I need to declare
> [...]

A simple binary chop search is possible.  The algorihtm is not that complex, and can
even be proven correct with respect to a formal specification (yes...I've
actually done this just recently.)  Decide if you want a truncated or rounded
answer, and be careful when you want an answer for values near Integer'Last, since
it's easy to end up trying to square a number that will overflow.

Another algorihtm is detailed at:
   http://www.best.com/~mxmora/umpg/UMPG_II_Math&Algorithms.html

In the article Jamie McCarthy, a fast "bit twiddly" algorithm is given which 
we've found to be about twice as fast as the binary chop.  Interestingly, it
can be implemented efficiently in Ada (even in the SPARK subset) without
any implementation-dependent support for unsigned integers or bit-wise
operations.  I wouldn't fancy your chances of proving this algorihtm
correct, though.  I've run an exhausitve test over our the domain of
inetegers we have, and it gives the same result as the binary chop algorithm,
so that's good enough for me!

 - Rod Chapman, 
   Praxis Critical Systems rod@praxis.co.uk