From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.8 required=5.0 tests=BAYES_00,INVALID_DATE,
	MSGID_SHORT autolearn=no autolearn_force=no version=3.4.4
Path: utzoo!mnetor!uunet!mcvax!dik
From: dik@cwi.nl (Dik T. Winter)
Newsgroups: comp.lang.ada
Subject: Floating point attribute verification.
Message-ID: <7517@boring.cwi.nl>
Date: 4 Mar 88 23:01:03 GMT
Organization: CWI, Amsterdam
List-Id: <comp.lang.ada>

Attached you will find a program that will verify the correctness of
the values returned by floating point type attributes.  This program
was written within the framework of the Ada Europe Numerics Working
Group, and I thank the group members for there input and advise.

Attributes are crucial when an attempt is made to write a portable
problem.  And it is, of course, essential that the values returned
are correct.  But even with my current, limited, knowledge I know
that for every floating point type attribute there is at least one
compiler system that returns the wrong value!  And only a minority (2)
of the compiler systems tested so far (9) return (apparently) correct
values in all cases.  But I know from other sources that one of these
2 compilers gives wrong results in a number of other cases, and the
other compiler gives wrong results when a port to a different machine
is used.

It is clear that a program for the verification of the attributes
would be appropriate in the validation suite.  The problem is that
validation programs should be portable to all machines and compilers,
however weird they are.  But this program relies on some properties
of the hardware, and I do not know of a method to avoid this.
The most important property this program requires is that multiplication
of a positive floating point number by the machine radix either yields
an overflown result (which might have exponent wrap-around) or the
correct result.  I know of at least one binary machine where multiplication
of a floating point number by two might loose precision (though there is
not yet an Ada compiler on it).  So this program will fail on that
machine without any doubt.

As it is not feasible to put this program in the validation suite, I
intend to have this program put to as wide a public as possible.
I would appreciate if you, when you compile and execute this program,
would mail the results to me.  My addresses are in the header page
of the output.  Also feel free to communicate any problems or errors
you encounter with the program, so that I am able to adjust the program
accordingly (no program is perfect).

dik t. winter, cwi, amsterdam, nederland
Internet: dik@cwi.nl
Bitnet  : dik@mcvax (this is a nickname, do NOT use hamcwi6, it will fail)
UUCP    : ....uunet!dik@cwi.nl (or something like that)
------------
-- AENWG 15.8
-- Copyright (C) 1988 Dik T. Winter, CWI, Amsterdam
-- This program may be freely distributed, but not be sold.
--
-- Verify-attributes version 1.3
--
-- To adjust to the true type to be tested see the program at the end.
-- This implementation tests FLOAT.
generic
  USER_DEFINED : BOOLEAN;
  type FLOAT_TYPE is digits <>;
procedure VERIFY_ATTRIBUTES;
with TEXT_IO;
use TEXT_IO;
procedure VERIFY_ATTRIBUTES is
-- 
-- This procedure is intended to verify the attributes of floating-
-- point types.  First the machine characteristics are determined.
-- This is done according to an algorithm due to M. Malcolm,
-- CACM 15 (1972), pp. 949-951, incorporating some improvements
-- suggested by M. Gentleman and S. Marovich, CACM 17 (1974),
-- pp. 276-277.  The version given here forces storing of intermediate
-- results to memory using tasks.  Even if procedures are used to
-- do this the compiler might optimise it away; it is difficult to
-- see how a compiler might optimise the tasks away.  Forced storing
-- into memory is needed on machines where the register size exceeds
-- memory word size.  For part implementations of Ada not having tasks
-- they might be elided, unless long registers are used.  In the last
-- case there is (apparently) no possibility to obtain the true values.
-- 
-- After the machine characteristics are calculated the attributes of
-- the floating-point type given are verified (including model
-- arithmetic but the last only in part).
-- 
-- History:
--
-- Version 1.0: June 6, 1987, original version.
--              Distributed as AENWG 13.9
--
-- Version 1.1: October 1, 1987.
--              Distributed as AENWG 14.2
--              Corrects:
--                  Output format
--                  Check for rounding
--                  Calculation of improved SAFE_EMAX
--
-- Version 1.2: December, 1987.
--              Corrects:
--                  Calculation of SAFE_EMAX if attribute too large
--                  Some minor corrections
--                  Check attributes for user defined types
--
-- Version 1.3: February 16, 1988.
--              Distributed as AENWG 15.8
--              Distributed through INFO-ADA mailing list and Usenet
--              comp.lang.ada newsgroup
--              Enhanced:
--                  Allows for floating point implementation where
--                  overflow results in wrap-around
--
-- Author: Dik T. Winter,
--         Centrum voor Wiskunde en Informatica,
--         Amsterdam
-- 
-- Users of this version are kindly requested to send (preferably by
-- e-mail) the output to the author, after filling in the blanks.
-- 
  package FLOAT_IO is new TEXT_IO.FLOAT_IO (FLOAT_TYPE);
  package INTEGER_IO is new TEXT_IO.INTEGER_IO (INTEGER);

  use FLOAT_IO, INTEGER_IO;

  ERRORS             : BOOLEAN := FALSE;
  FATAL_ERRORS       : BOOLEAN := FALSE;
  OVERFLOW_ERROR     : INTEGER := 0;
  ATT_DIGITS         : INTEGER;
  MAX_DIGITS         : INTEGER;
  MANTISSA           : INTEGER;
  EPSILON            : FLOAT_TYPE;
  EMAX               : INTEGER;
  REQUIRED_EMAX      : INTEGER;
  SMALL              : FLOAT_TYPE;
  LARGE              : FLOAT_TYPE;
  SAFE_DIGITS        : INTEGER;
  SAFE_EMAX          : INTEGER;
  SAFE_V_EMAX        : INTEGER;
  SAFE_SMALL         : FLOAT_TYPE;
  SAFE_V_SMALL       : FLOAT_TYPE;
  SAFE_SMALL_1       : FLOAT_TYPE;
  SAFE_LARGE         : FLOAT_TYPE;
  SAFE_V_LARGE       : FLOAT_TYPE;
  SAFE_VERY_EMAX     : INTEGER;
  SAFE_VERY_EMIN     : INTEGER;
  SAFE_VERY_SMALL    : FLOAT_TYPE;
  SAFE_VERY_LARGE    : FLOAT_TYPE;
  MAX_MANTISSA       : INTEGER;
  MACHINE_RADIX      : INTEGER;
  MACHINE_MANTISSA   : INTEGER;
  MACHINE_ROUNDS     : BOOLEAN;
  MACHINE_EMAX       : INTEGER;
  MACHINE_EMIN       : INTEGER;
  MACHINE_VERY_EMIN  : INTEGER;
  MACHINE_LARGE      : FLOAT_TYPE;
  MACHINE_SMALL      : FLOAT_TYPE;
  MACHINE_VERY_SMALL : FLOAT_TYPE;
  MACHINE_OVERFLOWS  : BOOLEAN;
  BIT_MULTIPLIER     : INTEGER;
  REQUIRED_MANTISSA  : INTEGER;

  -- temporaries
  A                      : FLOAT_TYPE;
  B                      : FLOAT_TYPE;
  BETA                   : FLOAT_TYPE;
  BETAM1                 : FLOAT_TYPE;
  BETAINV                : FLOAT_TYPE;
  C                      : FLOAT_TYPE;
  C_PLUS                 : FLOAT_TYPE;
  C_MINUS                : FLOAT_TYPE;
  D                      : FLOAT_TYPE;
  E                      : FLOAT_TYPE;
  K                      : INTEGER;
  MODEL_ONEMINUSEPS      : FLOAT_TYPE;
  ONEMINUSEPS            : FLOAT_TYPE;
  SAFE_MODEL_ONEMINUSEPS : FLOAT_TYPE;

  -- the following constant should work up to digits 100 at least
  DIGITS_MULTIPLIER : constant := 3.32193;

  -- force storing in memory
  -- if the Ada implementation under investigation does not implement
  -- tasks, this task may be omitted and the procedure hereafter
  -- has to be changed.
  task USE_MEMORY is
    entry STORE (F : FLOAT_TYPE);
    entry FETCH (F : out FLOAT_TYPE);
  end USE_MEMORY;

  task body USE_MEMORY is
    MEMORY : FLOAT_TYPE;
  begin
    loop
      select
        accept STORE (F : FLOAT_TYPE) do
          MEMORY := F;
        end STORE;
      or
        accept FETCH (F : out FLOAT_TYPE) do
          F := MEMORY;
        end FETCH;
      or
        terminate;
      end select;
    end loop;
  end USE_MEMORY;

  -- if the task is omitted the body should be changed to the
  -- single statement:
  --    return F;
  -- However, an optimizing compiler might optimize it away.
  --
  function THROUGH_MEMORY (F : FLOAT_TYPE) return FLOAT_TYPE is
    FF : FLOAT_TYPE;
  begin
    USE_MEMORY.STORE (F);
    USE_MEMORY.FETCH (FF);
    return FF;
  end THROUGH_MEMORY;

  -- output floating point number.  format is first with hexadecimal
  -- mantissa and base MACHINE_RADIX exponent, followed by decimal
  -- format.  if the latter gives *EXCEPTION* an error might be present
  -- in the standard output routines.
  procedure PUT_FLOAT (F : FLOAT_TYPE) is
    EXP          : INTEGER;
    MANT         : FLOAT_TYPE;
    SYMBOLS      : STRING (1 .. 16) := "0123456789abcdef";
    DIG          : INTEGER;
    ACCU         : INTEGER := 0;
    BITS_IN_ACCU : INTEGER := 0;
    FACTOR       : INTEGER := 1;
  begin
    MANT := abs F;
    EXP := 0;
    if F < 0.0 then
      PUT ("-");
    end if;
    if F = 0.0 then
      PUT ("0.0");
    else
      while MANT >= 1.0 loop
        MANT := MANT * BETAINV;
        EXP := EXP + 1;
      end loop;
      while MANT < BETAINV loop
        MANT := MANT * BETA;
        EXP := EXP - 1;
      end loop;
      if MANT = BETAINV then
        -- take care for machines with inexact comparison.
        declare
          A, B : FLOAT_TYPE;
        begin
          A := MANT * BETA;
          B := A - 0.5;
          if B /= 0.5 then
            -- comparison is inexact
            EXP := EXP + 1;
            MANT := A;
          end if;
        end;
      end if;
      PUT ("16#0.");
      while MANT /= 0.0 loop
        MANT := MANT * BETA;
        DIG := INTEGER (MANT);
        if FLOAT_TYPE (DIG) > MANT then
          DIG := DIG - 1;
        end if;
        if DIG >= MACHINE_RADIX then
          DIG := MACHINE_RADIX - 1;
        end if;
        ACCU := ACCU * MACHINE_RADIX + DIG;
        BITS_IN_ACCU := BITS_IN_ACCU + BIT_MULTIPLIER;
        FACTOR := FACTOR * MACHINE_RADIX;
        MANT := MANT - FLOAT_TYPE (DIG);
        if BITS_IN_ACCU >= 4 then
          FACTOR := FACTOR / 16;
          DIG := ACCU / FACTOR;
          ACCU := ACCU - DIG * FACTOR;
          BITS_IN_ACCU := BITS_IN_ACCU - 4;
          PUT (SYMBOLS (DIG + 1));
        end if;
      end loop;
      if ACCU /= 0 then
        for I in BITS_IN_ACCU + 1 .. 4 loop
          ACCU := ACCU * 2;
        end loop;
        PUT (SYMBOLS (ACCU + 1));
      end if;
      PUT ("#*");
      PUT (MACHINE_RADIX, 0);
      PUT ("**");
      PUT (EXP, 0);
    end if;
    PUT (" (");
    begin
      PUT (F);
    exception
      when others => 
        PUT ("*EXCEPTION*");
    end;
    PUT (")");
  end PUT_FLOAT;

  function MULTIPLIER (RADIX : INTEGER) return INTEGER is
  -- Given RADIX return the number of bits in radix
    L_RADIX : INTEGER := RADIX;
    O_RADIX : INTEGER;
    VALUE   : INTEGER := 0;
  begin
    case RADIX is
      when 2 =>  return 1;
      when 4 =>  return 2;
      when 8 =>  return 3;
      when 16 =>  return 4;
      when others => 
        loop
          O_RADIX := L_RADIX;
          L_RADIX := L_RADIX / 2;
          exit when L_RADIX * 2 /= O_RADIX;
          VALUE := VALUE + 1;
          if L_RADIX = 1 then
            return VALUE;
          end if;
        end loop;
        PUT ("Something weird is happening, the machine radix is not a");
        NEW_LINE;
        PUT ("power of 2.  This might play havoc with model arithmetic");
        NEW_LINE;
        PUT ("We must be very careful there.");
        NEW_LINE;
        return 0;
    end case;
  end MULTIPLIER;

begin
  NEW_PAGE;
  -- determine MACHINE_RADIX
  -- first multiply A by 2 until miltiplication is inexact when 1 is
  -- added to it (i.e. A becomes the smallest power of two such that
  -- addition of 1 is thrown away).
  A := 1.0;
  while (THROUGH_MEMORY (A + 1.0) - A) - 1.0 = 0.0 loop
    A := A + A;
  end loop;
  -- find the smallest power of 2 (B) such that addition of B to A
  -- increases A.
  B := 1.0;
  while THROUGH_MEMORY (A + B) - A = 0.0 loop
    B := B + B;
  end loop;
  MACHINE_RADIX := INTEGER (THROUGH_MEMORY (A + B) - A);
  BIT_MULTIPLIER := MULTIPLIER (MACHINE_RADIX);
  -- determine MACHINE_MANTISSA
  BETA := FLOAT_TYPE (MACHINE_RADIX);
  BETAINV := 1.0 / BETA;
  BETAM1 := BETA - 1.0;
  MACHINE_MANTISSA := 0;
  B := 1.0;
  while (THROUGH_MEMORY (B + 1.0) - B) - 1.0 = 0.0 loop
    B := B * BETA;
    MACHINE_MANTISSA := MACHINE_MANTISSA + 1;
  end loop;
  -- determine MACHINE_ROUNDS
  -- we can get away with division by two because MACHINE_RADIX has to
  -- be even (even a power of 2).
  E := B;
  C := BETA * 0.5;
  D := BETA;
  for I in 1 .. MACHINE_MANTISSA loop
    D := D * BETAINV;
  end loop;
  -- C is half the difference of B and the next higher number; C + D is the
  -- number next above C while C - D is the number next below D.
  -- we cannot check rounding with C itself, because this may round either
  -- way.
  C_PLUS := C + D;
  C_MINUS := C - D;
  -- if MACHINE_RADIX is 2 we can stuff one more bit in C_MINUS
  if MACHINE_RADIX = 2 then
    C_MINUS := C_MINUS + D * 0.5;
  end if;
  MACHINE_ROUNDS := FALSE;
  if THROUGH_MEMORY (E + C_PLUS) - E /= 0.0 then
    MACHINE_ROUNDS := TRUE;
  end if;
  if THROUGH_MEMORY (E + C_MINUS) - E /= 0.0 then
    MACHINE_ROUNDS := FALSE;
  end if;
  -- determine MACHINE_LARGE, MACHINE_SMALL, MACHINE_VERY_SMALL,
  -- MACHINE_EMAX, MACHINE_EMIN and MACHINE_VERY_EMIN.
  -- MACHINE_SMALL (and the associated MACHINE_EMIN) is the
  -- smallest hardware number with full precision, numbers
  -- between MACHINE_VERY_SMALL and MACHINE_SMALL have less
  -- precision (gradual underflow).
  ONEMINUSEPS := 0.0;
  A := BETAM1;
  for I in 1 .. MACHINE_MANTISSA loop
    A := A * BETAINV;
    ONEMINUSEPS := ONEMINUSEPS + A;
  end loop;
  A := ONEMINUSEPS;
  MACHINE_EMAX := 0;
  MACHINE_OVERFLOWS := FALSE;
  loop
    begin
      MACHINE_LARGE := A;
      A := THROUGH_MEMORY (A * BETA);
      exit when A * BETAINV /= MACHINE_LARGE or A <= MACHINE_LARGE;
      MACHINE_EMAX := MACHINE_EMAX + 1;
    exception
      when NUMERIC_ERROR => 
        MACHINE_OVERFLOWS := TRUE;
        exit;
      when CONSTRAINT_ERROR => 
        PUT ("Overflow raises CONSTRAINT_ERROR.");
        ERRORS := TRUE;
        NEW_LINE;
        MACHINE_OVERFLOWS := TRUE;
        exit;
      when others => 
        PUT ("Catching overflow but it was not NUMERIC_ERROR that was raised.");
        NEW_LINE;
        ERRORS := TRUE;
        MACHINE_OVERFLOWS := TRUE;
        exit;
    end;
  end loop;
  MACHINE_EMIN := 0;
  A := ONEMINUSEPS;
  MACHINE_SMALL := BETAINV;
  loop
    begin
      B := A;
      A := THROUGH_MEMORY (A * BETAINV);
      exit when A * BETA /= B;
      MACHINE_EMIN := MACHINE_EMIN - 1;
      MACHINE_SMALL := MACHINE_SMALL * BETAINV;
    exception
      when others => 
        PUT ("Apparently underflow raises an (illegal) exception.");
        NEW_LINE;
        ERRORS := TRUE;
        exit;
    end;
  end loop;
  A := MACHINE_SMALL;
  MACHINE_VERY_EMIN := MACHINE_EMIN;
  loop
    begin
      MACHINE_VERY_SMALL := A;
      A := THROUGH_MEMORY (A * BETAINV);
      exit when A >= MACHINE_VERY_SMALL or A = 0.0;
      MACHINE_VERY_EMIN := MACHINE_VERY_EMIN - 1;
    exception
      when others => 
        PUT ("Apparently underflow raises an (illegal) exception.");
        NEW_LINE;
        ERRORS := TRUE;
        exit;
    end;
  end loop;
  -- Now we have the machine characteristics and can compare to the
  -- attributes.  First with the MACHINE attributes.
  PUT ("MACHINE_RADIX is ");
  PUT (MACHINE_RADIX, 0);
  if FLOAT_TYPE'MACHINE_RADIX /= MACHINE_RADIX then
    PUT (" but the attribute gives ");
    PUT (FLOAT_TYPE'MACHINE_RADIX, 0);
    ERRORS := TRUE;
  end if;
  NEW_LINE;
  PUT ("MACHINE_MANTISSA is ");
  PUT (MACHINE_MANTISSA, 0);
  if FLOAT_TYPE'MACHINE_MANTISSA /= MACHINE_MANTISSA then
    PUT (" but the attribute gives ");
    PUT (FLOAT_TYPE'MACHINE_MANTISSA, 0);
    ERRORS := TRUE;
    if MULTIPLIER (FLOAT_TYPE'MACHINE_RADIX) *
       FLOAT_TYPE'MACHINE_MANTISSA =
       BIT_MULTIPLIER * MACHINE_MANTISSA then
      NEW_LINE;
      PUT ("But it fits with the wrong value of MACHINE_RADIX");
    end if;
  end if;
  NEW_LINE;
  PUT ("MACHINE_EMAX is ");
  PUT (MACHINE_EMAX, 0);
  if FLOAT_TYPE'MACHINE_EMAX /= MACHINE_EMAX then
    PUT (" but the attribute gives ");
    PUT (FLOAT_TYPE'MACHINE_EMAX, 0);
    ERRORS := TRUE;
  end if;
  NEW_LINE;
  PUT ("MACHINE_EMIN is ");
  PUT (MACHINE_EMIN, 0);
  if FLOAT_TYPE'MACHINE_EMIN /= MACHINE_VERY_EMIN then
    if FLOAT_TYPE'MACHINE_EMIN /= MACHINE_EMIN then
      PUT (" but the attribute gives ");
      PUT (FLOAT_TYPE'MACHINE_EMIN, 0);
      ERRORS := TRUE;
    else
      PUT (" apparently not the smallest number was used;");
      NEW_LINE;
      PUT (" as the attribute gives ");
      PUT (FLOAT_TYPE'MACHINE_EMIN, 0);
    end if;
  end if;
  NEW_LINE;
  -- Give also pseudo attributes
  if MACHINE_EMIN /= MACHINE_VERY_EMIN then
    PUT ("'MACHINE_VERY_EMIN' is ");
    PUT (MACHINE_VERY_EMIN, 0);
    NEW_LINE;
  end if;
  PUT ("'MACHINE_LARGE' is ");
  PUT_FLOAT (MACHINE_LARGE);
  NEW_LINE;
  PUT ("'MACHINE_SMALL' is ");
  PUT_FLOAT (MACHINE_SMALL);
  NEW_LINE;
  if MACHINE_SMALL /= MACHINE_VERY_SMALL then
    PUT ("'MACHINE_VERY_SMALL' is ");
    PUT_FLOAT (MACHINE_VERY_SMALL);
    NEW_LINE;
  end if;
  PUT ("MACHINE_ROUNDS is ");
  if MACHINE_ROUNDS then
    PUT ("TRUE");
  else
    PUT ("FALSE");
  end if;
  if MACHINE_ROUNDS /= FLOAT_TYPE'MACHINE_ROUNDS then
    -- rounding is not properly defined, does it mean the nearest
    -- harware number?
    PUT (" but the attribute does not agree");
    NEW_LINE;
    if MACHINE_ROUNDS then
      PUT ("probably not checked thoroughly enough.");
    else
      PUT ("(another interpretation?).");
      if THROUGH_MEMORY (E + C_PLUS) - E = 0.0 then
        NEW_LINE;
        PUT_FLOAT (E);
        PUT (" + ");
        PUT_FLOAT (C_PLUS);
        PUT (" = ");
        NEW_LINE;
        PUT ("          ");
        PUT_FLOAT (E);
        NEW_LINE;
        PUT ("should be ");
        PUT_FLOAT (E + BETA);
      end if;
      if THROUGH_MEMORY (E + C_MINUS) - E /= 0.0 then
        NEW_LINE;
        PUT_FLOAT (E);
        PUT (" + ");
        PUT_FLOAT (C_MINUS);
        PUT (" = ");
        NEW_LINE;
        PUT ("          ");
        PUT_FLOAT (E + C_MINUS);
        NEW_LINE;
        PUT ("should be ");
        PUT_FLOAT (E);
      end if;
    end if;
  end if;
  NEW_LINE;
  PUT ("MACHINE_OVERFLOWS is ");
  if MACHINE_OVERFLOWS then
    PUT ("TRUE");
  else
    PUT ("FALSE");
  end if;
  if MACHINE_OVERFLOWS /= FLOAT_TYPE'MACHINE_OVERFLOWS then
    if MACHINE_OVERFLOWS then
      -- might have that the system uses the strict interpretation of
      -- MACHINE_OVERFLOWS and hence is not allowed to return FALSE.
      PUT (" the attribute says no, perhaps a stricter interpretation.");
    else
      PUT (" the attribute says yes; clearly wrong.");
      ERRORS := TRUE;
    end if;
  end if;
  NEW_LINE;
  -- Now check the other attributes
  -- Cater for wobbling precision
  MAX_MANTISSA := (MACHINE_MANTISSA - 1) * BIT_MULTIPLIER + 1;
  ATT_DIGITS := FLOAT_TYPE'DIGITS;
  A := FLOAT_TYPE (ATT_DIGITS) * DIGITS_MULTIPLIER + 1.0;
  REQUIRED_MANTISSA := INTEGER (A);
  if FLOAT_TYPE (REQUIRED_MANTISSA) < A then
    REQUIRED_MANTISSA := REQUIRED_MANTISSA + 1;
  end if;
  MANTISSA := REQUIRED_MANTISSA;
  REQUIRED_EMAX := REQUIRED_MANTISSA * 4;
  EMAX := REQUIRED_EMAX;
  MAX_DIGITS := ATT_DIGITS;
  PUT ("DIGITS gives ");
  PUT (ATT_DIGITS, 0);
  NEW_LINE;
  -- check egainst MACHINE_MANTISSA
  if REQUIRED_MANTISSA > MAX_MANTISSA then
    if BIT_MULTIPLIER /= 0 then
      PUT ("The mantissa requirements are more than the hardware gives;");
      NEW_LINE;
      ERRORS := TRUE;
      FATAL_ERRORS := TRUE;
      while REQUIRED_MANTISSA > MAX_MANTISSA loop
        MAX_DIGITS := MAX_DIGITS - 1;
        A := FLOAT_TYPE (MAX_DIGITS) * DIGITS_MULTIPLIER + 1.0;
        REQUIRED_MANTISSA := INTEGER (A);
        if FLOAT_TYPE (REQUIRED_MANTISSA) < A then
          REQUIRED_MANTISSA := REQUIRED_MANTISSA + 1;
        end if;
      end loop;
      REQUIRED_EMAX := REQUIRED_MANTISSA * 4;
    else
      PUT ("This cannot be verified.");
      NEW_LINE;
    end if;
  elsif REQUIRED_MANTISSA < MAX_MANTISSA then
    -- MACHINE_MANTISSA would probably allow more
    A := FLOAT_TYPE (ATT_DIGITS + 1) * DIGITS_MULTIPLIER + 1.0;
    K := INTEGER (A);
    if FLOAT_TYPE (K) < A then
      K := K + 1;
    end if;
    if K <= MAX_MANTISSA then
      PUT ("Apparently DIGITS is limited by declaration or due to exponent");
      PUT (" limitations.");
      NEW_LINE;
    end if;
  end if;
  -- check against exponent range
  if REQUIRED_EMAX > MACHINE_EMAX * BIT_MULTIPLIER or
     REQUIRED_EMAX > -MACHINE_EMIN * BIT_MULTIPLIER then
    if BIT_MULTIPLIER /= 0 then
      ERRORS := TRUE;
      FATAL_ERRORS := TRUE;
      PUT ("The exponent requirements are more than the hardware gives.");
      NEW_LINE;
      if MAX_DIGITS /= ATT_DIGITS then
        PUT ("Even after adjustment for mantissa limitations!");
        NEW_LINE;
      end if;
      while REQUIRED_EMAX > MACHINE_EMAX * BIT_MULTIPLIER or
            REQUIRED_EMAX > -MACHINE_EMIN * BIT_MULTIPLIER loop
        MAX_DIGITS := MAX_DIGITS - 1;
        A := FLOAT_TYPE (MAX_DIGITS) * DIGITS_MULTIPLIER + 1.0;
        REQUIRED_MANTISSA := INTEGER (A);
        if FLOAT_TYPE (REQUIRED_MANTISSA) < A then
          REQUIRED_MANTISSA := REQUIRED_MANTISSA + 1;
        end if;
        REQUIRED_EMAX := REQUIRED_MANTISSA * 4;
      end loop;
    end if;
  end if;
  if ATT_DIGITS /= MAX_DIGITS then
    -- this is what the hardware allows
    PUT ("DIGITS should not be larger than ");
    PUT (MAX_DIGITS, 0);
    NEW_LINE;
  end if;
  PUT ("MANTISSA is ");
  PUT (MANTISSA, 0);
  if ATT_DIGITS /= MAX_DIGITS then
    PUT (" but with proper DIGITS value it is ");
    PUT (REQUIRED_MANTISSA, 0);
  end if;
  if FLOAT_TYPE'MANTISSA /= MANTISSA then
    ERRORS := TRUE;
    FATAL_ERRORS := TRUE;
    PUT (" the attribute gives ");
    PUT (FLOAT_TYPE'MANTISSA, 0);
    if FLOAT_TYPE'MANTISSA = REQUIRED_MANTISSA then
      PUT (" that fits the proper value of DIGITS!");
    end if;
    MANTISSA := FLOAT_TYPE'MANTISSA;
    EMAX := MANTISSA * 4;
  end if;
  NEW_LINE;
  PUT ("EMAX is ");
  PUT (REQUIRED_EMAX, 0);
  if REQUIRED_EMAX /= FLOAT_TYPE'EMAX then
    ERRORS := TRUE;
    FATAL_ERRORS := TRUE;
    PUT (" the attribute gives ");
    PUT (FLOAT_TYPE'EMAX, 0);
    if EMAX = FLOAT_TYPE'EMAX then
      PUT ("; that fits other attributes.");
    end if;
  end if;
  NEW_LINE;
  if FATAL_ERRORS then
    PUT ("Due to the preceeding errors the remainder may be faulty");
    NEW_LINE;
    PUT ("when comparing to attributes.");
    NEW_LINE;
    PUT ("This is because the attributes might match earlier wrong");
    NEW_LINE;
    PUT ("attributes.");
    NEW_LINE;
    MANTISSA := REQUIRED_MANTISSA;
    EMAX := REQUIRED_EMAX;
    ATT_DIGITS := MAX_DIGITS;
  end if;
  -- now calculate LARGE and SMALL
  -- (cross your fingers you will not get exceptions here.)
  MODEL_ONEMINUSEPS := 0.0;
  A := 1.0;
  for I in 1 .. MANTISSA loop
    A := A * 0.5;
    MODEL_ONEMINUSEPS := MODEL_ONEMINUSEPS + A;
  end loop;
  LARGE := MODEL_ONEMINUSEPS;
  for I in 1 .. EMAX loop
    LARGE := LARGE * 2.0;
  end loop;
  PUT ("LARGE is ");
  PUT_FLOAT (LARGE);
  if LARGE /= FLOAT_TYPE'LARGE then
    PUT (" but the attribute gives ");
    PUT_FLOAT (FLOAT_TYPE'LARGE);
    ERRORS := TRUE;
  end if;
  NEW_LINE;
  SMALL := 0.5;
  for I in 1 .. EMAX loop
    SMALL := SMALL * 0.5;
  end loop;
  PUT ("SMALL is ");
  PUT_FLOAT (SMALL);
  if SMALL /= FLOAT_TYPE'SMALL then
    PUT (" but the attribute gives ");
    PUT_FLOAT (FLOAT_TYPE'SMALL);
    ERRORS := TRUE;
  end if;
  NEW_LINE;
  EPSILON := 1.0;
  for I in 2 .. MANTISSA loop
    EPSILON := EPSILON * 0.5;
  end loop;
  PUT ("EPSILON is ");
  PUT_FLOAT (EPSILON);
  if EPSILON /= FLOAT_TYPE'EPSILON then
    PUT (" but the attribute gives ");
    PUT_FLOAT (FLOAT_TYPE'EPSILON);
    ERRORS := TRUE;
  end if;
  NEW_LINE;
  -- SAFE_DIGITS should be FLOAT_TYPE'BASE'DIGITS
  -- Assume either a predefined type or a user defined type of the form
  -- type USER_TYPE is digits <N>;
  SAFE_DIGITS := FLOAT_TYPE'BASE'DIGITS;
  if SAFE_DIGITS /= ATT_DIGITS then
    if not USER_DEFINED then
      PUT ("Although this is a predefined type, the attributes of the");
      NEW_LINE;
      PUT ("base type do not match!");
      NEW_LINE;
      ERRORS := TRUE;
    end if;
    SAFE_MODEL_ONEMINUSEPS := 0.0;
    A := 1.0;
    for I in 1 .. FLOAT_TYPE'BASE'MANTISSA loop
      A := A * 0.5;
      SAFE_MODEL_ONEMINUSEPS := SAFE_MODEL_ONEMINUSEPS + A;
    end loop;
  else
    SAFE_MODEL_ONEMINUSEPS := MODEL_ONEMINUSEPS;
    if USER_DEFINED then
      PUT ("Although this is a user defined type, the attributes of the");
      NEW_LINE;
      PUT ("base type appear to match the attributes of this type.");
      NEW_LINE;
      PUT ("Probably there is a predefined type with the specified number");
      PUT (" of digits.");
      NEW_LINE;
      PUT ("But it is more likely that the system is wrong.");
      NEW_LINE;
      ERRORS := TRUE;
    end if;
  end if;
  SAFE_EMAX := FLOAT_TYPE'SAFE_EMAX;
  PUT ("SAFE_EMAX gives ");
  PUT (SAFE_EMAX, 0);
  -- checking SAFE attributes; note: the range must be symmetric!
  SAFE_LARGE := SAFE_MODEL_ONEMINUSEPS;
  SAFE_SMALL_1 := SAFE_MODEL_ONEMINUSEPS;
  for I in 1 .. SAFE_EMAX loop
    begin
      A := THROUGH_MEMORY (SAFE_LARGE * 2.0);
      B := THROUGH_MEMORY (SAFE_SMALL_1 * 0.5);
      if SAFE_LARGE * 2.0 /= A or SAFE_SMALL_1 * 0.5 /= B then
        PUT (" detected lack of model arithmetic within given range.");
        NEW_LINE;
        PUT ("SAFE_EMAX has been adjusted to ");
        SAFE_EMAX := I - 1;
        PUT (SAFE_EMAX, 0);
        ERRORS := TRUE;
        exit;
      end if;
      SAFE_LARGE := A;
      SAFE_SMALL_1 := B;
    exception
      when NUMERIC_ERROR => 
        PUT (" caught NUMERIC_ERROR during verification.");
        NEW_LINE;
        PUT ("SAFE_EMAX has been adjusted to ");
        SAFE_EMAX := I - 1;
        PUT (SAFE_EMAX, 0);
        ERRORS := TRUE;
        exit;
      when CONSTRAINT_ERROR => 
        PUT (" caught CONSTRAINT_ERROR during verification.");
        NEW_LINE;
        PUT ("SAFE_EMAX has been adjusted to ");
        SAFE_EMAX := I - 1;
        PUT (SAFE_EMAX, 0);
        ERRORS := TRUE;
        exit;
      when others => 
        PUT (" caught some strange exception during verification.");
        NEW_LINE;
        PUT ("SAFE_EMAX has been adjusted to ");
        SAFE_EMAX := I - 1;
        PUT (SAFE_EMAX, 0);
        ERRORS := TRUE;
        exit;
    end;
  end loop;
  NEW_LINE;
  SAFE_SMALL := 0.5;
  for I in 1 .. SAFE_EMAX loop
    SAFE_SMALL := SAFE_SMALL * 0.5;
  end loop;
  PUT ("SAFE_LARGE is ");
  PUT_FLOAT (SAFE_LARGE);
  if SAFE_LARGE /= FLOAT_TYPE'SAFE_LARGE then
    PUT (" the attribute gives ");
    PUT_FLOAT (FLOAT_TYPE'SAFE_LARGE);
    ERRORS := TRUE;
  end if;
  NEW_LINE;
  PUT ("SAFE_SMALL is ");
  PUT_FLOAT (SAFE_SMALL);
  if SAFE_SMALL /= FLOAT_TYPE'SAFE_SMALL then
    PUT (" the attribute gives ");
    PUT_FLOAT (FLOAT_TYPE'SAFE_SMALL);
    ERRORS := TRUE;
  end if;
  NEW_LINE;
  if FLOAT_TYPE'SAFE_EMAX /= FLOAT_TYPE'BASE'SAFE_EMAX or
     FLOAT_TYPE'SAFE_LARGE /= FLOAT_TYPE'BASE'SAFE_LARGE or
     FLOAT_TYPE'SAFE_SMALL /= FLOAT_TYPE'BASE'SAFE_SMALL then
    PUT ("SAFE_EMAX, SAFE_LARGE and/or SAFE_SMALL does not match the");
    NEW_LINE;
    PUT ("corresponding attribute of the base type.");
    NEW_LINE;
    ERRORS := TRUE;
  end if;
  SAFE_V_LARGE := SAFE_LARGE;
  SAFE_V_SMALL := SAFE_SMALL;
  SAFE_V_EMAX := SAFE_EMAX;
  if SAFE_EMAX = FLOAT_TYPE'SAFE_EMAX then
    A := SAFE_LARGE;
    B := SAFE_SMALL_1;
    loop
      begin
        SAFE_V_LARGE := A;
        SAFE_SMALL_1 := B;
        A := THROUGH_MEMORY (A * 2.0);
        B := THROUGH_MEMORY (B * 0.5);
        exit when A * 0.5 /= SAFE_V_LARGE or B * 2.0 /= SAFE_SMALL_1;
        SAFE_V_EMAX := SAFE_V_EMAX + 1;
        SAFE_V_SMALL := SAFE_V_SMALL * 0.5;
      exception
        when NUMERIC_ERROR => 
          exit;
        when CONSTRAINT_ERROR => 
          PUT ("Caught unexpected CONSTRAINT_ERROR.");
          NEW_LINE;
          exit;
        when others => 
          PUT ("Caught some strange exception.");
          NEW_LINE;
          ERRORS := TRUE;
          exit;
      end;
    end loop;
    if SAFE_V_EMAX /= FLOAT_TYPE'SAFE_EMAX then
      PUT ("SAFE_EMAX is probably too pessimistic, the following values");
      PUT (" might be better:");
      NEW_LINE;
      PUT ("SAFE_EMAX could be ");
      PUT (SAFE_V_EMAX, 0);
      NEW_LINE;
      PUT ("SAFE_LARGE could be ");
      PUT_FLOAT (SAFE_V_LARGE);
      NEW_LINE;
      PUT ("SAFE_SMALL could be ");
      PUT_FLOAT (SAFE_V_SMALL);
      NEW_LINE;
    end if;
  end if;
  A := SAFE_V_LARGE;
  SAFE_VERY_EMAX := SAFE_V_EMAX;
  loop
    begin
      SAFE_VERY_LARGE := A;
      A := THROUGH_MEMORY (A * 2.0);
      exit when A * 0.5 /= SAFE_VERY_LARGE;
      SAFE_VERY_EMAX := SAFE_VERY_EMAX + 1;
    exception
      when NUMERIC_ERROR => 
        exit;
      when CONSTRAINT_ERROR => 
        PUT ("Caught unexpected CONSTRAINT_ERROR.");
        NEW_LINE;
        exit;
      when others => 
        PUT ("Caught some strange exception.");
        NEW_LINE;
        ERRORS := TRUE;
        exit;
    end;
  end loop;
  B := SAFE_SMALL_1;
  SAFE_VERY_SMALL := SAFE_V_SMALL;
  SAFE_VERY_EMIN := - SAFE_V_EMAX;
  loop
    begin
      SAFE_SMALL_1 := B;
      B := THROUGH_MEMORY (B * 0.5);
      exit when B * 2.0 /= SAFE_SMALL_1;
      SAFE_VERY_EMIN := SAFE_VERY_EMIN - 1;
      SAFE_VERY_SMALL := SAFE_VERY_SMALL * 0.5;
    exception
      when others => 
        PUT ("Caught some strange exception.");
        NEW_LINE;
        ERRORS := TRUE;
        exit;
    end;
  end loop;
  if SAFE_V_EMAX /= SAFE_VERY_EMAX or SAFE_V_EMAX /= - SAFE_VERY_EMIN then
    PUT ("The safe exponent range ought to be asymmetric with:");
    NEW_LINE;
    PUT ("SAFE_EMAX is ");
    PUT (SAFE_VERY_EMAX, 0);
    NEW_LINE;
    PUT ("SAFE_EMIN is ");
    PUT (SAFE_VERY_EMIN, 0);
    NEW_LINE;
    PUT ("SAFE_LARGE is ");
    PUT_FLOAT (SAFE_VERY_LARGE);
    NEW_LINE;
    PUT ("SAFE_SMALL is ");
    PUT_FLOAT (SAFE_VERY_SMALL);
    NEW_LINE;
  end if;
  if FLOAT_TYPE'MACHINE_OVERFLOWS and MACHINE_OVERFLOWS then
    PUT ("Verifying strictness of overflow interpretations.");
    NEW_LINE;
    begin
      begin
        B := EPSILON * 0.5 * 0.5;
        for I in 1 .. SAFE_EMAX loop
          B := B * 2.0;
        end loop;
        A := SAFE_LARGE + B;
        OVERFLOW_ERROR := 1;
        A := SAFE_LARGE * 2.0;
        OVERFLOW_ERROR := 2;
        for I in SAFE_EMAX + 1 .. SAFE_V_EMAX loop
          B := B * 2.0;
        end loop;
        A := SAFE_V_LARGE + B;
        OVERFLOW_ERROR := 3;
        A := SAFE_V_LARGE * 2.0;
        OVERFLOW_ERROR := 4;
        for I in SAFE_V_EMAX + 1 .. SAFE_VERY_EMAX loop
          B := B * 2.0;
        end loop;
        A := SAFE_VERY_LARGE + B;
        OVERFLOW_ERROR := 3;
        A := SAFE_VERY_LARGE * 2.0;
        OVERFLOW_ERROR := 4;
        raise NUMERIC_ERROR;
      exception
        when NUMERIC_ERROR =>
          raise;
        when others =>
          PUT ("Wrong exception raised on overflow.");
          NEW_LINE;
          raise NUMERIC_ERROR;
      end;
    exception
      when others =>
        case OVERFLOW_ERROR is
          when 0 =>
            PUT ("MACHINE_OVERFLOWS appears to be according to LRM 4.5.7(7).");
          when 1 =>
            PUT ("MACHINE_OVERFLOWS is not according to LRM 4.5.7(7)");
            NEW_LINE;
            PUT ("Overflow occurs for numbers slightly larger than");
            PUT (" SAFE_LARGE.");
          when 2 =>
            PUT ("If the recalculated SAFE attributes are used,");
            NEW_LINE;
            PUT ("MACHINE_OVERFLOWS appears to be according to LRM 4.5.7(7).");
          when 3 =>
            PUT ("MACHINE_OVERFLOWS is not according to LRM 4.5.7(7)");
            NEW_LINE;
            PUT ("for the recalculated SAFE attributes.");
            if SAFE_V_EMAX /= SAFE_VERY_EMAX then
              NEW_LINE;
              PUT ("But the asymmetric attributes help.");
            end if;
          when 4 =>
            PUT ("If the asymmetric SAFE attributes are used,");
            NEW_LINE;
            PUT ("MACHINE_OVERFLOWS appears to be according to LRM 4.5.7(7).");
          when 5 =>
            PUT ("Even if the asymmetric attributes are used,");
            NEW_LINE;
            PUT ("MACHINE_OVERFLOWS is not according to LRM 4.5.7(7)");
          when 6 =>
            PUT ("Cannot get an overflow exception with SAFE attributes,");
            NEW_LINE;
            PUT ("even not with the asymmetric ones.");
            NEW_LINE;
            PUT ("SAFE_LARGE * 2.0 does not overflow!");
          when others =>
            PUT ("This cannot happen!");
        end case;
        NEW_LINE;
    end;
  end if;
  if ERRORS then
    PUT ("It appears that some attributes are invalid.");
    NEW_LINE;
  else
    PUT ("No erroneous attributes were found");
    if SAFE_EMAX /= FLOAT_TYPE'SAFE_EMAX then
      PUT ("; but SAFE_EMAX requires further verification");
    end if;
    PUT (".");
    NEW_LINE;
  end if;
  PUT ("This concludes the verification.");
  NEW_LINE;
exception
  when NUMERIC_ERROR => 
    PUT ("Caught NUMERIC_ERROR in an unexpected place.");
    NEW_LINE;
    PUT ("Verification has to be abandoned.");
    NEW_LINE;
    return;
  when others => 
    PUT ("Caught some exception in an unexpected place.");
    NEW_LINE;
    PUT ("Verification has to be abandoned.");
    NEW_LINE;
    return;
end VERIFY_ATTRIBUTES;
with TEXT_IO;
use TEXT_IO;
procedure HEADER is
begin
  NEW_PAGE;
  PUT ("VERIFY Version 1.3");
  NEW_LINE;
  PUT ("Floating point attribute verifyer.");
  NEW_LINE;
  NEW_LINE;
  PUT ("Please send this output to the author after filling in the blanks.");
  NEW_LINE;
  PUT ("E-mail is preferred.");
  NEW_LINE;
  NEW_LINE;
  PUT ("E-mail: dik@cwi.nl");
  NEW_LINE;
  PUT ("Bitnet/EARN: dik@mcvax");
  NEW_LINE;
  PUT ("ARPA: dik%cwi.nl@uunet.uu.net");
  NEW_LINE;
  PUT ("Surface mail:");
  NEW_LINE;
  PUT ("    Dik T. Winter");
  NEW_LINE;
  PUT ("    Centrum voor Wiskunde en Informatica");
  NEW_LINE;
  PUT ("    Kruislaan 413");
  NEW_LINE;
  PUT ("    1098 SJ  Amsterdam");
  NEW_LINE;
  PUT ("    Nederland");
  NEW_LINE;
  NEW_LINE;
  PUT ("Please fill in the following blanks:");
  NEW_LINE;
  PUT ("Machine (manufacturer/type):");
  NEW_LINE;
  PUT ("Model:");
  NEW_LINE;
  PUT ("Hardware floating-point?");
  NEW_LINE;
  PUT ("If a separate processor, which one?");
  NEW_LINE;
  NEW_LINE;
  PUT ("Compiler manifacturer:");
  NEW_LINE;
  PUT ("Version (be as complete as possible):");
  NEW_LINE;
end HEADER;
with VERIFY_ATTRIBUTES, HEADER, TEXT_IO;
use TEXT_IO;
procedure PROGRAM is
  -- change the following lines to reflect the actual type to be tested.
  -- these line must be either of the form:
  -- type FLOAT_TO_TEST is new <predefined type>;
  -- or of the form:
  -- type USER_TYPEs digits <N>;
  -- in the latter case the program assumes that the attributes of the
  -- predefined types are verified (and correct!).
  -- the first parameter to VERIFY_ATTRIBUTES is TRUE for
  -- user defined types
  type FLOAT_TO_TEST is new FLOAT;
  type USER_TYPE is digits (FLOAT'DIGITS - 1);
  procedure VF_P is new VERIFY_ATTRIBUTES (USER_DEFINED => FALSE,
                                           FLOAT_TYPE   => FLOAT_TO_TEST);
  procedure VF_U is new VERIFY_ATTRIBUTES (USER_DEFINED => TRUE,
                                           FLOAT_TYPE   => USER_TYPE);
begin
  HEADER;
  NEW_PAGE;
  PUT ("Checking predefined type.");
  NEW_LINE;
  VF_P;
  NEW_PAGE;
  PUT ("Checking user defined type.");
  NEW_LINE;
  VF_U;
end PROGRAM;
-- 
dik t. winter, cwi, amsterdam, nederland
INTERNET   : dik@cwi.nl
BITNET/EARN: dik@mcvax