Top File of PVS float Library

 
top: THEORY
%------------------------------------------------------------------------
% Formalization of Floating Point numbers in PVS
%  
% The hardware level model was developed by Paul Miner (NASA LaRC). 
%   P. Miner, Defining the IEEE-854 floating-point standard in PVS, 
%   NASA/TM-95-110167, NASA Langley Research Center, 1995.
%   http://techreports.larc.nasa.gov/ltrs/dublincore/1995/NASA-95-tm110167.html
%
% The high level model was developed by Sylvie Boldo (ENS-Lyon) while
% visiting NIA.
%   S. Boldo, Preuves formelles en arithmetiques a virgule flottante, 
%   PhD. Thesis, Ecole Normale Superieure de Lyon, 2004.
%   http://www.ens-lyon.fr/LIP/Pub/Rapports/PhD/PhD2004/PhD2004-05.pdf
% This work has been partially funded by
% * NASA LaRC under the Research Cooperative Agreement No. NCC-1-02043
%   awarded to the National Institute of Aerospace
% * French CNRS under PICS 2533
%   awarded to the Laboratoire de l'Informatique du Parallelisme
%
% Users are invited to send feedback information to the authors  
% and to Marc.Daumas@ENS-Lyon.Fr
%
% Version 1.1    11/30/2005
%
% Note: This library currently links with lnexp (non-foundational).
%       If you want,  you can change this to lnexp_fnd in theory float.
%------------------------------------------------------------------------
BEGIN

  IMPORTING % High-level model (SB)

            float, axpy, 

            % Hardware-level (PyM)

            IEEE_854, IEEE_854_defs, infinity_arithmetic,
            comparison1, NaN_ops, arithmetic_ops, IEEE_854_remainder,
            IEEE_854_fp_int, real_to_fp, over_under, 
            IEEE_854_values, round, fp_round_aux,
            sum_lemmas, enumerated_type_defs, sum_hack,

            % Equivalence between the two models (SB)

            IEEE_link   
END top

The tag identifies links that are outside the NASA domain